Commit 3cb17d16 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

mini-compiler: a natural soundness lemma for compile_aexpr (to be proved)

parent 92211e8b
......@@ -338,6 +338,16 @@ module Compile_aexpr
any pos -> post ensures { result = aexpr_post a c.wcode.length }
in hoare pre c post
let compile_aexpr_natural (a: aexpr) : code
ensures { forall c p s m.
codeseq_at c p result ->
transition_star c
(VMS p s m)
(VMS (p + length result) (push (aeval m a) s) m) }
(compile_aexpr a).code
......@@ -52,7 +52,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
<theory name="Builtin_spec" sum="5aa78d7763695c29031c33c97a631785">
<theory name="Builtin_spec" sum="5aa78d7763695c29031c33c97a631785" expanded="true">
<goal name="iconst_post_lemma">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -159,7 +159,7 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
<theory name="Compile_aexpr" sum="cbedbac5d47b6ea1a869223fc9c2cebc" expanded="true">
<theory name="Compile_aexpr" sum="55743cafb73f7aef7a1729d9af24c55e" expanded="true">
<goal name="aexpr_post_lemma">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -364,6 +364,8 @@
<goal name="WP_parameter compile_aexpr_natural" expl="VC for compile_aexpr_natural" expanded="true">
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment