From fd09c489f94df50c6579973e85c205ec07d60187 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 31 Jul 2020 08:16:51 +0200 Subject: Improving Coqdoc on abstractbb --- kvx/abstractbb/SeqSimuTheory.v | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'kvx/abstractbb/SeqSimuTheory.v') diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v index 61f8f2ec..a957c50a 100644 --- a/kvx/abstractbb/SeqSimuTheory.v +++ b/kvx/abstractbb/SeqSimuTheory.v @@ -55,13 +55,14 @@ with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) : end end. -(* the symbolic memory: - - pre: pre-condition expressing that the computation has not yet abort on a None. - - post: the post-condition for each pseudo-register -*) -Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}. - -(** initial symbolic memory *) +(** The (abstract) symbolic memory state *) +Record smem := +{ + pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *) + post:> R.t -> term (**r the output term computed on each pseudo-register *) +}. + +(** Initial symbolic memory state *) Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}. Fixpoint exp_term (e: exp) (d old: smem) : term := @@ -78,11 +79,12 @@ with list_exp_term (le: list_exp) (d old: smem) : list_term := end. -(** assignment of the symbolic memory *) +(** assignment of the symbolic memory state *) Definition smem_set (d:smem) x (t:term) := {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m)); post:=fun y => if R.eq_dec x y then t else d y |}. +(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *) Section SIMU_THEORY. Variable ge: genv. @@ -375,8 +377,7 @@ Qed. End SIMU_THEORY. -(** REMARKS: more abstract formulation of the proof... - but relying on functional_extensionality. +(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom). *) Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)). -- cgit