Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

bump bedrock2, use "always" in GarageDoor spec #1846

Merged
merged 1 commit into from
Apr 2, 2024
+54 −35
Merged

bump bedrock2, use "always" in GarageDoor spec #1846

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rupicola
Open in desktop
Submodule rupicola updated 1 files
+1 −1 bedrock2
87 changes: 53 additions & 34 deletions src/Bedrock/End2End/X25519/GarageDoorTop.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,21 +165,23 @@ 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 : state)(t : Semantics.trace)(s' : state) :=
Definition good_transitions (s : state)(t : Semantics.trace)(s' : state) :=
exists ioh, SPI.mmio_trace_abstraction_relation ioh t /\
(BootSeq +++ stateful garagedoor_iteration s s') ioh.
Definition good_trace t := exists s0 s, good_transitions s0 t s.

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 |}.
goodTrace := good_trace;
isReady t m := exists s0 s, good_transitions 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.
cbv [isReady goodTrace garagedoor_spec good_trace]; intuition eauto.
case H as (?&?&?&?&?&H); eauto.
Qed.

Expand All @@ -202,39 +204,31 @@ Proof.
assumption.
Qed. Optimize Heap.

Import Word.Naive.
Import ToplevelLoop GoFlatToRiscv regs_initialized LowerPipeline.
Require Import bedrock2.WordNotations. Local Open Scope word_scope.
Import bedrock2.Map.Separation. Local Open Scope sep_scope.
Require Import bedrock2.ReversedListNotations.
Local Notation run_one_riscv_instr := (mcomp_sat (run1 Decode.RV32IM)).
Local Notation run1 := (mcomp_sat (run1 Decode.RV32IM)).
Local Notation RiscvMachine := MetricRiscvMachine.
Implicit Types mach : RiscvMachine.
Local Coercion word.unsigned : word.rep >-> Z.

Theorem garagedoor_invariant_proof: exists invariant: RiscvMachine -> Prop,
(forall mach,
getPc mach = code_start ml /\
getNextPc mach = getPc mach ^+ /[4] /\
regs_initialized (getRegs mach) /\
getLog mach = [] /\
(forall a, \[code_start ml] <= \[a] < \[code_pastend ml] -> In a (getXAddrs mach)) /\
valid_machine mach /\
(imem (code_start ml) (code_pastend ml) garagedoor_insns ⋆
mem_available (heap_start ml) (heap_pastend ml) ⋆
mem_available (stack_start ml) (stack_pastend ml)) (getMem mach)
-> invariant mach) /\
(forall mach, invariant mach -> run_one_riscv_instr mach invariant) /\
(forall mach, invariant mach -> exists extend s0 s1, good_trace s0 (getLog mach ;++ extend) s1).
Proof.
exists (ll_inv compile_ext_call ml garagedoor_spec).
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; [].
Definition initial_conditions mach :=
mach.(getPc) = code_start ml /\
mach.(getNextPc) = word.add mach.(getPc) (word.of_Z 4) /\
regs_initialized (getRegs mach) /\
mach.(getLog) = [] /\
(forall a : word32, code_start ml <= a < code_pastend ml -> In a (getXAddrs mach)) /\
valid_machine mach /\
(imem (code_start ml) (code_pastend ml) garagedoor_insns ⋆
mem_available (heap_start ml) (heap_pastend ml) ⋆
mem_available (stack_start ml) (stack_pastend ml)) (getMem mach).

clear HCI. destruct H as (? & ? & ? & ? & ? & ? & ?).
Lemma initial_conditions_sufficient mach :
initial_conditions mach ->
CompilerInvariant.initial_conditions compile_ext_call ml garagedoor_spec mach.
Proof.
intros (? & ? & ? & ? & ? & ? & ?).
econstructor.
eexists garagedoor_insns.
eexists garagedoor_finfo.
Expand Down Expand Up @@ -272,7 +266,7 @@ Proof.
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.
cbv [isReady garagedoor_spec good_trace]. eexists (_,_), (_,_); fwd. eauto.
cbv [isReady garagedoor_spec good_trace good_transitions]. eexists (_,_), (_,_); fwd. eauto.
{ rewrite <-app_nil_l. eapply TracePredicate.concat_app; eauto. econstructor. }
cbv [memrep]. ssplit.
{ use_sep_assumption. cancel.
Expand All @@ -289,15 +283,40 @@ Proof.
[|eapply link_loopfn]; try eassumption.
intros ? ? ? ?; repeat straightline; eapply good_trace_from_isRead.
eexists; fwd; try eassumption.
cbv [good_trace] in *; repeat straightline.
cbv [good_trace good_transitions] in *; repeat straightline.
{ subst a. (eexists; split; [eapply Forall2_app; eauto|]).
eapply stateful_app_r, stateful_singleton; eauto. } }
Qed.

Unshelve.
all : trivial using SortedListString.ok.
Theorem garagedoor_invariant_proof: exists invariant: RiscvMachine -> Prop,
(forall mach, initial_conditions mach -> invariant mach) /\
(forall mach, invariant mach -> run1 mach invariant) /\
(forall mach, invariant mach -> exists extend, good_trace (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 _.
{ exact (naive_word_riscv_ok 5%nat). }
{ eapply SortedListString.ok. }
{ eapply @compile_ext_call_correct; try exact _; eapply @SortedListString.ok. }
{ intros. cbv [compile_ext_call compile_interact]; BreakMatch.break_match; trivial. }
{ exact ml_ok. }
ssplit; intros; ssplit; eapply HCI; eauto using initial_conditions_sufficient.
Qed.

Import OmniSmallstepCombinators.

Theorem garagedoor_correct mach : initial_conditions mach ->
always run1 (eventually run1 (fun mach' => good_trace 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.
{ eapply (naive_word_riscv_ok 5%nat). }
{ eapply @SortedListString.ok. }
{ eapply @compile_ext_call_correct; try exact _. eapply @SortedListString.ok. }
Qed.

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