From 103edf0c84dec9b30ea9a938f9287ecb78426aed Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 2 Oct 2018 08:42:00 +0200
Subject: [PATCH] examples for lecture 8, stack machine
---
examples/compiler_noproof.mlw | 168 ++++++++++
examples/compiler_noproof/why3session.xml | 300 ++++++++++++++++++
examples/compiler_noproof/why3session.xml.bak | 298 +++++++++++++++++
examples/compiler_noproof/why3shapes.gz | Bin 0 -> 3541 bytes
examples/compiler_noproof/why3shapes.gz.bak | Bin 0 -> 3541 bytes
examples/imp_per.mlw | 86 +++++
examples/state.mlw | 45 +++
examples/vm_ind.mlw | 110 +++++++
examples/vm_mem.mlw | 103 ++++++
examples/vm_mem/why3session.xml | 28 ++
examples/vm_mem/why3session.xml.bak | 26 ++
examples/vm_mem/why3shapes.gz | Bin 0 -> 218 bytes
examples/vm_mem/why3shapes.gz.bak | Bin 0 -> 218 bytes
examples/vm_per.mlw | 254 +++++++++++++++
examples/vm_simple.mlw | 95 ++++++
examples/vm_simple/why3session.xml | 132 ++++++++
examples/vm_simple/why3session.xml.bak | 36 +++
examples/vm_simple/why3shapes.gz | Bin 0 -> 1143 bytes
examples/vm_simple/why3shapes.gz.bak | Bin 0 -> 322 bytes
19 files changed, 1681 insertions(+)
create mode 100644 examples/compiler_noproof.mlw
create mode 100644 examples/compiler_noproof/why3session.xml
create mode 100644 examples/compiler_noproof/why3session.xml.bak
create mode 100644 examples/compiler_noproof/why3shapes.gz
create mode 100644 examples/compiler_noproof/why3shapes.gz.bak
create mode 100644 examples/imp_per.mlw
create mode 100644 examples/state.mlw
create mode 100644 examples/vm_ind.mlw
create mode 100644 examples/vm_mem.mlw
create mode 100644 examples/vm_mem/why3session.xml
create mode 100644 examples/vm_mem/why3session.xml.bak
create mode 100644 examples/vm_mem/why3shapes.gz
create mode 100644 examples/vm_mem/why3shapes.gz.bak
create mode 100644 examples/vm_per.mlw
create mode 100644 examples/vm_simple.mlw
create mode 100644 examples/vm_simple/why3session.xml
create mode 100644 examples/vm_simple/why3session.xml.bak
create mode 100644 examples/vm_simple/why3shapes.gz
create mode 100644 examples/vm_simple/why3shapes.gz.bak
diff --git a/examples/compiler_noproof.mlw b/examples/compiler_noproof.mlw
new file mode 100644
index 0000000..cdf47dc
--- /dev/null
+++ b/examples/compiler_noproof.mlw
@@ -0,0 +1,168 @@
+
+
+(*Imp to Vm compiler *)
+(**************************************************************************)
+
+(* Compiler for arithmetic expressions *)
+module Compile_aexpr
+
+ use int.Int
+ use list.List
+ use list.Length
+ use list.Append
+ use imp_per.Imp
+ use vm_per.Vm
+ use state.State
+
+ function compile_aexpr (a:aexpr) : code =
+ match a with
+ | Anum n -> iconst n
+ | Avar x -> ivar x
+ | Aadd a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++ iadd
+ | Asub a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++ isub
+ end
+
+ goal g_2_1 : (* 2 + 1 *)
+ let c_imp = Aadd (Anum 2) (Anum 1) in
+ let c_out = compile_aexpr c_imp in
+ c_out = iconst 2 ++ iconst 1 ++ iadd
+
+ goal g_a_1 : (* a + 1 *)
+ let c_imp = Aadd (Avar (Id 1)) (Anum 1) in
+ let c_out = compile_aexpr c_imp in
+ c_out = ivar (Id 1) ++ iconst 1 ++ iadd
+
+end
+
+
+(* Compiler for boolean expressions. *)
+module Compile_bexpr
+
+ use int.Int
+ use list.List
+ use list.Length
+ use list.Append
+ use imp_per.Imp
+ use vm_per.Vm
+ use state.State
+ use Compile_aexpr
+
+ function compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) : code =
+ match b with
+ | Btrue -> if cond then ibranch ofs else Nil
+ | Bfalse -> if cond then Nil else ibranch ofs
+ | Bnot b1 -> compile_bexpr b1 (not cond) ofs
+ | Band b1 b2 ->
+ let c2 = compile_bexpr b2 cond ofs in
+ let ofs = if cond then length c2 else ofs + length c2 in
+ compile_bexpr b1 false ofs ++ c2
+
+ | Beq a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++
+ if cond then ibeq ofs else ibne ofs
+ | Ble a1 a2 -> compile_aexpr a1 ++ compile_aexpr a2 ++
+ if cond then ible ofs else ibgt ofs
+ end
+end
+
+module Compile_com
+
+ use int.Int
+ use list.List
+ use list.Length
+ use list.Append
+ use imp_per.Imp
+ use vm_per.Vm
+ use state.State
+ use Compile_aexpr
+ use Compile_bexpr
+
+ function compile_com (cmd: com) : code =
+ match cmd with
+ | Cskip -> Nil
+ | Cassign x a -> compile_aexpr a ++ isetvar x
+ | Cseq cmd1 cmd2 -> compile_com cmd1 ++ compile_com cmd2
+ | Cif bexpr cmd1 cmd2 ->
+ let code_false = compile_com cmd2 in
+ let code_true = compile_com cmd1 ++ ibranch (length code_false) in
+ compile_bexpr bexpr false (length code_true) ++
+ code_true ++
+ code_false
+ | Cwhile test body ->
+ let code_body = compile_com body in
+ let body_length = length code_body + 1 in
+ let code_test = compile_bexpr test false body_length in
+ let ofs = length code_test + body_length in
+ code_test ++ code_body ++ ibranch (- ofs)
+ end
+
+ function compile_program (prog : com) : code =
+ compile_com prog ++ ihalt
+
+ goal g1 : (* a := 2 + 1 *)
+ let c_in = Cassign (Id 1) (Aadd (Anum 2) (Anum 1)) in
+ let c_out =
+ iconst 2 ++
+ iconst 1 ++
+ iadd ++
+ isetvar (Id 1) ++
+ ihalt in
+ compile_program c_in = c_out
+
+ goal g2 : (* IF TRUE THEN a := 1 ELSE a := 2 END *)
+ let c_in = Cif Btrue (Cassign (Id 1) (Anum 1)) (Cassign (Id 1) (Anum 2)) in
+ let c_out =
+ (* <-- condition trivial true *)
+ iconst 1 ++ (* <-- then branch *)
+ isetvar (Id 1) ++
+ ibranch 2 ++
+ iconst 2 ++ (* <-- else branch *)
+ isetvar (Id 1) ++
+ ihalt
+ in
+ compile_program c_in = c_out
+
+ goal g3 : (* IF NOT TRUE THEN a := 1 ELSE a := 2 END *)
+ let c_in = Cif (Bnot Btrue) (Cassign (Id 1) (Anum 1)) (Cassign (Id 1) (Anum 2)) in
+ let c_out =
+ ibranch 3 ++ (* <-- condition trivial false *)
+ iconst 1 ++ (* <-- then branch *)
+ isetvar (Id 1) ++
+ ibranch 2 ++
+ iconst 2 ++ (* <-- else branch *)
+ isetvar (Id 1) ++
+ ihalt
+ in
+ compile_program c_in = c_out
+
+ goal g4 : (* IF a <= 0 THEN a := 1 ELSE a := 2 END *)
+ let c_in = Cif (Ble (Avar (Id 1)) (Anum 0)) (Cassign (Id 1) (Anum 1)) (Cassign (Id 1) (Anum 2)) in
+ let c_out =
+ ivar (Id 1) ++ (* <-- a <= 0 condition *)
+ iconst 0 ++
+ ibgt 3 ++
+ iconst 1 ++ (* <-- then branch *)
+ isetvar (Id 1) ++
+ ibranch 2 ++
+ iconst 2 ++ (* <-- else branch *)
+ isetvar (Id 1) ++
+ ihalt
+ in
+ compile_program c_in = c_out
+
+ (* simple sum program : *)
+ goal g5 : (* X := 1; WHILE NOT (Y <= 0) DO X := X + Y; Y := Y - 1 DONE *)
+ let x = Id 0 in
+ let y = Id 1 in
+ let cond = Bnot (Ble (Avar y) (Anum 0)) in
+ let body1 = Cassign x (Aadd (Avar x) (Avar y)) in
+ let body2 = Cassign y (Asub (Avar y) (Anum 1)) in
+ let lp = Cwhile cond (Cseq body1 body2) in
+ let code = Cseq (Cassign x (Anum 1)) lp in
+
+ let c_out =
+ (* your code here *)
+ ihalt in
+ compile_program code = c_out
+
+end
+
diff --git a/examples/compiler_noproof/why3session.xml b/examples/compiler_noproof/why3session.xml
new file mode 100644
index 0000000..a96c43a
--- /dev/null
+++ b/examples/compiler_noproof/why3session.xml
@@ -0,0 +1,300 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../imp_per.mlw" proved="true">
+<theory name="Imp" proved="true">
+ <goal name="ceval_deterministic_aux" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="42"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="79"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.2.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.2" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.3" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.3.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.3" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.4" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.4.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.4" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="47"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.6.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.6" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../compiler_noproof.mlw">
+<theory name="Compile_aexpr" proved="true">
+ <goal name="g_2_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g_a_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+</theory>
+<theory name="Compile_com">
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g4" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="g4.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g5">
+ <proof prover="2"><result status="timeout" time="1.00"/></proof>
+ <proof prover="3"><result status="timeout" time="1.00"/></proof>
+ <transf name="compute_in_goal" >
+ <goal name="g5.0">
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+<file name="../vm_per.mlw" proved="true">
+<theory name="ReflTransClosure" proved="true">
+ <goal name="transition_star_one" proved="true">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="transition_star_transitive" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="transition_star_transitive.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="transition_star_transitive.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Vm" proved="true">
+ <goal name="codeseq_at_app_right" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="codeseq_at_app_left" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="59"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="2"><result status="valid" time="0.13"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="27"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="90"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_3.0" proved="true">
+ <proof prover="0"><result status="valid" time="2.72"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="56"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="155"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.04" steps="68"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="183"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="193"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test2" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="110"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="263"/></proof>
+ </goal>
+ <goal name="cs_4" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="62"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.06" steps="187"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="74"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.09" steps="215"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="77"/></proof>
+ </goal>
+ <goal name="g4_trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.24"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="2"><result status="valid" time="0.21"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test3" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/compiler_noproof/why3session.xml.bak b/examples/compiler_noproof/why3session.xml.bak
new file mode 100644
index 0000000..36d5bc9
--- /dev/null
+++ b/examples/compiler_noproof/why3session.xml.bak
@@ -0,0 +1,298 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../imp_per.mlw" proved="true">
+<theory name="Imp" proved="true">
+ <goal name="ceval_deterministic_aux" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="42"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="79"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.2.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.2" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.2.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.3" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.3.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.3" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.3.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.4" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.4.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.4" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.4.6" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic_aux.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="47"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="ceval_deterministic_aux.6.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.2" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.3" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.4" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.5" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="ceval_deterministic_aux.6.6" proved="true">
+ <proof prover="2"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../compiler_noproof.mlw">
+<theory name="Compile_aexpr" proved="true">
+ <goal name="g_2_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+ <goal name="g_a_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+</theory>
+<theory name="Compile_com">
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ <goal name="g4" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="g4.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g5">
+ <proof prover="2"><result status="timeout" time="1.00"/></proof>
+ <proof prover="3"><result status="timeout" time="1.00"/></proof>
+ <transf name="compute_in_goal" >
+ <goal name="g5.0">
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+<file name="../vm_per.mlw" proved="true">
+<theory name="ReflTransClosure" proved="true">
+ <goal name="transition_star_one" proved="true">
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="transition_star_transitive" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="transition_star_transitive.0" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="transition_star_transitive.1" proved="true">
+ <proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Vm" proved="true">
+ <goal name="codeseq_at_app_right" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="codeseq_at_app_left" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="59"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="2"><result status="valid" time="0.13"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="27"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="90"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_3.0" proved="true">
+ <proof prover="0"><result status="valid" time="2.72"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="56"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="155"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.04" steps="68"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="183"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.07" steps="193"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test2" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="110"/></proof>
+ </goal>
+ <goal name="cs_3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="263"/></proof>
+ </goal>
+ <goal name="cs_4" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="3"><result status="valid" time="0.03" steps="62"/></proof>
+ </goal>
+ <goal name="g2_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.06" steps="187"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="74"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="3"><result status="valid" time="0.09" steps="215"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="3"><result status="valid" time="0.05" steps="77"/></proof>
+ </goal>
+ <goal name="g4_trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.24"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="2"><result status="valid" time="0.21"/></proof>
+ </goal>
+</theory>
+<theory name="Vm_test3" proved="true">
+ <goal name="cs_0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ <goal name="cs_0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="cs_1" proved="true">
+ <proof prover="3"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="cs_2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/compiler_noproof/why3shapes.gz b/examples/compiler_noproof/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..897e5bf6906611286c7048c79c74f76b21d628e6
GIT binary patch
literal 3541
zcmb2|=3oGW|8HZw^JR7l?t2~n#+D->RHZv*f{Y9^6OYACl^Naw60VzeXdjs->%IHt
zpWh+<&o0VrT_TxTCTneZ;~o3Sq}s2)R_#8n%6hPiFNU>aCF}KS;lwMCR%q9$hhP8u
z>iPSB8x~EiRt~M7^j$mV;HlVi=U;qcQfBe$@$|~rJ9%wz=)teAA{u|ysc!#tduPh#
zy=%9KGyN8xa^3v@j$dEW%mnrH^^-m|CcS%LqV`V6YxPD`o~^21Qq?rpRA`^LoidN}
zQ?a98-08DtuYSLNx$fKa=9(S9Dy{z9eqaClyQk;GuTdMEZnrJro7p6^Wlj*sQGq2d
zHi(@QslJh~yzWw&bWXL`=G+fm&pyT7e__A;>HRa$&OLODQG8p_9=h%F&)gX~TWn8%
zE-g6p^J?0%*#YzKa%<mVY^`f8tM8i{JL~PGcZUqFzrD6}YkbTOp-K5sXH*&mqkUWC
zM3Q@^u5RAh_^EEC$#fy{4IYy%pEI*PKaqC-=CZ>ab0o{&@3T;B&11R7Yw^h7d*X|V
z*23+15sSt3*()*_gxYp~U+|f6*X3tkIa^)W4X3Y~l6CyWZtg-p*+&~5&z!S|VP5Zp
z#3RQZU)DO8C=oL+JoE9VJzf0`*<S6k9C^HDJ7jE*^)8cmX2+8km3VKh^!0@2KX(-}
zOlL2+Tw8GQl90)J9V_l#SE2>pFEDv!SfZo6<8fc+fegmjSxJ8iIQVbODl<sv__JZL
z&Pj<yM;p2q%OCQ)pOeX)C@_^h<JqEVN@v@aFh2k3_gU+`N~FiSPtARfY<KitafGMD
zS@l~<E$VC2y`UWEKFzE=(7kPr>Wa!M7a7!e1Kqg;#k<o>^}I5~G7p?FRQHHnzAMP7
zZf5caizln3vnn_A?{uqKnEv5`WaWpR9hax8U%zp8@}`|Lo~)l=f2IAg_3YfT!Wq{J
z&A&g<yvCM)F!9~tw34*hb0st1Dz?8fw&3O|et&)LjfK;n6y<f^`065d+iv>}qtZWI
zXFEPDkky@g+`Rr@nC{62TT^z^?R>138<J07+qr8>(#pTCsRn$?|Gpl+T0M7y^ofR>
z9|dB(oBSJoPn~jb)wDNC*DfeGbY00gvuGj9%ZsbOY;HR#yXX5OmAwXjk1SFGyKa^&
zubR_8^Y$;xr4!lTu+RKiH{o9Q#XmcwYjs^O8*h1_=;AxC+V|edZF8#2*0Qhrc;a8W
zU+}fasqcOr{+nX6l5y7B>FpJpXIhIUFg?Fu6x_Uh+Zk5z2?=l4ER}gDrK$4OFnH4k
zg%?3`ISFZp9#1k-FEeO<=3j1Lz)(0LyYH%PO1#W+9u3|-OIc5xRTdXj+tl5^<eudh
z?_2YCvL3u#q|Z~aqww9v7a^~v${y=-;??}>z~Si`k)6-c|HMzCB&O*(kL{6|j(Cxx
zeQHU1*%xoeUvPbp$yqpW72Emc!Z!D_{f=&$F6xr9?AStc2IZ+2cQwAa!=3xP=wC%o
z;rYAl4>I2re&|#@@#$lmf~zAd+tFFU&TK2UUWswu%66}P{RM&a#82^u#BOb|+_Fc0
z$Mh4uy(Ve$LOT-7ir%I^eK05FkN1@33zM=k&;Hh1`21cJPh6J9MbGEVC2?<7o_~1h
z_>Ncl?#uc$1)ry1j$c$^;Ii0#-%pty?WomWC#%B5tunk4{do4tNPl~LW@gs2Pv4tz
zmPxbEcQMwsc-SBjW2hUvsi{-)$La-#lT&2Z*CcU2TcG-MTK23%QJfbmlaE}pT`sP6
z;J=jJo8vp(4-3cSsG81*`=K!TSldNIi=s%a)5+(r{P*vu*L8Z+zVo>BcC+vx5pky#
zjx(!1pY@PvIz8=8(NC_<8{%n4>Sk2$QSJK9FtbLK#WDWiOjDtfQWlXPXIviFw+Pu^
zmpB;RJZWj<$I}uETMkWHkfHYEl~ld*oF6+?9h09b8LkTORSo3V+?v#*F~Q+P|K7Hr
z_L~2G?w=%Lzr8^s`ioPnOhBGb&(y0+UvNbP%OBb}|J9kK6S;|U_r9#TYJI0obK^}m
zmqxW?(ayS2Cw?aI>SQjC^KiMd`NYq=W_&j+=N>tiUiI`SYcA)l#@@|}hqJqu+uxT=
ze*EC_eCF(X#>;LmxZ$M9u`wZMBm4WwZeL}ZZWOBVx^H9T&YE|F{X%B#feDS%6PG0?
z)cp#cuee^OPOU`eOz7l|Yx`F1-6mDrae&vQ`+S*7RY_@N(3d^3>~q87+QeH=|NeYj
z;?c|R3zH|=RZOp1qj;jbUFxFaa*Nv5shd}9wVtzfFaO(?YiT#1p1XTn$MfgWS+i9W
z&%e)mvE`9T{o|c77fXCx<UhKV#Idz^EDKhe<+asFc&A^#zpGXR_tHBH*)x0nDl)gc
z@kmd9e|lcYJGU;s$M1e@VSbj}^Y6=YEdz_&KW3i3=(fF1l0(8eG1;Z3?$wPAUc4u_
zHmg0%HvAP?wJrblJGZ=vT4H*p;@T3uXYVChf4>-dzrQ|iN6fzSH)ZQ?KaDOv8Y5ZL
z|5{Guf`omvxK^-dyYM|FInjpn7tYg_KZIwyO!xlv)B0lm?i<d&mzzIah<X+!RIdE_
zB*)@5y`w*Wec;dHtMd=;*3U6r>=SbE>$$CBTKkHevnHnPKXdTx#r!&B>lO0r^YgTG
z`Ez;-d$$MK*ZoL&u}Apt&&$t6_e>2hi;Ro?|Ks4Xb^i}?dxuUjDc@K!HKr$Uj@a9~
zi`|}Ys(1S2|0(j`7SBh4i^>n1UkYBS)w^<qW?qP<`=^B~#3t%_{XXu#o7KMd-;clP
zKMiV^e=o~)c5hM+H?P`#{}2DCf8XA2bH4TFgI$=TX{xVj#@U1iEgF$k4l~W-)A`fl
zH{5Q{eSFaEbo$P9_HVW>Om$ti>(9q)F<%^(Zk6J`{^F34s&?r+mlJWC37=h+lN1id
z-Hi;rEt|8YF#W=}Uyt8*YPpM)>@9mL!sRseCG+u@p6l5^?7SB5_H?;3htK=>`RAEV
zRon7dT1d&wmHU>!awwtJFvD+Jr;^K+TR}7be)5aEZT94>-?_Ul!=~@vY~A{-eB0w^
z(f51qzA~5h``*6)Ud*g7Q|;sT#{ZwGw>F{u9Tz|QTJ|+%?ePis*{ydeEV{O)`N7Nf
z775S2pA#h2zRB%2`M*J4O0$0V=I_1#iobWTo3+KZZokdtS<WxJCg9ztIgOuRJv+Xs
zY~s~x;`h#p-+cDwWrgjFw`v#6`nJwZ{aJe{=dXFp6P3=S&V#2qn5xBXR(h9Ra{f4%
z-}bp;!b1)2z2+;9HS(XCJ;l=VNS=G!MZK8$8~)|@>b|ed{;+H2$)f^?-kp7RZ|8-q
zmU{v#n|D16+Hzyp)~9*v^48nM?ccp~E>D8bL5_3(KHZ&qy1S)w!=jzsQ73zXWv}a8
z>&tL@`10V@OF{3>9!ibc*Hg~Yy6AJ*TaKdePqLf0#cjwoUc|LQMXkqLPUPmKu7}cd
z3@%)px_{4}JuhaO{?0liEP1^tPWAW{<;B?>mu*n7n5R`yW4ohHv9P|%s`Tm>uE(p^
zzw<3GfA5r*Hg`sj!QQ!>Wg2!~KXmosm#wTO*XJG$d=L`#^V}xKVD6XYMZ5hgj``ew
z{q_5H`#ZVWc1QBwZhmxY$t#1-!*7hY1>E{_CRnh>^xyKtU!RKR*a<##7vGZf>gKAW
zUv^E|)S$ic)}@4ZZ(Sd4NL?8`_x7<1tmSTHswFG-w))*m|N3Ih=5?IAyboVdb}Ey9
zeS5}k`B$&+yiUqrcO{JBjsJqo=%dBGmc_H`_S)oB`WNe;QP>wDnUd^z`S!1KimQ{>
z%I^45v_fZX<nz{*qGz+EMM|gLsy%nib`xg_Z%@<J=E!$?yQ6jUv?Mu~U3@kBqu7hK
z4Illyru>n7P}pv%wP1VF{K-dSN{-GsvP)*eevRm+R{_r&)kDMTe|0;WKi$Q@!S3cZ
z?)|@Gm!AFFeJW;eV4d?#A<hWP1v!Peal#V?3KGw@re3?ASzqfZ<lQQfBxZPrVT0S@
zf>kRH^hCU0-m5A)Z&KpDC?*RJQGuAH8Dg(5ojstIq%`6Cmdcu=Uj?@Bf46N?mtbL0
zpUygk-EPM&sWzTIxl)MT#%uP{*4JM+oxg?6aMm=lDcS5ZWkH(C@+5=5Umo6FTlcS^
zRCjyT=XbZRUFV;l_dk~@Co+1WVTFnFwR2q8{vOLJO!$|yAbR$d4-*%NCoLD<bdr<z
z%B;A+WM1JiP4i37tH18Exg413VEE*ns`={&yur>hl(|zrCVZ`_D*YQEbzs_V(?2t-
zPu+`Bwa)Ha)%GZ7>6B@g86s9YCY{UQ<G-@x)a(C!i&ZD8Y08}|DsJ-+>n`Tm7JPdB
zzEoYY5ZjYij+=;Yyl^mQzo*jHU{UetkgV7n%4XZnyiq@s-F2QTV`Xsr1I_Ye=?gvF
zPx``Eaha6f{QjA><n-AWDbEu4l2-;BiW%muJiB$;p)Z-wPBZWF-_OIpb+)Klnd5~s
zjl8+un~$w!ny<g$XzPi!$(u@E#d@!a>U?uTJ$r|9Wtqcd%g|L}h0>;H!#o2g9XuR1
zX=gz*tEkwt$oTK&>c6)izTA6~arN#4d7PcT0hwV7ET2Wxd|Id+!E==L+RiQikF!|t
z=B!jn3hK_<e~vT2a`B2%&&iwlIx{EtO`D!H%W2E+CC4IlZ5F4l?$DVPyJ_9Gy0%*d
zm3ugx#3moJYo3w3d&cVUfQ_+|YbKp`YP)qV_DsO{O&9XMOli%Unw7XxH*~AdrJfII
z4_Xc~o#MKoXgMQwVb;~kUm9l(jN5YdwFXyB%vpMl=MsPD5??oiNz=MQ?_by;?p?fb
zYR<~pMI9<ZmxCn}#VxwR9B=q9ie?ut(mLjIz;JiQYuP}zf6Tj;qtDOwU|;|MeEAUV
literal 0
HcmV?d00001
diff --git a/examples/compiler_noproof/why3shapes.gz.bak b/examples/compiler_noproof/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..897e5bf6906611286c7048c79c74f76b21d628e6
GIT binary patch
literal 3541
zcmb2|=3oGW|8HZw^JR7l?t2~n#+D->RHZv*f{Y9^6OYACl^Naw60VzeXdjs->%IHt
zpWh+<&o0VrT_TxTCTneZ;~o3Sq}s2)R_#8n%6hPiFNU>aCF}KS;lwMCR%q9$hhP8u
z>iPSB8x~EiRt~M7^j$mV;HlVi=U;qcQfBe$@$|~rJ9%wz=)teAA{u|ysc!#tduPh#
zy=%9KGyN8xa^3v@j$dEW%mnrH^^-m|CcS%LqV`V6YxPD`o~^21Qq?rpRA`^LoidN}
zQ?a98-08DtuYSLNx$fKa=9(S9Dy{z9eqaClyQk;GuTdMEZnrJro7p6^Wlj*sQGq2d
zHi(@QslJh~yzWw&bWXL`=G+fm&pyT7e__A;>HRa$&OLODQG8p_9=h%F&)gX~TWn8%
zE-g6p^J?0%*#YzKa%<mVY^`f8tM8i{JL~PGcZUqFzrD6}YkbTOp-K5sXH*&mqkUWC
zM3Q@^u5RAh_^EEC$#fy{4IYy%pEI*PKaqC-=CZ>ab0o{&@3T;B&11R7Yw^h7d*X|V
z*23+15sSt3*()*_gxYp~U+|f6*X3tkIa^)W4X3Y~l6CyWZtg-p*+&~5&z!S|VP5Zp
z#3RQZU)DO8C=oL+JoE9VJzf0`*<S6k9C^HDJ7jE*^)8cmX2+8km3VKh^!0@2KX(-}
zOlL2+Tw8GQl90)J9V_l#SE2>pFEDv!SfZo6<8fc+fegmjSxJ8iIQVbODl<sv__JZL
z&Pj<yM;p2q%OCQ)pOeX)C@_^h<JqEVN@v@aFh2k3_gU+`N~FiSPtARfY<KitafGMD
zS@l~<E$VC2y`UWEKFzE=(7kPr>Wa!M7a7!e1Kqg;#k<o>^}I5~G7p?FRQHHnzAMP7
zZf5caizln3vnn_A?{uqKnEv5`WaWpR9hax8U%zp8@}`|Lo~)l=f2IAg_3YfT!Wq{J
z&A&g<yvCM)F!9~tw34*hb0st1Dz?8fw&3O|et&)LjfK;n6y<f^`065d+iv>}qtZWI
zXFEPDkky@g+`Rr@nC{62TT^z^?R>138<J07+qr8>(#pTCsRn$?|Gpl+T0M7y^ofR>
z9|dB(oBSJoPn~jb)wDNC*DfeGbY00gvuGj9%ZsbOY;HR#yXX5OmAwXjk1SFGyKa^&
zubR_8^Y$;xr4!lTu+RKiH{o9Q#XmcwYjs^O8*h1_=;AxC+V|edZF8#2*0Qhrc;a8W
zU+}fasqcOr{+nX6l5y7B>FpJpXIhIUFg?Fu6x_Uh+Zk5z2?=l4ER}gDrK$4OFnH4k
zg%?3`ISFZp9#1k-FEeO<=3j1Lz)(0LyYH%PO1#W+9u3|-OIc5xRTdXj+tl5^<eudh
z?_2YCvL3u#q|Z~aqww9v7a^~v${y=-;??}>z~Si`k)6-c|HMzCB&O*(kL{6|j(Cxx
zeQHU1*%xoeUvPbp$yqpW72Emc!Z!D_{f=&$F6xr9?AStc2IZ+2cQwAa!=3xP=wC%o
z;rYAl4>I2re&|#@@#$lmf~zAd+tFFU&TK2UUWswu%66}P{RM&a#82^u#BOb|+_Fc0
z$Mh4uy(Ve$LOT-7ir%I^eK05FkN1@33zM=k&;Hh1`21cJPh6J9MbGEVC2?<7o_~1h
z_>Ncl?#uc$1)ry1j$c$^;Ii0#-%pty?WomWC#%B5tunk4{do4tNPl~LW@gs2Pv4tz
zmPxbEcQMwsc-SBjW2hUvsi{-)$La-#lT&2Z*CcU2TcG-MTK23%QJfbmlaE}pT`sP6
z;J=jJo8vp(4-3cSsG81*`=K!TSldNIi=s%a)5+(r{P*vu*L8Z+zVo>BcC+vx5pky#
zjx(!1pY@PvIz8=8(NC_<8{%n4>Sk2$QSJK9FtbLK#WDWiOjDtfQWlXPXIviFw+Pu^
zmpB;RJZWj<$I}uETMkWHkfHYEl~ld*oF6+?9h09b8LkTORSo3V+?v#*F~Q+P|K7Hr
z_L~2G?w=%Lzr8^s`ioPnOhBGb&(y0+UvNbP%OBb}|J9kK6S;|U_r9#TYJI0obK^}m
zmqxW?(ayS2Cw?aI>SQjC^KiMd`NYq=W_&j+=N>tiUiI`SYcA)l#@@|}hqJqu+uxT=
ze*EC_eCF(X#>;LmxZ$M9u`wZMBm4WwZeL}ZZWOBVx^H9T&YE|F{X%B#feDS%6PG0?
z)cp#cuee^OPOU`eOz7l|Yx`F1-6mDrae&vQ`+S*7RY_@N(3d^3>~q87+QeH=|NeYj
z;?c|R3zH|=RZOp1qj;jbUFxFaa*Nv5shd}9wVtzfFaO(?YiT#1p1XTn$MfgWS+i9W
z&%e)mvE`9T{o|c77fXCx<UhKV#Idz^EDKhe<+asFc&A^#zpGXR_tHBH*)x0nDl)gc
z@kmd9e|lcYJGU;s$M1e@VSbj}^Y6=YEdz_&KW3i3=(fF1l0(8eG1;Z3?$wPAUc4u_
zHmg0%HvAP?wJrblJGZ=vT4H*p;@T3uXYVChf4>-dzrQ|iN6fzSH)ZQ?KaDOv8Y5ZL
z|5{Guf`omvxK^-dyYM|FInjpn7tYg_KZIwyO!xlv)B0lm?i<d&mzzIah<X+!RIdE_
zB*)@5y`w*Wec;dHtMd=;*3U6r>=SbE>$$CBTKkHevnHnPKXdTx#r!&B>lO0r^YgTG
z`Ez;-d$$MK*ZoL&u}Apt&&$t6_e>2hi;Ro?|Ks4Xb^i}?dxuUjDc@K!HKr$Uj@a9~
zi`|}Ys(1S2|0(j`7SBh4i^>n1UkYBS)w^<qW?qP<`=^B~#3t%_{XXu#o7KMd-;clP
zKMiV^e=o~)c5hM+H?P`#{}2DCf8XA2bH4TFgI$=TX{xVj#@U1iEgF$k4l~W-)A`fl
zH{5Q{eSFaEbo$P9_HVW>Om$ti>(9q)F<%^(Zk6J`{^F34s&?r+mlJWC37=h+lN1id
z-Hi;rEt|8YF#W=}Uyt8*YPpM)>@9mL!sRseCG+u@p6l5^?7SB5_H?;3htK=>`RAEV
zRon7dT1d&wmHU>!awwtJFvD+Jr;^K+TR}7be)5aEZT94>-?_Ul!=~@vY~A{-eB0w^
z(f51qzA~5h``*6)Ud*g7Q|;sT#{ZwGw>F{u9Tz|QTJ|+%?ePis*{ydeEV{O)`N7Nf
z775S2pA#h2zRB%2`M*J4O0$0V=I_1#iobWTo3+KZZokdtS<WxJCg9ztIgOuRJv+Xs
zY~s~x;`h#p-+cDwWrgjFw`v#6`nJwZ{aJe{=dXFp6P3=S&V#2qn5xBXR(h9Ra{f4%
z-}bp;!b1)2z2+;9HS(XCJ;l=VNS=G!MZK8$8~)|@>b|ed{;+H2$)f^?-kp7RZ|8-q
zmU{v#n|D16+Hzyp)~9*v^48nM?ccp~E>D8bL5_3(KHZ&qy1S)w!=jzsQ73zXWv}a8
z>&tL@`10V@OF{3>9!ibc*Hg~Yy6AJ*TaKdePqLf0#cjwoUc|LQMXkqLPUPmKu7}cd
z3@%)px_{4}JuhaO{?0liEP1^tPWAW{<;B?>mu*n7n5R`yW4ohHv9P|%s`Tm>uE(p^
zzw<3GfA5r*Hg`sj!QQ!>Wg2!~KXmosm#wTO*XJG$d=L`#^V}xKVD6XYMZ5hgj``ew
z{q_5H`#ZVWc1QBwZhmxY$t#1-!*7hY1>E{_CRnh>^xyKtU!RKR*a<##7vGZf>gKAW
zUv^E|)S$ic)}@4ZZ(Sd4NL?8`_x7<1tmSTHswFG-w))*m|N3Ih=5?IAyboVdb}Ey9
zeS5}k`B$&+yiUqrcO{JBjsJqo=%dBGmc_H`_S)oB`WNe;QP>wDnUd^z`S!1KimQ{>
z%I^45v_fZX<nz{*qGz+EMM|gLsy%nib`xg_Z%@<J=E!$?yQ6jUv?Mu~U3@kBqu7hK
z4Illyru>n7P}pv%wP1VF{K-dSN{-GsvP)*eevRm+R{_r&)kDMTe|0;WKi$Q@!S3cZ
z?)|@Gm!AFFeJW;eV4d?#A<hWP1v!Peal#V?3KGw@re3?ASzqfZ<lQQfBxZPrVT0S@
zf>kRH^hCU0-m5A)Z&KpDC?*RJQGuAH8Dg(5ojstIq%`6Cmdcu=Uj?@Bf46N?mtbL0
zpUygk-EPM&sWzTIxl)MT#%uP{*4JM+oxg?6aMm=lDcS5ZWkH(C@+5=5Umo6FTlcS^
zRCjyT=XbZRUFV;l_dk~@Co+1WVTFnFwR2q8{vOLJO!$|yAbR$d4-*%NCoLD<bdr<z
z%B;A+WM1JiP4i37tH18Exg413VEE*ns`={&yur>hl(|zrCVZ`_D*YQEbzs_V(?2t-
zPu+`Bwa)Ha)%GZ7>6B@g86s9YCY{UQ<G-@x)a(C!i&ZD8Y08}|DsJ-+>n`Tm7JPdB
zzEoYY5ZjYij+=;Yyl^mQzo*jHU{UetkgV7n%4XZnyiq@s-F2QTV`Xsr1I_Ye=?gvF
zPx``Eaha6f{QjA><n-AWDbEu4l2-;BiW%muJiB$;p)Z-wPBZWF-_OIpb+)Klnd5~s
zjl8+un~$w!ny<g$XzPi!$(u@E#d@!a>U?uTJ$r|9Wtqcd%g|L}h0>;H!#o2g9XuR1
zX=gz*tEkwt$oTK&>c6)izTA6~arN#4d7PcT0hwV7ET2Wxd|Id+!E==L+RiQikF!|t
z=B!jn3hK_<e~vT2a`B2%&&iwlIx{EtO`D!H%W2E+CC4IlZ5F4l?$DVPyJ_9Gy0%*d
zm3ugx#3moJYo3w3d&cVUfQ_+|YbKp`YP)qV_DsO{O&9XMOli%Unw7XxH*~AdrJfII
z4_Xc~o#MKoXgMQwVb;~kUm9l(jN5YdwFXyB%vpMl=MsPD5??oiNz=MQ?_by;?p?fb
zYR<~pMI9<ZmxCn}#VxwR9B=q9ie?ut(mLjIz;JiQYuP}zf6Tj;qtDOwU|;|MeEAUV
literal 0
HcmV?d00001
diff --git a/examples/imp_per.mlw b/examples/imp_per.mlw
new file mode 100644
index 0000000..52ce429
--- /dev/null
+++ b/examples/imp_per.mlw
@@ -0,0 +1,86 @@
+theory Imp
+
+ use state.State
+ use bool.Bool
+ use int.Int
+
+
+ (* ************************ SYNTAX ************************ *)
+ type aexpr =
+ | Anum int
+ | Avar id
+ | Aadd aexpr aexpr
+ | Asub aexpr aexpr
+
+ type bexpr =
+ | Btrue
+ | Bfalse
+ | Bnot bexpr
+ | Beq aexpr aexpr
+ | Ble aexpr aexpr
+ | Band bexpr bexpr
+
+ type com =
+ | Cskip
+ | Cassign id aexpr
+ | Cseq com com
+ | Cif bexpr com com
+ | Cwhile bexpr com
+
+
+ (* ************************ SEMANTICS ************************ *)
+ function aeval (st:state) (e:aexpr) : int =
+ match e with
+ | Anum n -> n
+ | Avar x -> st[x]
+ | Aadd e1 e2 -> aeval st e1 + aeval st e2
+ | Asub e1 e2 -> aeval st e1 - aeval st e2
+ end
+
+ function beval (st:state) (b:bexpr) : bool =
+ match b with
+ | Btrue -> true
+ | Bfalse -> false
+ | Bnot b' -> notb (beval st b')
+ | Beq a1 a2 -> aeval st a1 = aeval st a2
+ | Ble a1 a2 -> aeval st a1 <= aeval st a2
+ | Band b1 b2 -> andb (beval st b1) (beval st b2)
+
+ end
+
+ inductive ceval state com state =
+ (* skip *)
+ | E_Skip : forall m. ceval m Cskip m
+
+ (* assignement *)
+ | E_Ass : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
+
+ (* sequence *)
+ | E_Seq : forall cmd1 cmd2 m0 m1 m2.
+ ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
+
+ (* if then else *)
+ | E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
+ ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
+
+ | E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
+ ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
+
+ (* while *)
+ | E_WhileEnd : forall cond m body. not beval m cond ->
+ ceval m (Cwhile cond body) m
+
+ | E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
+ ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
+ ceval mi (Cwhile cond body) mf
+
+
+ (* Determinstic semantics *)
+ lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
+ forall mf2. ([@inversion] ceval mi c mf2) -> mf1 = mf2
+
+ lemma ceval_deterministic : forall c mi mf1 mf2.
+ ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
+
+end
+
diff --git a/examples/state.mlw b/examples/state.mlw
new file mode 100644
index 0000000..a655477
--- /dev/null
+++ b/examples/state.mlw
@@ -0,0 +1,45 @@
+
+module State
+
+ use int.Int
+
+ type id = Id int
+ type state = id -> int
+
+ let function get (f: state) (x: id) = f x
+
+ let function set (f: state) (x: id) (v: int) : state =
+ fun (y: id) ->
+ match (x, y) with
+ | (Id xv, Id yv) -> if xv = yv then v else (f y)
+ end
+ meta rewrite_def function set
+
+ let function ([]) f x = f x
+ let function ([<-]) f x v = set f x v
+
+ let function const (v: int) : state
+ ensures { forall x. result[x] = v }
+ = fun _ -> v
+
+end
+
+module Reg
+
+ use int.Int
+
+ type idr = int
+ type regs = idr -> int
+
+ let function read (f: regs) (x: idr) = f x
+
+ let function write (f: regs) (x: idr) (v: int) : regs =
+ fun (y: idr) -> if x = y then v else (f y)
+
+ meta rewrite_def function write
+
+ let function const (v: int) : regs
+ ensures { forall x. read result x = v }
+ = fun _ -> v
+
+end
\ No newline at end of file
diff --git a/examples/vm_ind.mlw b/examples/vm_ind.mlw
new file mode 100644
index 0000000..752c229
--- /dev/null
+++ b/examples/vm_ind.mlw
@@ -0,0 +1,110 @@
+module ReflTransClosure
+
+ type parameter
+ type state
+ predicate transition parameter state state
+
+ inductive transition_star parameter (x y : state) =
+ | Refl_ : forall p x. transition_star p x x
+ | Step: forall p x y z.
+ transition p x y -> transition_star p y z -> transition_star p x z
+
+ lemma transition_star_one: forall p s1 s2.
+ transition p s1 s2 -> transition_star p s1 s2
+
+ lemma transition_star_transitive: forall p s1 s2 s3.
+ transition_star p s1 s2 -> transition_star p s2 s3 ->
+ transition_star p s1 s3
+
+end
+
+
+theory VM_ind
+
+ use export int.Int
+ use export list.List
+ use export list.NthNoOpt
+ use export state.State
+
+ type stack = list int
+ type pos = int
+ type machine_state = (pos, stack, state)
+
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Ivar id (* push the value of variable *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+ | Ihalt (* end of program *)
+
+ type code = list instr
+
+ function pop (st : stack) : (int, stack) =
+ match st with
+ | Nil -> (0, st)
+ | Cons c st' -> (c, st')
+ end
+
+ function push (v : int) (st : stack) : stack = Cons v st
+
+ inductive transition code machine_state machine_state =
+ | trans_const: forall c p n. nth p c = (Iconst n) ->
+ forall s m. transition c (p, s, m) (p + 1, push n s, m)
+
+ | trans_var: forall c p id. nth p c = (Ivar id) ->
+ forall s m. transition c (p, s, m) (p + 1, push m[id] s, m)
+
+ | trans_add: forall c p. nth p c = (Iadd) ->
+ forall n1 n2 s m. transition c (p, push n2 (push n1 s), m) (p + 1, push (n1 + n2) s, m)
+
+ | trans_sub: forall c p. nth p c = (Isub) ->
+ forall n1 n2 s m. transition c (p, push n2 (push n1 s), m) (p + 1, push (n1 - n2) s, m)
+
+
+ clone export ReflTransClosure with type parameter = code,
+ type state = machine_state, predicate transition = transition
+
+ predicate vm_terminates (c:code) (mi mf:state) =
+ exists p. nth p c = Ihalt /\
+ transition_star c (0, Nil, mi) (p, Nil, mf)
+
+ predicate vm_terminates_non_empty (c:code) (mi mf:state) =
+ exists p s. nth p c = Ihalt /\
+ transition_star c (0, Nil, mi) (p, s, mf)
+
+end
+
+theory VM_ind_test
+
+ use VM_ind
+ use map.Const
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = (Ivar (Id 1) :: (Iconst 1 :: (Iadd :: (Ihalt :: Nil))))
+
+ lemma c0 : nth 0 c = Ivar (Id 1)
+ lemma c1 : nth 1 c = Iconst 1
+ lemma c2 : nth 2 c = Iadd
+ lemma c3 : nth 3 c = Ihalt
+
+ lemma g1 : (* 2 + 1 = 3, step one *)
+ transition c (0, Nil, m0) (1, 2 :: Nil, m0)
+
+ lemma g2 : (* 2 + 1 = 3, step two *)
+ transition c (1, 2 :: Nil, m0) (2, 1 :: (2 :: Nil), m0)
+
+ lemma g3 : (* 2 + 1 = 3, step three *)
+ transition c (2, 1 :: (2 :: Nil), m0) (3, 3 :: Nil, m0)
+
+ lemma g3_trans : (* 2 + 1 = 3, multiple steps *)
+ transition_star c (0, Nil, m0) (3, 3 :: Nil, m0)
+
+ goal g_term : (* 2 + 1 = 3, terminates with non-empty stack *)
+ vm_terminates_non_empty c m0 m0
+
+end
+
+
+
diff --git a/examples/vm_mem.mlw b/examples/vm_mem.mlw
new file mode 100644
index 0000000..25ac783
--- /dev/null
+++ b/examples/vm_mem.mlw
@@ -0,0 +1,103 @@
+theory VM_mem
+
+ use export int.Int
+ use export list.List
+ use export state.State
+
+ type stack = list int
+ type machine_state = (stack, state)
+
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Ivar id (* push the value of variable *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+
+ function pop (st : stack) : (int, stack) =
+ match st with
+ | Nil -> (0, st)
+ | Cons c st' -> (c, st')
+ end
+
+
+ function push (v : int) (st : stack) : stack = Cons v st
+
+ function fconst (v : int) (m : machine_state) : machine_state =
+ let (stack, state) = m in (push v stack, state)
+
+ function fvar (id : id) (m : machine_state) : machine_state =
+ let (stack, state) = m in (push state[id] stack, state)
+
+
+ function fadd (m : machine_state) : machine_state =
+ let (stack, state) = m in
+ let (a1, st1) = pop stack in
+ let (a2, st2) = pop st1 in
+ (push (a1 + a2) st2, state)
+
+ function fsub (m : machine_state) : machine_state =
+ let (stack, state) = m in
+ let (a1, st1) = pop stack in
+ let (a2, st2) = pop st1 in
+ (push (a2 - a1) st2, state)
+
+end
+
+
+theory VM_mem_test
+
+ use VM_mem
+
+ goal g1 : (* 2 + 1 = 3 *)
+ forall state.
+ fadd (fconst 1 (fconst 2 (Nil, state))) = (Cons 3 Nil, state)
+
+ constant s0 : state = (const 0)[Id 1 <- 2]
+ constant m0 : machine_state = (Nil, s0)
+
+ goal g2 : (* a + 1 = 3, state[a] = 2 *)
+ fadd (fconst 1 (fvar (Id 1) m0)) = (Cons 3 Nil, s0)
+
+end
+
+
+theory VM_mem_list
+
+ use export VM_mem
+
+ function vm_i (i : instr) (m : machine_state) : machine_state =
+ match i with
+ | Iconst v -> fconst v m
+ | Ivar id -> fvar id m
+ | Iadd -> fadd m
+ | Isub -> fsub m
+ end
+
+ function vm (il : list instr) (m : machine_state) : machine_state =
+ match il with
+ | Nil -> m
+ | Cons i il' -> vm il' (vm_i i m)
+ end
+
+end
+
+theory VM_mem_list_test
+
+ use VM_mem_list
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ constant s0 : state = (const 0)[Id 1 <- 2]
+ constant m0 : machine_state = (Nil, s0)
+
+ goal g1 : (* 2 + 1 = 3 *)
+ vm (Iconst 2 :: (Iconst 1 :: (Iadd :: Nil))) m0 = (3 :: Nil, s0)
+
+ goal g2 : (* a + 1 = 3 *)
+ vm (Ivar (Id 1) :: (Iconst 1 :: (Iadd :: Nil))) m0 = (3 :: Nil, s0)
+
+
+end
+
+
+
diff --git a/examples/vm_mem/why3session.xml b/examples/vm_mem/why3session.xml
new file mode 100644
index 0000000..2a1422b
--- /dev/null
+++ b/examples/vm_mem/why3session.xml
@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../vm_mem.mlw">
+<theory name="VM_mem_test">
+ <goal name="g1">
+ <proof prover="0"><result status="unknown" time="0.06"/></proof>
+ <proof prover="1"><result status="timeout" time="1.00"/></proof>
+ <proof prover="2"><result status="timeout" time="10.00"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+</theory>
+<theory name="VM_mem_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="138"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="137"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_mem/why3session.xml.bak b/examples/vm_mem/why3session.xml.bak
new file mode 100644
index 0000000..1e7e846
--- /dev/null
+++ b/examples/vm_mem/why3session.xml.bak
@@ -0,0 +1,26 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../vm_mem.mlw">
+<theory name="VM_mem_test">
+ <goal name="g1">
+ <proof prover="0"><result status="unknown" time="0.06"/></proof>
+ <proof prover="1"><result status="timeout" time="1.00"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+</theory>
+<theory name="VM_mem_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="138"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="137"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_mem/why3shapes.gz b/examples/vm_mem/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..7861f4e60dd895c80d51205854aebe7f33b1657d
GIT binary patch
literal 218
zcmb2|=3oGW|4aK1W-%M`xV-<_RnwFkxlQE7N`VtgmtWeg6S-l+lBJ%`_WO5lxt+^o
z`PFPzW96(_QkuIqS~=-osM1;EaBcJVc@?^cFSeim+Pq^%=j+!WORiaTtDKk5|2^+X
z=8gR=KPzO6&)&aR#(F|RmT8Jhi{R{8Ow(JgMk-&~-O;`0^f|ZE9eHglBmEMut~&Za
zXv&$B#)}_oC?<HzBwt+mv*^df*}ZR`UC*EU<M>RwnHt<x=fw7ioD%ggG8I~VO(=7P
a4d2tYhL?Q*%CFV`j9=+tJ!KCg0|Nj)UTwDk
literal 0
HcmV?d00001
diff --git a/examples/vm_mem/why3shapes.gz.bak b/examples/vm_mem/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..7861f4e60dd895c80d51205854aebe7f33b1657d
GIT binary patch
literal 218
zcmb2|=3oGW|4aK1W-%M`xV-<_RnwFkxlQE7N`VtgmtWeg6S-l+lBJ%`_WO5lxt+^o
z`PFPzW96(_QkuIqS~=-osM1;EaBcJVc@?^cFSeim+Pq^%=j+!WORiaTtDKk5|2^+X
z=8gR=KPzO6&)&aR#(F|RmT8Jhi{R{8Ow(JgMk-&~-O;`0^f|ZE9eHglBmEMut~&Za
zXv&$B#)}_oC?<HzBwt+mv*^df*}ZR`UC*EU<M>RwnHt<x=fw7ioD%ggG8I~VO(=7P
a4d2tYhL?Q*%CFV`j9=+tJ!KCg0|Nj)UTwDk
literal 0
HcmV?d00001
diff --git a/examples/vm_per.mlw b/examples/vm_per.mlw
new file mode 100644
index 0000000..7928a57
--- /dev/null
+++ b/examples/vm_per.mlw
@@ -0,0 +1,254 @@
+
+(* Utility module: reflexive transitive closure of a parameterized
+ relation. *)
+module ReflTransClosure
+
+ type parameter
+ type state
+ predicate transition parameter state state
+
+ inductive transition_star parameter (x y:state) =
+ | Refl_: forall p x. transition_star p x x
+ | Step: forall p x y z.
+ transition p x y -> transition_star p y z -> transition_star p x z
+
+ lemma transition_star_one: forall p s1 s2.
+ transition p s1 s2 -> transition_star p s1 s2
+
+ lemma transition_star_transitive: forall p s1 s2 s3.
+ transition_star p s1 s2 -> transition_star p s2 s3 ->
+ transition_star p s1 s3
+
+end
+
+
+(******************************************************************************)
+
+(* The machine operates on a code c (a fixed list of instructions)
+ and three variable components:
+ - a program counter, denoting a position in c
+ - a state assigning integer values to variables
+ - an evaluation stack, containing integers.
+*)
+
+theory Vm
+
+ use export state.State
+ use export int.Int
+ use export list.List
+ use export list.Length
+ use export list.Append
+ use export int.EuclideanDivision
+
+ type pos = int (* read position on stack *)
+ type stack = list int (* stack contains just integers *)
+ type machine_state = VMS pos stack state (* virtual machine configuration *)
+
+
+ type ofs = int
+ (* The instruction set of the machine. *)
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Ivar id (* push the value of variable *)
+ | Isetvar id (* pop an integer, assign it to variable *)
+ | Ibranch ofs (* skip ofs instructions *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+ | Imul (* pop two values, push their product *)
+ | Ibeq ofs (* pop n2, pop n1, skip ofs forward if n1 = n2 *)
+ | Ibne ofs (* pop n2, pop n1, skip ofs forward if n1 <> n2 *)
+ | Ible ofs (* pop n2, pop n1, skip ofs forward if n1 <= n2 *)
+ | Ibgt ofs (* pop n2, pop n1, skip ofs forward if n1 > n2 *)
+ | Ihalt (* end of program *)
+
+ type code = list instr
+
+ (* Read pointer to code *)
+ inductive codeseq_at code pos code =
+ | codeseq_at_intro : forall c1 c2 c3.
+ codeseq_at (c1 ++ c2 ++ c3) (length c1) c2
+
+
+ lemma codeseq_at_app_right: forall c c1 c2 p.
+ codeseq_at c p (c1 ++ c2) -> codeseq_at c (p + length c1) c2
+
+
+ lemma codeseq_at_app_left: forall c c1 c2 p.
+ codeseq_at c p (c1 ++ c2) -> codeseq_at c p c1
+
+ function push (n:int) (s:stack) : stack = Cons n s
+ function iconst (n:int) : code = Cons (Iconst n) Nil
+ function ivar (x:id) : code = Cons (Ivar x) Nil
+ function isetvar (x:id) : code = Cons (Isetvar x) Nil
+ constant iadd : code = Cons Iadd Nil
+ constant isub : code = Cons Isub Nil
+ constant imul : code = Cons Imul Nil
+ function ibeq (ofs:ofs) : code = Cons (Ibeq ofs) Nil
+ function ible (ofs:ofs) : code = Cons (Ible ofs) Nil
+ function ibne (ofs:ofs) : code = Cons (Ibne ofs) Nil
+ function ibgt (ofs:ofs) : code = Cons (Ibgt ofs) Nil
+ function ibranch (ofs:ofs) : code = Cons (Ibranch ofs) Nil
+ constant ihalt : code = (Cons Ihalt Nil)
+
+ (* The semantics of the virtual machine is given in small-step style,
+ as a transition relation between machine states: triples (program
+ counter, evaluation stack, variable state). The transition relation is
+ parameterized by the code c. There is one transition rule for each
+ kind of instruction, except Ihalt, which has no transition. *)
+
+ inductive transition code machine_state machine_state =
+ | trans_const : forall c p n. codeseq_at c p (iconst n) ->
+ forall s m. transition c (VMS p s m) (VMS (p + 1) (push n s) m)
+
+ | trans_var : forall c p x. codeseq_at c p (ivar x) ->
+ forall s m. transition c (VMS p s m) (VMS (p + 1) (push m[x] s) m)
+
+ | trans_set_var: forall c p x. codeseq_at c p (isetvar x) ->
+ forall n s m. transition c (VMS p (push n s) m) (VMS (p + 1) s m[x<-n])
+
+ | trans_add : forall c p. codeseq_at c p iadd ->
+ forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
+ (VMS (p + 1) (push (n1 + n2) s) m)
+
+ | trans_sub : forall c p. codeseq_at c p isub ->
+ forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
+ (VMS (p + 1) (push (n1 - n2) s) m)
+
+ | trans_mul : forall c p. codeseq_at c p imul ->
+ forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
+ (VMS (p + 1) (push (n1 * n2) s) m)
+
+ | trans_beq: forall c p1 ofs. codeseq_at c p1 (ibeq ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 = n2 then p1 + 1 + ofs else p1 + 1) s m)
+
+ | trans_bne: forall c p1 ofs. codeseq_at c p1 (ibne ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 = n2 then p1 + 1 else p1 + 1 + ofs) s m)
+
+ | trans_ble: forall c p1 ofs. codeseq_at c p1 (ible ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 <= n2 then p1 + 1 + ofs else p1 + 1) s m)
+
+ | trans_bgt: forall c p1 ofs. codeseq_at c p1 (ibgt ofs) ->
+ forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
+ (VMS (if n1 <= n2 then p1 + 1 else p1 + 1 + ofs) s m)
+
+ | trans_branch: forall c p ofs. codeseq_at c p (ibranch ofs) ->
+ forall s m. transition c (VMS p s m) (VMS (p + 1 + ofs) s m)
+
+ (* As usual with small-step semantics, we form sequences of machine
+ transitions to define the behavior of a code. We always start with pc
+ = 0 and an empty evaluation stack. We stop successfully if pc points
+ to an Ihalt instruction and the evaluation stack is empty. *)
+
+ clone export ReflTransClosure with type parameter = code,
+ type state = machine_state, predicate transition = transition
+
+ predicate vm_terminates (c:code) (mi mf:state) =
+ exists p. codeseq_at c p ihalt /\
+ transition_star c (VMS 0 Nil mi) (VMS p Nil mf)
+
+ predicate vm_terminates_non_empty (c:code) (mi mf:state) =
+ exists p s. codeseq_at c p ihalt /\
+ transition_star c (VMS 0 Nil mi) (VMS p s mf)
+
+end
+
+theory Vm_test
+
+ use Vm
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = ivar (Id 1) ++ (iconst 1 ++ (iadd ++ ihalt))
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ lemma cs_0 : codeseq_at c 0 (ivar (Id 1))
+ lemma cs_1 : codeseq_at c 1 (iconst 1)
+ lemma cs_2 : codeseq_at c 2 iadd
+ lemma cs_3 : codeseq_at c 3 ihalt
+
+ lemma g1 : (* 0 -> 1 *)
+ transition c (VMS 0 Nil m0) (VMS 1 (2 :: Nil) m0)
+
+ lemma g2 : (* 1 -> 2 *)
+ transition c (VMS 1 (2::Nil) m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g2_trans : (* 0 -> 2 *)
+ transition_star c (VMS 0 Nil m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g3 : (* 2 -> 3 *)
+ transition c (VMS 2 (1::(2::Nil)) m0) (VMS 3 (3::Nil) m0)
+
+ goal g3_trans : (* 0 -> 3 *)
+ transition_star c (VMS 0 Nil m0) (VMS 3 (3::Nil) m0)
+
+ goal g_term :
+ vm_terminates_non_empty c m0 m0
+
+end
+
+
+theory Vm_test2
+
+ use Vm
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = ivar (Id 1) ++ (iconst 1 ++ (iadd ++ (isetvar (Id 2) ++ (ihalt))))
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ lemma cs_0 : codeseq_at c 0 (ivar (Id 1))
+ lemma cs_1 : codeseq_at c 1 (iconst 1)
+ lemma cs_2 : codeseq_at c 2 iadd
+ lemma cs_3 : codeseq_at c 3 (isetvar (Id 2))
+ lemma cs_4 : codeseq_at c 4 ihalt
+
+ lemma g1 :
+ transition c (VMS 0 Nil m0) (VMS 1 (2 :: Nil) m0)
+
+ lemma g2 :
+ transition c (VMS 1 (2::Nil) m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g2_trans :
+ transition_star c (VMS 0 Nil m0) (VMS 2 (1::(2 :: Nil)) m0)
+
+ lemma g3 :
+ transition c (VMS 2 (1::(2::Nil)) m0) (VMS 3 (3::Nil) m0)
+
+ goal g3_trans :
+ transition_star c (VMS 0 Nil m0) (VMS 3 (3::Nil) m0)
+
+ lemma g4 :
+ transition c (VMS 3 (3::Nil) m0) (VMS 4 Nil m0[Id 2<-3])
+
+ goal g4_trans :
+ transition_star c (VMS 0 Nil m0) (VMS 4 Nil m0[Id 2<-3])
+
+ goal g_term :
+ vm_terminates c m0 m0[Id 2<-3]
+
+end
+
+theory Vm_test3
+
+ use Vm
+
+ constant m0 : state = (const 0)[Id 1 <- 2]
+ constant c : code = ibranch 1 ++ (iconst 1 ++ ihalt)
+
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ lemma cs_0 : codeseq_at c 0 (ibranch 1)
+ lemma cs_1 : codeseq_at c 1 (iconst 1)
+ lemma cs_2 : codeseq_at c 2 ihalt
+
+ lemma g1 :
+ transition c (VMS 0 Nil m0) (VMS 2 Nil m0)
+
+ goal g_term :
+ vm_terminates_non_empty c m0 m0
+
+end
+
diff --git a/examples/vm_simple.mlw b/examples/vm_simple.mlw
new file mode 100644
index 0000000..d6898b2
--- /dev/null
+++ b/examples/vm_simple.mlw
@@ -0,0 +1,95 @@
+theory VM_simple
+
+ use export int.Int
+ use export list.List
+
+ type stack = list int
+
+ type instr =
+ | Iconst int (* push n on stack *)
+ | Iadd (* pop two values, push their sum *)
+ | Isub (* pop two values, push their difference *)
+
+ function pop (st : stack) : (int, stack) =
+ match st with
+ | Nil -> (0, st)
+ | Cons c st' -> (c, st')
+ end
+
+ function push (v : int) (st : stack) : stack = Cons v st
+
+ function fconst (v : int) (st : stack) : stack = push v st
+
+ function fadd (st : stack) : stack =
+ let (a1, st1) = pop st in
+ let (a2, st2) = pop st1 in
+ push (a1 + a2) st2
+
+ function fsub (st : stack) : stack =
+ let (a1, st1) = pop st in
+ let (a2, st2) = pop st1 in
+ push (a2 - a1) st2
+
+end
+
+theory VM_simple_test
+
+ use VM_simple
+
+ goal g1 : (* 1 + 2 = 3 *)
+ fadd (fconst 2 (fconst 1 Nil)) = Cons 3 Nil
+
+ goal g2 : (* 2 - 1 = 1 *)
+ fsub (fconst 1 (fconst 2 Nil)) = Cons 1 Nil
+
+ goal g3 : (* 3 - (1 + 2) = 0 *)
+ fsub (fadd (fconst 2 (fconst 1 (fconst 3 Nil)))) = Cons 0 Nil
+
+ goal g4 : (* (3 - 1) + 2 = 4 *)
+ fadd (fconst 2 (fsub (fconst 1 (fconst 3 Nil)))) = Cons 4 Nil
+
+end
+
+
+theory VM_simple_list
+
+ use export VM_simple
+
+ function vm_i (i : instr) (st : stack) : stack =
+ match i with
+ | Iconst v -> fconst v st
+ | Iadd -> fadd st
+ | Isub -> fsub st
+ end
+
+ function vm (il : list instr) (st : stack) : stack =
+ match il with
+ | Nil -> st
+ | Cons i il' -> vm il' (vm_i i st )
+ end
+
+end
+
+theory VM_simple_list_test
+
+ use VM_simple_list
+ function (::) (i : 'a) (l : list 'a) : list 'a = Cons i l
+
+ goal g1 : (* 1 + 2 = 3 *)
+ vm (Iconst 1 :: (Iconst 2 :: (Iadd :: Nil))) Nil = 3 :: Nil
+
+ goal g2 : (* 2 - 1 = 1 *)
+ vm (Iconst 2 :: (Iconst 1 :: (Isub :: Nil))) Nil = 1 :: Nil
+
+ goal g3 : (* 3 - (1 + 2) = 0 *)
+ vm (Iconst 3 :: (Iconst 1 :: (Iconst 2 :: (Iadd :: (Isub :: Nil))))) Nil
+ = 0 :: Nil
+
+ goal g4 : (* (3 - 1) + 2 = 4 *)
+ vm (Iconst 3 :: (Iconst 1 :: (Isub :: (Iconst 2 :: (Iadd :: Nil))))) Nil
+ = 4 :: Nil
+
+end
+
+
+
diff --git a/examples/vm_simple/why3session.xml b/examples/vm_simple/why3session.xml
new file mode 100644
index 0000000..83ad4d6
--- /dev/null
+++ b/examples/vm_simple/why3session.xml
@@ -0,0 +1,132 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../vm_ind.mlw" proved="true">
+<theory name="ReflTransClosure" proved="true">
+ <goal name="transition_star_one" proved="true">
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="transition_star_transitive" proved="true">
+ <transf name="induction_pr" proved="true" >
+ <goal name="transition_star_transitive.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
+ </goal>
+ <goal name="transition_star_transitive.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="VM_ind_test" proved="true">
+ <goal name="c0" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
+ </goal>
+ <goal name="c1" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+ </goal>
+ <goal name="c2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
+ </goal>
+ <goal name="c3" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="41"/></proof>
+ </goal>
+ <goal name="g1" proved="true">
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="55"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="64"/></proof>
+ </goal>
+ <goal name="g3_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="185"/></proof>
+ </goal>
+ <goal name="g_term" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="46"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../state.mlw" proved="true">
+<theory name="State" proved="true">
+ <goal name="VC get" expl="VC for get" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC set" expl="VC for set" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix [<-]" expl="VC for mixfix [<-]" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="Reg" proved="true">
+ <goal name="VC read" expl="VC for read" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC write" expl="VC for write" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../vm_mem.mlw" proved="true">
+<theory name="VM_mem_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+</theory>
+<theory name="VM_mem_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="138"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="137"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../vm_simple.mlw" proved="true">
+<theory name="VM_simple_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.01" steps="31"/></proof>
+ </goal>
+</theory>
+<theory name="VM_simple_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.07" steps="224"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0" timelimit="1"><result status="valid" time="0.07" steps="227"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_simple/why3session.xml.bak b/examples/vm_simple/why3session.xml.bak
new file mode 100644
index 0000000..fd93fcb
--- /dev/null
+++ b/examples/vm_simple/why3session.xml.bak
@@ -0,0 +1,36 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../vm_simple.mlw" proved="true">
+<theory name="VM_simple_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
+ </goal>
+</theory>
+<theory name="VM_simple_list_test" proved="true">
+ <goal name="g1" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g2" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="113"/></proof>
+ </goal>
+ <goal name="g3" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="224"/></proof>
+ </goal>
+ <goal name="g4" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="227"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/vm_simple/why3shapes.gz b/examples/vm_simple/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..7899402116a3e26b0ad9aca419da93ef5386d71e
GIT binary patch
literal 1143
zcmb2|=3oGW|4YMs`=!l!_WllkBd?(lxX6V~_kz*^rs|g~KP=T?@=}s!j#S^Ep84zj
z>B#gqU*F|4nXn&L&io-~Ki|zmBkEdEk(WgkuUQfc_bj(XS>{HvDfM@JcYptFe%zDq
z_J-c*9o1WEZ|%GrpweMmwl2_Tm8V(i%R5sRO$ofd@Y3B=W^3~8FMMG$O%-cCuxx_v
zCcf;8B}a4=*IazC^>}#Wn{V5G*L?2Qznt25yC(8T?!LWy?@EY2y)$=?Lo(;JR_#Jv
z!`@q**E?Q+7rLJPsAzYZ-~Dc{=sj+K-_ET3G~;w=<Ylw`i;vqv&L%CnQR1L=Pm-<q
z^9li*H&%IKDL4J|t0(A{&wrv&zWBH=Yx5%8BpFjhQSQj*Nnwp_A&0l-&dL4#`)^^<
zWe?6mmBlv{mrvN>^7=|Z)3ZrGIyKKMGdk9$?2_Xr&SQBb&}4V4E_18k#C2yc<$Mdf
z=PT{habZ%CziFqb&IJoc>3{=scf5)-|MmEBd-*JzTldS~Ke5w!{e$)IRqgLDO14OL
zwl6HnmndQW`cp&BH#3U4pq8<cHPf=`^hK%p>Q;e$iiIXpF4w$0EU#EJJy(8Zb^p5K
z^zE0PYUtLuUafj(IYDjh%80XFC!+!sxeuLx_UP%CwFkMATI1aEaswW#&Dg}#voS*6
zO8m>^zq390zwh4bQ&qFMTx{=ugTJp$`rdHNylB0=EhwAqjYOw~Aiq$~(biXKzkeOO
zC!hE4TIQ{Swnx8?9`rD*Hd)D2@Hyz2Qc_%;-8uc`FV?>J$SkBK`cU!S;hkS!q*Olm
z^y%-r&obBM*ZWHI7%Q0?yKWBRiCSk-6zILRv@+|{Xa78r1I>L8UaXmyqUv>ZzJi(9
zd*!$uxwPkZ9;Aoa=Fk0CKbN&kIxm*1iN8WkH2wX&Q2DP`6E^-l@$-bpH^pVFe-{`n
z>s7Dk@qG0*rnhRD%&x@qhfhCx_MGK!@eSWs#YY1JXS%6pIWO40?4+x)`Zq7BHM{MC
zYY%7pM;3QZ=$ps2UQ2P>o0Z2+_S|9BZ_azS@rHP8q}+om#r(YccuzmtI)84|c}ugC
z#)4<JE@u$jwdTu3Vetc5cam4>2kHDO&wG3PL=n&IFn1ocg_jLB?R2~-AN=9S=JK-r
z3iZ3}&mURT`yof&?$%7(N}JFRCClc-aXp>oVPrZfusyqwf2wUj-VA}b1@`S<7yo(T
z6k*|zH_z*<W9Pacxmx*!yOKUuB|V(<Q1bbti@w2*r|yO*m+zPV^XP++<i_%%%$)uY
zee$=x^yhq(Tkv-kzhji#;i;1YV^c3BFn(B=yK~AXk^H+S_4!{m{aa8jy&@)JMe6^K
z3t>(fN_SI>8+Ki|`XlK}_C9;3^ZYLYg<D@eUft_;d{N8FY~2GFZf<?KdhOReTQ&sU
z`dJ<uGTrp;-Tb)!S`ud_*dCbY{eAWQlesteO}@x{HNF-+*DLJ5+RD1^tl?8G6~EQE
z=l8EvF)I6~R`xIXi}i<B2iLmuG47n1JvZJmhS9S9QF~&=!q&P2t7m@QtzGh}`#(eb
L?EO5ixEUA#z~Vhc
literal 0
HcmV?d00001
diff --git a/examples/vm_simple/why3shapes.gz.bak b/examples/vm_simple/why3shapes.gz.bak
new file mode 100644
index 0000000000000000000000000000000000000000..1e48fe050851d7d73db8b72fee23aaac8079dfc0
GIT binary patch
literal 322
zcmb2|=3oGW|4S$N`Z*i&w0yU9?SEjgQ8qm3XcupJfsFeqmefE8nfc#;IcsaU9#Fb;
zV&Xo@bf+f=xFV!Zc3jfD`cU$Owa5C<>D%u0e7*hYSlidU!}HB<rypPJQMSKs!)?#%
zc~2L$2I|@=O|o)Pd}UM;5}I|VWX{KJ`fpo)GSq)4dvP>?A$w_g+Zqu^({j@zhKoeg
z{+-z^^GV@TC!e)d*QTgkRYRBLhO}okOOh9CUXs6k|CGNyab;gbb~a5pb5YB>Fyxfn
zp%pJ)EuH&feLwrosGD~Me^)l8PqsY!#%%uMFBcdbcO=icC%ao~TBf7^n}?Z3^0hIg
zM^{@uTf2Y9yXr?m7XuxHIQ+|8=j8nIYdh=IvVPYy`<(yIt7`Y}Wtgz7@m_=rt0(t|
e63$w!Td(Yc&aT^^m+@c!9^*~+XJRGH3=9B+iJqAN
literal 0
HcmV?d00001
--
GitLab