(WIP) mini-compiler in Why3

examples/in_progress/mini-compiler/compiler.mlw

@@ -107,6 +107,7 @@ module Compiler_logic
   ensures { forall p ms. result.pre p ms <-> ibinop_pre p ms}
   ensures { forall p ms ms'. result.post p ms ms' <-> iadd_post p ms ms' }
   ensures { total_correctness result }
+  ensures { result.code.length = 1 }
   = let res = {code = Cons Iadd Nil; pre  = ibinop_pre ; post = iadd_post } in
     assert {
      forall p ms. res.pre p ms ->
@@ -171,4 +172,4 @@ module Compile_aexpr
 end
 
 
-(* *)
\ No newline at end of file
+(* *)

examples/in_progress/mini-compiler/compiler/why3session.xml

@@ -2,67 +2,125 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
-<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
-<prover id="2" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
+<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
+<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
+<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
 <file name="../compiler.mlw" expanded="true">
-<theory name="Compiler_logic" expanded="true">
+<theory name="Compiler_logic">
  <goal name="WP_parameter infix ~" expl="VC for infix ~" sum="fa7d6c44c79cef6a80a978742d2617d6">
- <proof prover="1"><result status="unknown" time="0.06"/></proof>
+ <proof prover="2"><result status="unknown" time="0.06"/></proof>
  <transf name="split_goal_wp">
   <goal name="WP_parameter infix ~.1" expl="1. assertion" sum="f3f108497bbf837fcc75638e1d28d0b9">
-  <proof prover="1"><result status="unknown" time="0.05"/></proof>
-  <proof prover="2"><result status="timeout" time="4.99"/></proof>
+  <proof prover="2"><result status="unknown" time="0.05"/></proof>
+  <proof prover="3"><result status="timeout" time="4.99"/></proof>
   <transf name="split_goal_wp">
    <goal name="WP_parameter infix ~.1.1" expl="1. assertion" sum="d4534d480ad1f98af7e92a760cabdfaa">
-   <proof prover="0"><result status="valid" time="0.08"/></proof>
+   <proof prover="1"><result status="valid" time="0.08"/></proof>
    </goal>
    <goal name="WP_parameter infix ~.1.2" expl="2. assertion" sum="24f9a46939994e9a838c76878d829761">
-   <proof prover="1"><result status="valid" time="0.05"/></proof>
+   <proof prover="2"><result status="valid" time="0.05"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="WP_parameter infix ~.2" expl="2. postcondition" sum="ff9863e72a666be3b0cd345b5409f15a">
-  <proof prover="1"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter infix ~.3" expl="3. postcondition" sum="13ed203bd5092ef08ed16f0014a4fc9b">
-  <proof prover="1"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="WP_parameter prefix !!" expl="VC for prefix !!" sum="2ff861142eda6026ee2412ddd4e7e835">
- <proof prover="1"><result status="valid" time="0.04"/></proof>
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
- <goal name="WP_parameter hoare" expl="VC for hoare" sum="a8c3289f8e0cf02d847a25f040be6688" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <goal name="WP_parameter hoare.1" expl="1. postcondition" sum="a8c3289f8e0cf02d847a25f040be6688" expanded="true">
-  <proof prover="0"><result status="valid" time="0.04"/></proof>
+ <goal name="WP_parameter hoare" expl="VC for hoare" sum="a8c3289f8e0cf02d847a25f040be6688">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter hoare.1" expl="1. postcondition" sum="a8c3289f8e0cf02d847a25f040be6688">
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
  </transf>
  </goal>
- <goal name="WP_parameter iaddf" expl="VC for iaddf" sum="2f5389c5c965c8f99199b178d034b1c8">
+ <goal name="WP_parameter iaddf" expl="VC for iaddf" sum="5bf5f73b1dc21b91892bf2bab7fbd770">
  <transf name="split_goal_wp">
   <goal name="WP_parameter iaddf.1" expl="1. assertion" sum="a13c8410e34d726336936ee0efeb1f81">
   <transf name="split_goal_wp">
    <goal name="WP_parameter iaddf.1.1" expl="1. assertion" sum="8a4df943eeb9ff1be531d26dba251042">
-   <proof prover="1"><result status="valid" time="0.04"/></proof>
+   <proof prover="2"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="WP_parameter iaddf.1.2" expl="2. assertion" sum="f1c5f93fd831ce093a5bb016baf1ccca">
-   <proof prover="1"><result status="valid" time="0.05"/></proof>
+   <proof prover="2"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="WP_parameter iaddf.1.3" expl="3. assertion" sum="6652a495d5e0d3784c38f12481a078f1">
-   <proof prover="1"><result status="valid" time="0.03"/></proof>
+   <proof prover="2"><result status="valid" time="0.03"/></proof>
    </goal>
    <goal name="WP_parameter iaddf.1.4" expl="4. assertion" sum="8455ac7f2f7395ad8f057a4e86d19a07">
-   <proof prover="1"><result status="valid" time="0.04"/></proof>
+   <proof prover="2"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="WP_parameter iaddf.1.5" expl="5. assertion" sum="d06106f33bf8867c806c805438fa3380">
-   <proof prover="1"><result status="valid" time="0.03"/></proof>
+   <proof prover="2"><result status="valid" time="0.03"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="WP_parameter iaddf.2" expl="2. postcondition" sum="5d23745a653c482f1bc074a5700f9f67">
-  <proof prover="1"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="WP_parameter iaddf.3" expl="3. postcondition" sum="bc98183c218a9804142fb1d4a74db26e">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Compile_aexpr" expanded="true">
+ <goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr" sum="50c9bb44bebdab5e0e5583268d099e2e" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="WP_parameter compile_aexpr.1" expl="1. unreachable point" sum="a444d605c7a63c05109fa23897c8e31a" expanded="true">
+  <proof prover="2"><result status="unknown" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.2" expl="2. unreachable point" sum="43006cc60f880717725b0da38cfe6eb1" expanded="true">
+  <proof prover="2"><result status="unknown" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.3" expl="3. precondition" sum="4d3840e6d4629cfe8a76b305aa02c497">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.4" expl="4. variant decrease" sum="a170786f33fb8bdcda7a305066f12a62">
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.5" expl="5. precondition" sum="e78d14f8eb9c6f2441fc60c1b96d10e5">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.6" expl="6. variant decrease" sum="04949c96ae372468948223467cb0f566">
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.7" expl="7. precondition" sum="57498abc24bcfbd2811af59b1bac88f2">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.8" expl="8. precondition" sum="eb6c9e5c57bbdaa9c0ff73151523306c">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.9" expl="9. precondition" sum="7bd16e30fbfa9ed35967e373e5b94708">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.10" expl="10. precondition" sum="81bfb1196c77f355fa986a8ee05e8365">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.11" expl="11. precondition" sum="0be3a356046d9dc7629c7c1c4b32ff41">
+  <proof prover="0" edited="compiler_Compile_aexpr_WP_parameter_compile_aexpr_2.v"><result status="valid" time="3.33"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.12" expl="12. postcondition" sum="c11c12bcaf5a6ad59d82815044f1e625">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.13" expl="13. postcondition" sum="b2402d7e6cd99485c35d684a860173fc">
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.14" expl="14. postcondition" sum="3bf5df7cfd7c50ca642e67b2b568f24d" expanded="true">
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.15" expl="15. unreachable point" sum="7a687df7386cbadc8b6420f46125b053" expanded="true">
+  <proof prover="2"><result status="unknown" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter compile_aexpr.16" expl="16. unreachable point" sum="148162fb1b05bec98f1291ad57dfb3ef" expanded="true">
+  <proof prover="2"><result status="unknown" time="0.03"/></proof>
   </goal>
  </transf>
  </goal>