Skip to content

Commit

Permalink
Merge pull request #1598 from mit-plv/garagedoor-prettify
Browse files Browse the repository at this point in the history 
Garagedoor Prettification
  • Loading branch information
@andres-erbsen
andres-erbsen authored May 3, 2023
2 parents 071b78a + abc1978 commit 79642ca
Show file tree
Hide file tree
Showing 2 changed files with 254 additions and 218 deletions.
230 changes: 12 additions & 218 deletions src/Bedrock/End2End/X25519/GarageDoor.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175,11 +175,11 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
fun '(seed, sk) ioh '(SEED, SK) =>
(lightbulb_spec.lan9250_recv_no_packet _ ioh \/
lightbulb_spec.lan9250_recv_packet_too_long _ ioh \/
TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) \/
TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) /\ SEED=seed /\ SK=sk \/
(exists incoming, lightbulb_spec.lan9250_recv _ incoming ioh /\
let ethertype := le_combine (rev (firstn 2 (skipn 12 incoming))) in ethertype < 1536 \/
let ipproto := nth 23 incoming x00 in ipproto <> x11 \/
(length incoming <> 14+20+8 +2+16 +4 /\ length incoming <> 14+20+8 +2+32 +4)%nat) \/
let ipproto := nth 23 incoming x00 in (ipproto <> x11 \/
length incoming <> 14+20+8 +2+16 +4 /\ length incoming <> 14+20+8 +2+32 +4)%nat) /\ SEED=seed /\ SK=sk \/
exists (mac_local mac_remote : tuple byte 6),
exists (ethertype : Z) (ih_const : tuple byte 2) (ip_length : Z) (ip_idff : tuple byte 5),
exists (ipproto := x11) (ip_checksum : Z) (ip_local ip_remote : tuple byte 4),
Expand All @@ -205,8 +205,9 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
(word.unsigned set0 = 1 <-> firstn 16 v = m) /\
(word.unsigned set1 = 1 <-> skipn 16 v = m) /\
action = word.or (word.and doorstate (word.of_Z (Z.clearbit (Z.clearbit (2^32-1) 11) 12))) (word.slu (word.or (word.slu set1 (word.of_Z 1)) set0) (word.of_Z 11)) /\
(* /\ (word.unsigned set0 <> 0 \/ word.unsigned set1 <> 0 -> SEED++SK = RupicolaCrypto.Spec.chacha20_encrypt k (Z.to_nat (word.unsigned counter)) _ _) *)
(word.unsigned set1 = 0 -> word.unsigned set0 = 0 -> SEED=seed /\ SK=sk))) \/
(word.unsigned (word.or set0 set1) = 0 -> SEED=seed /\ SK=sk) /\
(word.unsigned (word.or set0 set1) <> 0 -> SEED++SK = RupicolaCrypto.Spec.chacha20_block seed (ChaCha20.le_split 4 (word.of_Z 0) ++ firstn 12 garageowner))
)) \/
TracePredicate.concat (lightbulb_spec.lan9250_recv _ incoming)
(lightbulb_spec.lan9250_send _
(let ip_length := 62 in
Expand Down Expand Up @@ -313,7 +314,7 @@ Proof.
autoforward with typeclass_instances in E0.
2: {
fwd; slv; [].
right. left. eexists. ssplit; try eassumption. left.
right. left. ssplit; trivial; []. eexists; split; try eassumption; trivial. left.
rewrite skipn_app, skipn_all2, ?Lpp, ?app_nil_l by ZnWords.
cbn [List.skipn minus firstn List.firstn List.app rev]. ZnWords. }

Expand All @@ -337,7 +338,7 @@ Proof.
destr Z.eqb; rewrite ?word.unsigned_of_Z_0, ?word.unsigned_of_Z_1; intuition try discriminate; autoforward with typeclass_instances in E1.
2: {
fwd; slv; [].
right. left. eexists. ssplit; try eassumption. right. left.
right. left. ssplit; trivial; []. eexists. ssplit; try eassumption. right. left.
rewrite app_nth2 by ZnWords.
rewrite app_comm_cons.
rewrite app_nth2 by SepAutoArray.listZnWords.
Expand All @@ -358,7 +359,7 @@ Proof.
destr Z.eqb; rewrite ?word.unsigned_of_Z_0, ?word.unsigned_of_Z_1; intuition try discriminate; autoforward with typeclass_instances in E3.
2: {
fwd; slv.
right. left. eexists. ssplit; try eassumption. right. right. SepAutoArray.listZnWords. }
right. left. ssplit; trivial; []. eexists. ssplit; try eassumption. right. right. SepAutoArray.listZnWords. }
repeat straightline.
straightline_call; ssplit; try ecancel_assumption; try trivial; try ZnWords.
{ cbv. inversion 1. }
Expand Down Expand Up @@ -533,8 +534,7 @@ Proof.
rewrite !ListUtil.skipn_app_sharp by ZnWords.
eexists _, _; ssplit; try eassumption; subst mmio_val; eauto.

intros; exfalso. apply H39.
rewrite word.unsigned_or_nowrap. apply Z.lor_eq_0_iff; auto.
all : rewrite ?firstn_skipn; intuition auto.
(* end chacha20*) }

Optimize Proof. Optimize Heap.
Expand Down Expand Up @@ -605,7 +605,7 @@ Optimize Proof. Optimize Heap.
rewrite <-Hvv.
rewrite !ListUtil.firstn_app_sharp by ZnWords.
rewrite !ListUtil.skipn_app_sharp by ZnWords.
eexists _, _; ssplit; try eassumption; subst mmio_val; eauto.
eexists _, _; ssplit; try eassumption; subst mmio_val; eauto; congruence.
}

