Skip to content

GitLab

Commit 17c1643a authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Nex example: toy compiler

parent b137be24
Hide whitespace changes
Inline Side-by-side
ROADMAP
View file @ 17c1643a
......@@ -195,7 +195,7 @@
== TODOs ==
* replayer: replay should be considered failed if new goals appeared.
* DONE replayer: replay should be considered failed if new goals appeared.
* documentation des nouvelles features higher-order
......
examples/toy_compiler.mlw 0 → 100644
View file @ 17c1643a
theory Expr
use import int.Int
type expr = Cte int | Plus expr expr | Minus expr expr | Mult expr expr
function eval_expr (e:expr) : int =
match e with
| Cte n -> n
| Plus e1 e2 -> eval_expr e1 + eval_expr e2
| Minus e1 e2 -> eval_expr e1 - eval_expr e2
| Mult e1 e2 -> eval_expr e1 * eval_expr e2
end
end
theory StackMachine
type asm = Push int | Add | Sub | Mul
use export int.Int
use export list.List
function compute (s:list int) (a:list asm) : list int =
match a with
| Nil -> s
| Cons a r ->
match a,s with
| Push n, _ -> compute (Cons n s) r
| Add, (Cons n1 (Cons n2 s)) -> compute (Cons (n2+n1) s) r
| Sub, (Cons n1 (Cons n2 s)) -> compute (Cons (n2-n1) s) r
| Mul, (Cons n1 (Cons n2 s)) -> compute (Cons (n2*n1) s) r
| _ -> s
end
end
end
module Compiler
use export list.Append
use import Expr
use import StackMachine
function compile (e:expr) : list asm =
match e with
| Cte n -> Cons (Push n) Nil
| Plus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Add Nil)
| Minus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Sub Nil)
| Mult e1 e2 -> compile e1 ++ (compile e2 ++ Cons Mul Nil)
end
let rec lemma soundness_gen (e:expr) (s:list int) (r:list asm)
variant { e }
ensures { compute s (compile e ++ r) = compute (Cons (eval_expr e) s) r }
= match e with
| Cte n ->
assert { compile e ++ r = Cons (Push n) r }
| Plus e1 e2 ->
soundness_gen e1 s (compile e2 ++ Cons Add r);
soundness_gen e2 (Cons (eval_expr e1) s) (Cons Add r)
| Minus e1 e2 ->
soundness_gen e1 s (compile e2 ++ Cons Sub r);
soundness_gen e2 (Cons (eval_expr e1) s) (Cons Sub r)
| Mult e1 e2 ->
soundness_gen e1 s (compile e2 ++ Cons Mul r);
soundness_gen e2 (Cons (eval_expr e1) s) (Cons Mul r)
end
let lemma soundness (e:expr)
ensures { compute Nil (compile e) = (Cons (eval_expr e) Nil) }
=
assert { compute Nil (compile e) = compute Nil (compile e ++ Nil) }
end
examples/toy_compiler/why3session.xml 0 → 100644
View file @ 17c1643a
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
name="CVC4"
version="1.3"/>
<prover
id="3"
name="Z3"
version="3.2"/>
<prover
id="4"
name="Z3"
version="4.3.1"/>
<file
name="../toy_compiler.mlw"
verified="true"
expanded="true">
<theory
name="Expr"
locfile="../toy_compiler.mlw"
loclnum="3" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
</theory>
<theory
name="StackMachine"
locfile="../toy_compiler.mlw"
loclnum="19" loccnumb="7" loccnume="19"
verified="true"
expanded="false">
</theory>
<theory
name="Compiler"
locfile="../toy_compiler.mlw"
loclnum="42" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
<goal
name="WP_parameter soundness_gen"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="VC for soundness_gen"
sum="7d75d20235ea1eb25cec98b191a56447"
proved="true"
expanded="true"
shape="Cainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Aainfix =ainfix ++acompileV0V2aConsaPushV3V2aCteVainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =acomputeV8ainfix ++acompileV5V7acomputeaConsaeval_exprV5V8V7ACfaCtewainfix =V10V5Oainfix =V9V5aPlusVVainfix =V12V5Oainfix =V11V5aMinusVVainfix =V14V5Oainfix =V13V5aMultVVV0LaConsaeval_exprV4V1LaConsaAddV2Iainfix =acomputeV1ainfix ++acompileV4V6acomputeaConsaeval_exprV4V1V6ACfaCtewainfix =V16V4Oainfix =V15V4aPlusVVainfix =V18V4Oainfix =V17V4aMinusVVainfix =V20V4Oainfix =V19V4aMultVVV0Lainfix ++acompileV5aConsaAddV2aPlusVVainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =acomputeV25ainfix ++acompileV22V24acomputeaConsaeval_exprV22V25V24ACfaCtewainfix =V27V22Oainfix =V26V22aPlusVVainfix =V29V22Oainfix =V28V22aMinusVVainfix =V31V22Oainfix =V30V22aMultVVV0LaConsaeval_exprV21V1LaConsaSubV2Iainfix =acomputeV1ainfix ++acompileV21V23acomputeaConsaeval_exprV21V1V23ACfaCtewainfix =V33V21Oainfix =V32V21aPlusVVainfix =V35V21Oainfix =V34V21aMinusVVainfix =V37V21Oainfix =V36V21aMultVVV0Lainfix ++acompileV22aConsaSubV2aMinusVVainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =acomputeV42ainfix ++acompileV39V41acomputeaConsaeval_exprV39V42V41ACfaCtewainfix =V44V39Oainfix =V43V39aPlusVVainfix =V46V39Oainfix =V45V39aMinusVVainfix =V48V39Oainfix =V47V39aMultVVV0LaConsaeval_exprV38V1LaConsaMulV2Iainfix =acomputeV1ainfix ++acompileV38V40acomputeaConsaeval_exprV38V1V40ACfaCtewainfix =V50V38Oainfix =V49V38aPlusVVainfix =V52V38Oainfix =V51V38aMinusVVainfix =V54V38Oainfix =V53V38aMultVVV0Lainfix ++acompileV39aConsaMulV2aMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
<goal
name="WP_parameter soundness_gen.1"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="1. assertion"
sum="a27ad7fd22466f1f61b6d6a0aa35704b"
proved="true"
expanded="false"
shape="assertionCainfix =ainfix ++acompileV0V2aConsaPushV3V2aCteVtaPlusVVtaMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.18"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.2"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="2. postcondition"
sum="42976fdb5985b1187529016f5c35405f"
proved="true"
expanded="false"
shape="postconditionCainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =ainfix ++acompileV0V2aConsaPushV3V2aCteVtaPlusVVtaMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.3"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="3. variant decrease"
sum="b5384854e87899b767adc77cccfac514"
proved="true"
expanded="false"
shape="variant decreaseCtaCteVCfaCtewainfix =V8V4Oainfix =V7V4aPlusVVainfix =V10V4Oainfix =V9V4aMinusVVainfix =V12V4Oainfix =V11V4aMultVVV0Lainfix ++acompileV5aConsaAddV2aPlusVVtaMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.4"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="4. variant decrease"
sum="4864e2ce3862ff95464a9ec1c9cd93ce"
proved="true"
expanded="false"
shape="variant decreaseCtaCteVCfaCtewainfix =V10V5Oainfix =V9V5aPlusVVainfix =V12V5Oainfix =V11V5aMinusVVainfix =V14V5Oainfix =V13V5aMultVVV0LaConsaeval_exprV4V1LaConsaAddV2Iainfix =acomputeV1ainfix ++acompileV4V6acomputeaConsaeval_exprV4V1V6Lainfix ++acompileV5aConsaAddV2aPlusVVtaMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.5"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="5. postcondition"
sum="4fbc42b0f30de3c40b41cc23014e5553"
proved="true"
expanded="false"
shape="postconditionCtaCteVainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =acomputeV8ainfix ++acompileV5V7acomputeaConsaeval_exprV5V8V7LaConsaeval_exprV4V1LaConsaAddV2Iainfix =acomputeV1ainfix ++acompileV4V6acomputeaConsaeval_exprV4V1V6Lainfix ++acompileV5aConsaAddV2aPlusVVtaMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.6"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="6. variant decrease"
sum="03983af0097da991771e457366f0bf6a"
proved="true"
expanded="false"
shape="variant decreaseCtaCteVtaPlusVVCfaCtewainfix =V10V6Oainfix =V9V6aPlusVVainfix =V12V6Oainfix =V11V6aMinusVVainfix =V14V6Oainfix =V13V6aMultVVV0Lainfix ++acompileV7aConsaSubV2aMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.7"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="7. variant decrease"
sum="dd7877736d0d0d9e5a38a3ebb9534006"
proved="true"
expanded="false"
shape="variant decreaseCtaCteVtaPlusVVCfaCtewainfix =V12V7Oainfix =V11V7aPlusVVainfix =V14V7Oainfix =V13V7aMinusVVainfix =V16V7Oainfix =V15V7aMultVVV0LaConsaeval_exprV6V1LaConsaSubV2Iainfix =acomputeV1ainfix ++acompileV6V8acomputeaConsaeval_exprV6V1V8Lainfix ++acompileV7aConsaSubV2aMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.8"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="8. postcondition"
sum="15de6d80300e5218b09f5acf5f54bc55"
proved="true"
expanded="false"
shape="postconditionCtaCteVtaPlusVVainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =acomputeV10ainfix ++acompileV7V9acomputeaConsaeval_exprV7V10V9LaConsaeval_exprV6V1LaConsaSubV2Iainfix =acomputeV1ainfix ++acompileV6V8acomputeaConsaeval_exprV6V1V8Lainfix ++acompileV7aConsaSubV2aMinusVVtaMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.50"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.9"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="9. variant decrease"
sum="25367a6e77c45970d27f77fff73a9fa2"
proved="true"
expanded="false"
shape="variant decreaseCtaCteVtaPlusVVtaMinusVVCfaCtewainfix =V12V8Oainfix =V11V8aPlusVVainfix =V14V8Oainfix =V13V8aMinusVVainfix =V16V8Oainfix =V15V8aMultVVV0Lainfix ++acompileV9aConsaMulV2aMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.10"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="10. variant decrease"
sum="6d0597bf79413a7b1aa33078558d3b93"
proved="true"
expanded="false"
shape="variant decreaseCtaCteVtaPlusVVtaMinusVVCfaCtewainfix =V14V9Oainfix =V13V9aPlusVVainfix =V16V9Oainfix =V15V9aMinusVVainfix =V18V9Oainfix =V17V9aMultVVV0LaConsaeval_exprV8V1LaConsaMulV2Iainfix =acomputeV1ainfix ++acompileV8V10acomputeaConsaeval_exprV8V1V10Lainfix ++acompileV9aConsaMulV2aMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter soundness_gen.11"
locfile="../toy_compiler.mlw"
loclnum="56" loccnumb="16" loccnume="29"
expl="11. postcondition"
sum="c1c3e70f0b75cd8fcb7a2ba9ffb92ca0"
proved="true"
expanded="false"
shape="postconditionCtaCteVtaPlusVVtaMinusVVainfix =acomputeV1ainfix ++acompileV0V2acomputeaConsaeval_exprV0V1V2Iainfix =acomputeV12ainfix ++acompileV9V11acomputeaConsaeval_exprV9V12V11LaConsaeval_exprV8V1LaConsaMulV2Iainfix =acomputeV1ainfix ++acompileV8V10acomputeaConsaeval_exprV8V1V10Lainfix ++acompileV9aConsaMulV2aMultVVV0F">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness_gen"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.51"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter soundness"
locfile="../toy_compiler.mlw"
loclnum="73" loccnumb="12" loccnume="21"
expl="VC for soundness"
sum="35015690b35ca33cfa700b42a08a50fa"
proved="true"
expanded="true"
shape="ainfix =acomputeaNilacompileV0aConsaeval_exprV0aNilAainfix =acomputeaNilacompileV0acomputeaNilainfix ++acompileV0aNilF">
<label
name="why3:lemma"/>
<label
name="expl:VC for soundness"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"