diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml index 8d3c4353ca..ae0789dbe0 100644 --- a/.github/workflows/coq-windows.yml +++ b/.github/workflows/coq-windows.yml @@ -26,7 +26,7 @@ jobs: env: NJOBS: "2" - COQ_VERSION: "8.18.0" # minimal major version required for bedrock2 components + COQ_VERSION: "8.20.0" COQEXTRAFLAGS: "-async-proofs-j 1" COQCHKEXTRAFLAGS: "" OPAMYES: "true" @@ -43,7 +43,7 @@ jobs: - name: Set up OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.13.1 + ocaml-compiler: 4.14 - run: opam install conf-time conf-gcc - run: opam install 'ocamlfind>=1.9.7' - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }} diff --git a/rupicola b/rupicola index 24f4a75801..041455f8b4 160000 --- a/rupicola +++ b/rupicola @@ -1 +1 @@ -Subproject commit 24f4a758018202de7117b6b4bc1933592c3e947e +Subproject commit 041455f8b498d5e8a956dd86e093604baf352ef8 diff --git a/src/Bedrock/End2End/X25519/GarageDoor.v b/src/Bedrock/End2End/X25519/GarageDoor.v index 7450badbb3..dcff1f91f3 100644 --- a/src/Bedrock/End2End/X25519/GarageDoor.v +++ b/src/Bedrock/End2End/X25519/GarageDoor.v @@ -119,16 +119,9 @@ Definition BootSeq : list OP -> Prop := ||| lan9250_boot_timeout _ ||| (any+++spi_timeout _)). -Import WeakestPrecondition ProgramLogic SeparationLogic. +Import LeakageSemantics LeakageWeakestPrecondition LeakageProgramLogic SeparationLogic. Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*). Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a"). -Global Instance spec_of_initfn : spec_of "initfn" := - fnspec! "initfn" / bs R, - { requires t m := m =* bs $@(word.of_Z PK) * R /\ length bs = 32%nat; - ensures t' m' := m' =* garageowner$@(word.of_Z PK) * R /\ - exists iol, t' = iol ++ t /\ - exists ioh, mmio_trace_abstraction_relation ioh iol /\ - BootSeq ioh }. Ltac fwd := repeat match goal with @@ -138,6 +131,17 @@ Ltac fwd := end; trivial. Ltac slv := try solve [ trivial | ecancel_assumption | SepAutoArray.listZnWords | intuition idtac | reflexivity | eassumption]. +Section WithPickSp. +Context {pick_sp: PickSp}. + +Global Instance spec_of_initfn : spec_of "initfn" := + fnspec! "initfn" / bs R, + { requires k t m := m =* bs $@(word.of_Z PK) * R /\ length bs = 32%nat; + ensures k' t' m' := m' =* garageowner$@(word.of_Z PK) * R /\ + exists iol, t' = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ + BootSeq ioh }. + Local Instance spec_of_memconst_pk : spec_of "memconst_pk" := spec_of_memconst "memconst_pk" garageowner. Local Instance WHY_spec_of_lan9250_init : spec_of "lan9250_init" := spec_of_lan9250_init. Lemma initfn_ok : program_logic_goal_for_function! initfn. @@ -146,13 +150,13 @@ Proof. straightline_call. { ssplit. eassumption. rewrite H2. all : vm_compute; trivial. } repeat straightline. - eapply WeakestPreconditionProperties.interact_nomem; repeat straightline. + eapply LeakageWeakestPreconditionProperties.interact_nomem; repeat straightline. eexists; fwd; slv. { vm_compute. intuition congruence. } - eapply WeakestPreconditionProperties.interact_nomem; repeat straightline. + eapply LeakageWeakestPreconditionProperties.interact_nomem; repeat straightline. eexists; fwd; slv. { vm_compute. intuition congruence. } - eapply WeakestPreconditionProperties.interact_nomem; repeat straightline. + eapply LeakageWeakestPreconditionProperties.interact_nomem; repeat straightline. eexists; fwd; slv. { vm_compute. intuition congruence. } straightline_call; repeat straightline; fwd. @@ -251,8 +255,8 @@ Definition memrep bs R : state -> map.rep(map:=SortedListWord.map _ _) -> Prop : Global Instance spec_of_loopfn : spec_of "loopfn" := fnspec! "loopfn" / seed sk bs R, - { requires t m := memrep bs R (Build_state seed sk) m; - ensures T M := exists SEED SK BS, memrep BS R (Build_state SEED SK) M /\ + { requires k t m := memrep bs R (Build_state seed sk) m; + ensures K T M := exists SEED SK BS, memrep BS R (Build_state SEED SK) M /\ exists iol, T = iol ++ t /\ exists ioh, SPI.mmio_trace_abstraction_relation ioh iol /\ protocol_step (Build_state seed sk) ioh (Build_state SEED SK) }. @@ -272,20 +276,20 @@ Proof. rename H11 into Lseed. rename H12 into Lsk. rename H13 into H11. straightline_call; try ecancel_assumption; trivial; repeat straightline. intuition idtac; repeat straightline; - eexists; split; repeat straightline; split; intros; try contradiction; [|]; repeat straightline. + eexists; eexists; split; repeat straightline; split; intros; try contradiction; [|]; repeat straightline. 2: fwd; slv. pose proof H12 as Hbuf. seprewrite_in @bytearray_index_merge Hbuf. { ZnWords. } - eexists; split; repeat straightline. + eexists; eexists; split; repeat straightline. rewrite word.unsigned_ltu, ?word.unsigned_of_Z_nowrap by ZnWords.ZnWords; destr Z.ltb; rewrite ?word.unsigned_of_Z_0, ?word.unsigned_of_Z_1; intuition try discriminate; autoforward with typeclass_instances in E. 2: { fwd; slv. right. left. fwd; slv; intuition try ZnWords. } repeat straightline. - eapply WeakestPreconditionProperties.dexpr_expr. + eapply LeakageWeakestPreconditionProperties.dexpr_expr. eexists; split; repeat straightline. case (SepAutoArray.list_expose_nth x3 12 ltac:(ZnWords)) as (Hpp&Lpp). @@ -318,7 +322,7 @@ Proof. cbv [word.wrap]; (rewrite_strat (bottomup (terms (Zmod_small)))); try ZnWords.ZnWords. { rewrite Z.lor_comm; reflexivity. } } - eexists; split; repeat straightline. + eexists; eexists; split; repeat straightline. rewrite word.unsigned_ltu, ?word.unsigned_of_Z_nowrap by ZnWords.ZnWords; destr Z.ltb; rewrite ?word.unsigned_of_Z_0, ?word.unsigned_of_Z_1; intuition try discriminate; autoforward with typeclass_instances in E0. @@ -341,7 +345,7 @@ Proof. repeat eplace (word.add (word.add buf _) _) with (word.add buf _) in H12 by (ring_simplify; trivial). repeat straightline. - eexists; split; repeat straightline. + eexists; eexists; split; repeat straightline. subst protocol. pose proof byte.unsigned_range ipproto. rewrite word.unsigned_eqb, ?word.unsigned_and_nowrap, ?word.unsigned_of_Z_nowrap by ZnWords.ZnWords. @@ -358,13 +362,13 @@ Proof. cbn. intro. subst. apply E1. reflexivity. } repeat straightline. - eexists; split; repeat straightline. + eexists; eexists; split; repeat straightline. rewrite word.unsigned_eqb, ?word.unsigned_of_Z_nowrap by ZnWords.ZnWords. destr Z.eqb; rewrite ?word.unsigned_of_Z_0, ?word.unsigned_of_Z_1; intuition try discriminate; autoforward with typeclass_instances in E2. 2: { repeat straightline. - eexists; split; repeat straightline. + eexists; eexists; split; repeat straightline. rewrite word.unsigned_eqb, ?word.unsigned_of_Z_nowrap by ZnWords.ZnWords. destr Z.eqb; rewrite ?word.unsigned_of_Z_0, ?word.unsigned_of_Z_1; intuition try discriminate; autoforward with typeclass_instances in E3. 2: { @@ -411,6 +415,7 @@ Proof. seprewrite_in_by (Array.bytearray_append vv0) H33 SepAutoArray.listZnWords. repeat straightline. + repeat rewrite <- app_assoc in * || cbn [List.app] in *. straightline_call; ssplit. { ecancel_assumption. } { use_sep_assumption. cancel. cancel_seps_at_indices 2%nat 0%nat. @@ -432,13 +437,13 @@ Proof. { ZnWords. } repeat straightline. - eexists. split. repeat straightline. + eexists. eexists. split. repeat straightline. eexists _, _; split; [eapply map.split_empty_r; reflexivity|]. eexists; ssplit; trivial. { cbv. clear. intuition congruence. } repeat straightline. - eexists. split. repeat straightline. + eexists. eexists. split. repeat straightline. eexists _, _; split; [eapply map.split_empty_r; reflexivity|]. eexists; ssplit; trivial. eexists; ssplit; trivial. @@ -446,7 +451,7 @@ Proof. repeat straightline. eapply map.split_empty_r in H38; destruct H38. - eapply map.split_empty_r in H39; destruct H39. + eapply map.split_empty_r in H41; destruct H41. seprewrite_in_by @bytearray_index_merge H33 SepAutoArray.listZnWords. seprewrite_in_by @bytearray_index_merge H33 SepAutoArray.listZnWords. seprewrite_in_by @bytearray_index_merge H33 SepAutoArray.listZnWords. @@ -457,7 +462,7 @@ Proof. change (word.of_Z 134217728) with st in H33. repeat straightline. - eexists; ssplit; repeat straightline. + eexists; eexists; ssplit; repeat straightline. { (* chacha20 *) (* NOTE: viewing the same memory in two different ways, ++ combined and split *) straightline_call; ssplit. @@ -472,15 +477,15 @@ Proof. { SepAutoArray.listZnWords. } repeat straightline. - rewrite <-(List.firstn_skipn 32 x6) in H46. - seprewrite_in_by (Array.bytearray_append (List.firstn 32 x6)) H46 SepAutoArray.listZnWords. + rewrite <-(List.firstn_skipn 32 x6) in H48. + seprewrite_in_by (Array.bytearray_append (List.firstn 32 x6)) H48 SepAutoArray.listZnWords. replace (word.of_Z (BinInt.Z.of_nat (Datatypes.length (List.firstn 32 x6)))) with (word.of_Z 32 : word32) in * by SepAutoArray.listZnWords. ssplit; trivial. eexists _, _, _; ssplit; try ecancel_assumption; try SepAutoArray.listZnWords. eexists; ssplit. - { subst a0 a. change (?x::?y::?t) with ([x;y]++t). rewrite app_assoc. trivial. } + { subst a7 a0. change (?x::?y::?t) with ([x;y]++t). rewrite app_assoc. trivial. } eexists; ssplit. { eapply Forall2_app; try eassumption. eapply Forall2_cons. 2:eapply Forall2_cons. 3:eapply Forall2_nil. @@ -498,7 +503,7 @@ Proof. rewrite <-(firstn_skipn 6 mac) at 1; rewrite <-?app_assoc. eapply (f_equal2 app); [rewrite to_list_from_list; trivial|]. eapply (f_equal2 app); [rewrite to_list_from_list; trivial|]. - change ([?x]++?y::?z) with ([x;y]++z). + change (?x::?y::?z) with ([x;y]++z). eapply (f_equal2 app). { cbv [be2]. progress change 2%nat with (List.length [ethertype_lo; ethertype_hi]). setoid_rewrite split_le_combine; trivial. } @@ -510,7 +515,7 @@ Proof. rewrite split_le_combine, rev_involutive; trivial. rewrite rev_length. SepAutoArray.listZnWords. } eapply (f_equal2 app); [rewrite to_list_from_list; trivial|]. - eapply (f_equal2 app). { f_equal. eapply byte.unsigned_inj. rewrite E1. trivial. } + eapply (f_equal2 cons). { f_equal. eapply byte.unsigned_inj. rewrite E1. trivial. } rewrite <-(firstn_skipn 2 pPP) at 1; rewrite <-?app_assoc. eapply (f_equal2 app). { eplace 2%nat with _ at 2; cycle 1. @@ -553,7 +558,7 @@ Optimize Proof. Optimize Heap. ssplit; trivial. eexists _, _, _; ssplit; try ecancel_assumption; try SepAutoArray.listZnWords. eexists; ssplit. - { subst a. change (?x::?y::?t) with ([x;y]++t). rewrite app_assoc. trivial. } + { subst a0. change (?x::?y::?t) with ([x;y]++t). rewrite app_assoc. trivial. } eexists; ssplit. { eapply Forall2_app; try eassumption. eapply Forall2_cons. 2:eapply Forall2_cons. 3:eapply Forall2_nil. @@ -571,7 +576,7 @@ Optimize Proof. Optimize Heap. rewrite <-(firstn_skipn 6 mac) at 1; rewrite <-?app_assoc. eapply (f_equal2 app); [rewrite to_list_from_list; trivial|]. eapply (f_equal2 app); [rewrite to_list_from_list; trivial|]. - change ([?x]++?y::?z) with ([x;y]++z). + change (?x::?y::?z) with ([x;y]++z). eapply (f_equal2 app). { cbv [be2]. progress change 2%nat with (List.length [ethertype_lo; ethertype_hi]). setoid_rewrite split_le_combine; trivial. } @@ -583,7 +588,7 @@ Optimize Proof. Optimize Heap. rewrite split_le_combine, rev_involutive; trivial. rewrite rev_length. SepAutoArray.listZnWords. } eapply (f_equal2 app); [rewrite to_list_from_list; trivial|]. - eapply (f_equal2 app). { f_equal. eapply byte.unsigned_inj. rewrite E1. trivial. } + eapply (f_equal2 cons). { f_equal. eapply byte.unsigned_inj. rewrite E1. trivial. } rewrite <-(firstn_skipn 2 pPP) at 1; rewrite <-?app_assoc. eapply (f_equal2 app). { eplace 2%nat with _ at 2; cycle 1. @@ -789,24 +794,24 @@ Optimize Proof. Optimize Heap. repeat match goal with x := word.of_Z 0 |- _ => subst x end. repeat match goal with x := word.of_Z 62 |- _ => subst x end. - rewrite !word.unsigned_of_Z_nowrap in H43 by Lia.lia. + rewrite !word.unsigned_of_Z_nowrap in H42 by Lia.lia. progress replace ((ih_const ++ [byte.of_Z 0] ++ [byte.of_Z 62] ++ ip_idff ++ [ipproto] ++ [byte.of_Z 0] ++ [byte.of_Z 0] ++ ip_local) ++ ip_remote)%list with ((ih_const ++ [byte.of_Z 0] ++ [byte.of_Z 62] ++ ip_idff ++ [ipproto]) ++ [byte.of_Z 0] ++ [byte.of_Z 0] ++ ip_local ++ ip_remote)%list in * by (rewrite ?app_assoc; trivial). - seprewrite_in @Array.bytearray_append H43. - seprewrite_in (@Array.bytearray_append _ _ _ _ _ [byte.of_Z 0]) H43. - seprewrite_in (@Array.bytearray_append _ _ _ _ _ [byte.of_Z 0]) H43. - rewrite ?app_length in H43; cbn [length] in H43; rewrite ?LL in H43. - replace (Datatypes.length ip_idff) with 5%nat in H43 by ZnWords. - cbn [plus] in H43. - repeat eplace (word.add (word.add buf _) _) with (word.add buf _) in H43 by (ring_simplify; trivial). + seprewrite_in @Array.bytearray_append H42. + seprewrite_in (@Array.bytearray_append _ _ _ _ _ [byte.of_Z 0]) H42. + seprewrite_in (@Array.bytearray_append _ _ _ _ _ [byte.of_Z 0]) H42. + rewrite ?app_length in H42; cbn [length] in H42; rewrite ?LL in H42. + replace (Datatypes.length ip_idff) with 5%nat in H42 by ZnWords. + cbn [plus] in H42. + repeat eplace (word.add (word.add buf _) _) with (word.add buf _) in H42 by (ring_simplify; trivial). Import symmetry. - seprewrite_in (symmetry! (fun a=>@ptsto_to_array _ _ _ _ _ a (byte.of_Z 0))) H43. - seprewrite_in (symmetry! (fun a=>@ptsto_to_array _ _ _ _ _ a (byte.of_Z 0))) H43. + seprewrite_in (symmetry! (fun a=>@ptsto_to_array _ _ _ _ _ a (byte.of_Z 0))) H42. + seprewrite_in (symmetry! (fun a=>@ptsto_to_array _ _ _ _ _ a (byte.of_Z 0))) H42. repeat straightline. - match goal with H : ?P ?m |- store _ ?m _ _ _ => revert H end. + match goal with H : ?P ?m |- LeakageWeakestPrecondition.store _ ?m _ _ _ => revert H end. repeat match goal with H : sep _ _ _ |- _ => clear H end. repeat straightline. @@ -870,13 +875,13 @@ Optimize Proof. Optimize Heap. repeat straightline. destruct H35; repeat straightline; [intuition idtac | ]. { eexists; ssplit. eexists _, _; ssplit; slv. - eexists; ssplit. subst a4. subst a. rewrite app_assoc. reflexivity. + eexists; ssplit. subst a18. subst a0. rewrite app_assoc. reflexivity. eexists; ssplit. eapply Forall2_app; eassumption. intuition eauto using TracePredicate.any_app_more. } ssplit; trivial. eexists _, _, _; ssplit; slv. - eexists; ssplit. subst a4. subst a. rewrite app_assoc. reflexivity. + eexists; ssplit. subst a18. subst a0. rewrite app_assoc. reflexivity. eexists; ssplit. eapply Forall2_app; eassumption. right. right. @@ -924,3 +929,4 @@ Optimize Proof. Optimize Heap. Unshelve. all : try SepAutoArray.listZnWords. Qed. +End WithPickSp. diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v index ea55a5b933..8fac6e2f15 100644 --- a/src/Bedrock/End2End/X25519/GarageDoorTop.v +++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v @@ -24,13 +24,14 @@ Require Import bedrock2Examples.memswap. Require Import bedrock2Examples.memconst. Require Import Rupicola.Examples.Net.IPChecksum.IPChecksum. Require Import Crypto.Bedrock.End2End.X25519.GarageDoor. +Require Import bedrock2.SemanticsRelations. Import Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20. Local Open Scope string_scope. Import Syntax Syntax.Coercions NotationsCustomEntry. Import ListNotations. Import Coq.Init.Byte. Import coqutil.Macros.WithBaseName. -Import WeakestPrecondition ProgramLogic SeparationLogic. +Import LeakageSemantics LeakageWeakestPrecondition LeakageProgramLogic SeparationLogic. (* these wrappers exist because CompilerInvariant requires execution proofs with arbitrary locals in the starting state, which ProgramLogic does not support *) Definition init := func! { initfn() } . @@ -76,13 +77,14 @@ Qed. Ltac pose_correctness lem := let H := fresh in pose proof (lem (map.of_list funcs)) as H; - unfold program_logic_goal_for in H; + unfold LeakageProgramLogic.program_logic_goal_for, ProgramLogic.program_logic_goal_for in H; repeat lazymatch type of H with | map.get (map.of_list _) _ = Some _ -> _ => specialize (H eq_refl) end. Import SPI. -Lemma link_loopfn : spec_of_loopfn (map.of_list funcs). + +Lemma link_loopfn {pick_sp: PickSp} : spec_of_loopfn (map.of_list funcs). Proof. pose_correctness loopfn_ok. pose_correctness memswap.memswap_ok. @@ -233,7 +235,7 @@ Proof. eauto. Qed. -Lemma link_initfn : spec_of_initfn (map.of_list funcs). +Lemma link_initfn {pick_sp: PickSp} : spec_of_initfn (map.of_list funcs). Proof. pose_correctness initfn_ok. pose_correctness lan9250_init_ok. @@ -271,6 +273,7 @@ Local Coercion word.unsigned : word.rep >-> Z. Definition initial_conditions mach := 0x20400000 = mach.(getPc) /\ [] = mach.(getLog) /\ + Some [] = mach.(getTrace) /\ mach.(getNextPc) = word.add mach.(getPc) (word.of_Z 4) /\ regs_initialized (getRegs mach) /\ (forall a : word32, code_start ml <= a < code_pastend ml -> In a (getXAddrs mach)) /\ @@ -283,7 +286,7 @@ Lemma initial_conditions_sufficient mach : initial_conditions mach -> CompilerInvariant.initial_conditions compile_ext_call ml garagedoor_spec mach. Proof. - intros (? & ? & ? & ? & ? & ? & ?). + intros (? & ? & ? & ? & ? & ? & ? & ?). econstructor. eexists garagedoor_insns. eexists garagedoor_finfo. @@ -295,33 +298,33 @@ Proof. 1: instantiate (1:=snd init). 3: instantiate (1:=snd loop). 1,3: exact eq_refl. - 1,2: cbv [hl_inv]; intros; eapply MetricSemantics.of_metrics_free; eapply WeakestPreconditionProperties.sound_cmd. + 1,2: cbv [hl_inv]; intros; eapply metricleakage_to_leakage_exec; eapply LeakageWeakestPreconditionProperties.sound_cmd. 3: { eapply word.unsigned_inj. rewrite <-H. trivial. } all : repeat straightline; subst args. { 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; + cbv [datamem_pastend datamem_start garagedoor_spec heap_start heap_pastend ml] in H7. + SeparationLogic.extract_ex1_and_emp_in H7. + change (BinIntDef.Z.of_nat (Datatypes.length anybytes) = 0x2000) in H7_emp0. + Tactics.rapply LeakageWeakestPreconditionProperties.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. + rewrite <-(List.firstn_skipn 0x40 anybytes) in H7. + rewrite <-(List.firstn_skipn 0x20 (List.skipn _ anybytes)) in H7. + do 2 seprewrite_in @Array.bytearray_append H7. + rewrite 2firstn_length, skipn_length, 2Nat2Z.inj_min, Nat2Z.inj_sub, H7_emp0 in H7. 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 ? m ? ?; repeat straightline; eapply good_trace_from_isReady. - subst a; rewrite app_nil_r. + intros ? ? m ? ?; repeat straightline; eapply good_trace_from_isReady. + subst a0; rewrite app_nil_r. lazymatch goal with H: sep _ _ m |- _ => rename H into M end. rewrite <-(List.firstn_skipn 0x20 (List.firstn _ anybytes)) in M. rewrite <-(List.firstn_skipn 1520 (skipn 32 (skipn 64 anybytes))) in M. do 2 seprewrite_in @Array.bytearray_append M. - rewrite ?firstn_length, ?skipn_length, ?Nat2Z.inj_min, ?Nat2Z.inj_sub, H6_emp0 in M. + rewrite ?firstn_length, ?skipn_length, ?Nat2Z.inj_min, ?Nat2Z.inj_sub, H7_emp0 in M. cbv [isReady garagedoor_spec protocol_spec io_spec only_mmio_satisfying]. eexists (Build_state _ _), (Build_state _ _); fwd. eauto. { rewrite <-app_nil_l. eapply TracePredicate.concat_app; eauto. econstructor. } @@ -336,13 +339,13 @@ Proof. { match goal with H : goodTrace _ _ |- _ => clear H end. cbv [isReady goodTrace protocol_spec io_spec garagedoor_spec] in *; repeat straightline. DestructHead.destruct_head' state. - Tactics.rapply WeakestPreconditionProperties.Proper_call; + Tactics.rapply LeakageWeakestPreconditionProperties.Proper_call; [|eapply link_loopfn]; try eassumption. intros ? ? ? ?; repeat straightline; eapply good_trace_from_isReady. eexists; fwd; try eassumption. cbv [only_mmio_satisfying protocol_spec io_spec] in *; repeat straightline. try move H6 at bottom. - { subst a. (eexists; split; [eapply Forall2_app; eauto|]). + { subst a0. eexists; split; [eapply Forall2_app; eauto|]. eapply stateful_app_r, stateful_singleton; eauto. } } Qed. @@ -352,7 +355,7 @@ Theorem garagedoor_invariant_proof: exists invariant: RiscvMachine -> Prop, (forall mach, invariant mach -> exists extend, io_spec (getLog mach ;++ extend)). Proof. exists (ll_inv compile_ext_call ml garagedoor_spec). - unshelve epose proof compiler_invariant_proofs _ _ _ _ _ garagedoor_spec as HCI; shelve_unifiable; try exact _. + 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; try exact _; eapply @SortedListString.ok. } @@ -367,7 +370,7 @@ Theorem garagedoor_correct : forall mach : RiscvMachine, initial_conditions mach always run1 (eventually run1 (fun mach' => io_spec mach'.(getLog))) mach. Proof. intros ? H%initial_conditions_sufficient; revert H. - unshelve Tactics.rapply @always_eventually_good_trace; trivial using ml_ok, @Naive.word32_ok. + unshelve Tactics.rapply @always_eventually_good_trace; trivial using ml_ok, @Naive.word32_ok; cycle 1. { eapply (naive_word_riscv_ok 5%nat). } { eapply @SortedListString.ok. } { eapply @compile_ext_call_correct; try exact _. eapply @SortedListString.ok. }