{
Expand Down Expand Up @@ -861,7 +861,7 @@ Optimize Proof. Optimize Heap.
{ eexists; ssplit. eexists _, _; ssplit; slv.
eexists; ssplit. subst a4. subst a. rewrite app_assoc. reflexivity.
eexists; ssplit. eapply Forall2_app; eassumption.
eauto using TracePredicate.any_app_more. }
intuition eauto using TracePredicate.any_app_more. }

ssplit; trivial.
eexists _, _, _; ssplit; slv.
Expand Down Expand Up @@ -913,209 +913,3 @@ Optimize Proof. Optimize Heap.
Unshelve.
all : try SepAutoArray.listZnWords.
Qed.

Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties.
Import bedrock2.Syntax.
Import coqutil.Macros.WithBaseName.

(* these wrappers exist because CompilerInvariant requires execution proofs with arbitrary locals in the starting state, which ProgramLogic does not support *)
Definition init := func! { initfn() } .
Definition loop := func! { loopfn() } .
Definition memconst_pk := memconst garageowner.
Definition ip_checksum := ip_checksum_br2fn.

Definition funcs :=
&[, init; loop;
initfn; loopfn;
memswap; memequal; memconst_pk;
ip_checksum;
ChaCha20.chacha20_block; ChaCha20.quarter;
lan9250_tx ]
++lightbulb.function_impls
++MontgomeryLadder.funcs.


Lemma chacha20_ok: forall functions, ChaCha20.spec_of_chacha20 (&,ChaCha20.chacha20_block::&,ChaCha20.quarter::functions).
intros.
simple eapply ChaCha20.chacha20_block_body_correct.
constructor.
eapply ChaCha20.quarter_body_correct.
constructor.
Qed.

Import SPI.
Lemma link_loopfn : spec_of_loopfn funcs.
Proof.
eapply loopfn_ok; try eapply memswap.memswap_ok; try eapply memequal_ok.
repeat (eapply recvEthernet_ok || eapply lightbulb_handle_ok);
eapply lan9250_readword_ok; eapply spi_xchg_ok;
(eapply spi_write_ok || eapply spi_read_ok).
eapply ip_checksum_br2fn_ok; exact I.
eapply x25519_base_ok; try eapply fe25519_from_word_correct; try eapply link_montladder; try eapply fe25519_to_bytes_correct.
eapply lan9250_tx_ok; try eapply lan9250_writeword_ok; try eapply spi_xchg_ok; (eapply spi_write_ok || eapply spi_read_ok).
eapply x25519_ok; try eapply fe25519_from_bytes_correct; try eapply link_montladder; try eapply fe25519_to_bytes_correct.
eapply chacha20_ok.
Qed. Optimize Heap.

Require compiler.ToplevelLoop.
Definition ml: MemoryLayout.MemoryLayout(word:=Naive.word32) := {|
MemoryLayout.code_start := word.of_Z 0x20400000;
MemoryLayout.code_pastend := word.of_Z 0x21400000;
MemoryLayout.heap_start := word.of_Z 0x80000000;
MemoryLayout.heap_pastend := word.of_Z 0x80002000;
MemoryLayout.stack_start := word.of_Z 0x80002000;
MemoryLayout.stack_pastend := word.of_Z 0x80004000;
|}.

Lemma ml_ok : MemoryLayout.MemoryLayoutOk ml. Proof. split; cbv; trivial; inversion 1. Qed.

Local Instance : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl.
Derive garagedoor_compiler_result SuchThat
(ToplevelLoop.compile_prog (string_keyed_map:[email protected]) MMIO.compile_ext_call ml funcs
= Success garagedoor_compiler_result)
As garagedoor_compiler_result_ok.
Proof.
match goal with x := _ |- _ => cbv delta [x]; clear x end.
vm_compute.
match goal with |- @Success ?A ?x = Success ?e => is_evar e;
exact (@eq_refl (result A) (@Success A x)) end.
Qed. Optimize Heap.

Definition garagedoor_stack_size := snd garagedoor_compiler_result.
Definition garagedoor_finfo := snd (fst garagedoor_compiler_result).
Definition garagedoor_insns := fst (fst garagedoor_compiler_result).
Definition garagedoor_bytes := Pipeline.instrencode garagedoor_insns.
Definition garagedoor_symbols : list byte := Symbols.symbols garagedoor_finfo.

Require Import compiler.CompilerInvariant.
Require Import compiler.NaiveRiscvWordProperties.
Local Existing Instance SortedListString.map.

Lemma compiler_emitted_valid_instructions :
bverify.bvalidInstructions Decode.RV32IM garagedoor_insns = true.
Proof. vm_cast_no_check (eq_refl true). Qed.

Definition good_trace s t s' :=
exists ioh, SPI.mmio_trace_abstraction_relation ioh t /\
(BootSeq +++ stateful garagedoor_iteration s s') ioh.
Import ExprImpEventLoopSpec.
Definition garagedoor_spec : ProgramSpec := {|
datamem_start := MemoryLayout.heap_start ml;
datamem_pastend := MemoryLayout.heap_pastend ml;
goodTrace t := exists s0 s, good_trace s0 t s;
isReady t m := exists s0 s, good_trace s0 t s /\ exists bs R, memrep bs R s m |}.

Lemma good_trace_from_isRead a a0 : isReady garagedoor_spec a a0 ->
isReady garagedoor_spec a a0 /\
ExprImpEventLoopSpec.goodTrace garagedoor_spec a.
Proof.
cbv [isReady goodTrace garagedoor_spec]; intuition eauto.
case H as (?&?&?&?&?&H); eauto.
Qed.

Lemma link_initfn : spec_of_initfn funcs.
Proof.
eapply initfn_ok.
eapply memconst_ok.
eapply lan9250_init_ok;
try (eapply lan9250_wait_for_boot_ok || eapply lan9250_mac_write_ok);
(eapply lan9250_readword_ok || eapply lan9250_writeword_ok);
eapply spi_xchg_ok;
(eapply spi_write_ok || eapply spi_read_ok).
Qed. Optimize Heap.

Import ToplevelLoop GoFlatToRiscv .
Local Notation invariant := (ll_inv compile_ext_call ml garagedoor_spec).
Lemma invariant_proof :
forall initial : MetricRiscvMachine,
getPc (getMachine initial) = MemoryLayout.code_start ml ->
getNextPc (getMachine initial) = word.add (getPc (getMachine initial)) (word.of_Z 4)->
regs_initialized.regs_initialized (getRegs (getMachine initial)) ->
getLog (getMachine initial) = [] ->
(forall a, word.unsigned (MemoryLayout.code_start ml) <= word.unsigned a < word.unsigned (MemoryLayout.code_pastend ml) -> In a (getXAddrs (getMachine initial))) ->
valid_machine initial ->
(imem (MemoryLayout.code_start ml) (MemoryLayout.code_pastend ml) garagedoor_insns *
LowerPipeline.mem_available (MemoryLayout.heap_start ml) (MemoryLayout.heap_pastend ml) *
LowerPipeline.mem_available (MemoryLayout.stack_start ml) (MemoryLayout.stack_pastend ml))%sep (getMem (getMachine initial)) ->

invariant initial /\
(forall st, invariant st -> mcomp_sat (run1 Decode.RV32IM) st invariant /\
exists extend s0 s1, good_trace s0 (extend ++ getLog (getMachine st)) s1).
Proof.
intros.

unshelve epose proof compiler_invariant_proofs _ _ _ _ _ garagedoor_spec as HCI; shelve_unifiable; try exact _.
{ exact (naive_word_riscv_ok 5%nat). }
{ eapply SortedListString.ok. }
{ eapply compile_ext_call_correct. }
{ intros. cbv [compile_ext_call compile_interact]; BreakMatch.break_match; trivial. }
{ exact ml_ok. }
ssplit; intros; ssplit; eapply HCI; eauto; [].

econstructor.
eexists garagedoor_insns.
eexists garagedoor_finfo.
eexists garagedoor_stack_size.
rewrite garagedoor_compiler_result_ok; ssplit; trivial using compiler_emitted_valid_instructions.
2,3:vm_compute; inversion 1.
econstructor (* ProgramSatisfiesSpec *).
1: vm_compute; reflexivity.
1: instantiate (1:=snd init).
3: instantiate (1:=snd loop).
1,3: exact eq_refl.
1,2: cbv [hl_inv]; intros; eapply WeakestPreconditionProperties.sound_cmd.
1,3: eapply Crypto.Util.Bool.Reflect.reflect_bool; vm_compute; reflexivity.

all : repeat straightline; subst args.
{ repeat straightline.
cbv [LowerPipeline.mem_available LowerPipeline.ptsto_bytes] in *.
cbv [datamem_pastend datamem_start garagedoor_spec heap_start heap_pastend ml] in H6.
SeparationLogic.extract_ex1_and_emp_in H6.
change (BinIntDef.Z.of_nat (Datatypes.length anybytes) = 0x2000) in H6_emp0.
Tactics.rapply WeakestPreconditionProperties.Proper_call;
[|eapply link_initfn]; try eassumption.
2: {
rewrite <-(List.firstn_skipn 0x40 anybytes) in H6.
rewrite <-(List.firstn_skipn 0x20 (List.skipn _ anybytes)) in H6.
do 2 seprewrite_in @Array.bytearray_append H6.
rewrite 2firstn_length, skipn_length, 2Nat2Z.inj_min, Nat2Z.inj_sub, H6_emp0 in H6.
split.
{ use_sep_assumption. cancel. cancel_seps_at_indices 0%nat 0%nat; [|ecancel_done].
Morphisms.f_equiv. }
{ rewrite firstn_length, skipn_length. Lia.lia. }
{ Lia.lia. } }
intros ? ? ? ?; repeat straightline; eapply good_trace_from_isRead.
subst a; rewrite app_nil_r.
rewrite <-(List.firstn_skipn 0x20 (List.firstn _ anybytes)) in H11.
rewrite <-(List.firstn_skipn 1520 (skipn 32 (skipn 64 anybytes))) in H11.
do 2 seprewrite_in @Array.bytearray_append H11.
rewrite ?firstn_length, ?skipn_length, ?Nat2Z.inj_min, ?Nat2Z.inj_sub, H6_emp0 in H11.
cbv [isReady garagedoor_spec good_trace]. eexists (_,_), (_,_); fwd. eauto.
{ rewrite <-app_nil_l. eapply TracePredicate.concat_app; eauto. econstructor. }
cbv [memrep]. ssplit.
{ use_sep_assumption. cancel.
cancel_seps_at_indices 0%nat 0%nat; [reflexivity|].
cancel_seps_at_indices 0%nat 0%nat; [reflexivity|].
cancel_seps_at_indices 0%nat 0%nat; [reflexivity|].
ecancel_done. }
all : repeat rewrite ?firstn_length, ?skipn_length; try Lia.lia. }

{ match goal with H : goodTrace _ _ |- _ => clear H end.
cbv [isReady goodTrace good_trace garagedoor_spec] in *; repeat straightline.
DestructHead.destruct_head' state.
Tactics.rapply WeakestPreconditionProperties.Proper_call;
[|eapply link_loopfn]; try eassumption.
intros ? ? ? ?; repeat straightline; eapply good_trace_from_isRead.
eexists; fwd; try eassumption.
cbv [good_trace] in *; repeat straightline.
{ subst a. (eexists; split; [eapply Forall2_app; eauto|]).
eapply stateful_app_r, stateful_singleton; eauto. } }

Unshelve.
all : trivial using SortedListString.ok.
Qed.

(*
Print Assumptions link_loopfn. (* Closed under the global context *)
Print Assumptions invariant_proof. (* propositional_extensionality, functional_extensionality_dep *)
*)
Loading

0 comments on commit 79642ca

Please sign in to comment.