Commit b9633ad1 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Merge branch 'new_system' into mp

Conflicts:
	share/emacs/why3.el
	share/vim/syntax/why3.vim
	src/mlw/compile.ml
	src/mlw/dexpr.ml
	src/parser/parser.mly
	src/parser/typing.ml
parents 43806070 54e5a079
......@@ -178,8 +178,8 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
collect_data_model parse_smtv2_model_lexer parse_smtv2_model \
parse_smtv2_model
LIB_MLW = ity expr dexpr pdecl eval_match typeinv vc pmodule \
pinterp compile pdriver cprinter ocaml_printer
LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \
pinterp mltree compile pdriver cprinter ocaml_printer
LIB_PARSER = ptree glob typing parser lexer
......@@ -1601,8 +1601,9 @@ CLEANDIRS += src/trywhy3
.PHONY: bench test
bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
share/Makefile.config
# temporarily disabled dependency: bin/why3extract
share/Makefile.config bin/why3extract.@OCAMLBEST@
bash bench/bench ".@OCAMLBEST@"
@echo "=== Checking Why3 API ==="
$(MAKE) test-api-logic.@OCAMLBEST@
# $(MAKE) test-api-mlw-tree.@OCAMLBEST@
# $(MAKE) test-api-mlw.@OCAMLBEST@
......@@ -1611,9 +1612,9 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
bash bench/bench ".@OCAMLBEST@"
@if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \
echo ; \
echo "=== Checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic.@OCAMLBEST@; fi
###############
......
......@@ -169,10 +169,6 @@ list_stuff () {
fi
}
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
echo "=== Checking theories ==="
goods theories --type-only # FIXME remove --type-only
echo ""
......@@ -193,6 +189,33 @@ bads bench/typing/bad --type-only
bads bench/programs/bad-typing --type-only
echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
echo "=== Checking execution ==="
execute examples/euler001.mlw Euler001.bench
execute examples/euler002.mlw Solve.bench
......@@ -225,7 +248,7 @@ execute examples/vstte10_queens.mlw NQueens.test8
echo ""
echo "=== Extraction to Ocaml ==="
echo "=== Checking extraction to OCaml ==="
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
......@@ -234,31 +257,6 @@ extract_and_run examples/defunctionalization defunctionalization.ml
extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/in_progress
echo ""
echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking --list-* ==="
list_stuff --list-transforms
list_stuff --list-printers
......
......@@ -127,14 +127,14 @@ we invoke \texttt{extract} from the directory where this file is stored. File
\texttt{aqueue.ml} now contains the following OCaml code:
\begin{whycode}
let enqueue (x: 'a) (q: 'a queue) : 'a queue =
create (q.front) (q.lenf) (x :: (q.rear))
(Z.add (q.lenr) (Z.of_string "1"))
create (q.front) (q.lenf) (x :: (q.rear))
(Z.add (q.lenr) (Z.of_string "1"))
\end{whycode}
Choosing a function symbol as the entry point of extraction allows us to focus
only on specific parts of the program. However, the generated code cannot be
type-checked by the OCaml compiler, as it depends on function \texttt{create}
and on type \texttt{'a queue}, whose definitions are not given. In order to
obtain a \emph{correct} OCaml implementation, we can perform a recursive
obtain a \emph{complete} OCaml implementation, we can perform a recursive
extraction:
\begin{verbatim}
> why3 extraction --recursive -D ocaml64 -L . \
......@@ -162,6 +162,9 @@ let enqueue (x: 'a) (q: 'a queue) : 'a queue =
create (q.front) (q.lenf) (x :: (q.rear))
(Z.add (q.lenr) (Z.of_string "1"))
\end{whycode}
This new version of the code is now accepted by the OCaml compiler.
Let us now consider the
% \label{fig:extract-queens}
% \caption{Recursive extraction of \texttt{queens} function.}
% \end{figure}
......
......@@ -59,30 +59,24 @@ module AddListImp
use import SumList
use import ref.Ref
exception Break
let sum (l: list or_integer_float) : (int, real) =
returns { si, sf -> si = add_int l /\ sf = add_real l }
let si = ref 0 in
let sf = ref 0.0 in
let ll = ref l in
try
while True do
while True do
invariant { !si + add_int !ll = add_int l /\
!sf +. add_real !ll = add_real l
}
!sf +. add_real !ll = add_real l }
variant { !ll }
match !ll with
| Nil -> raise Break
| Nil -> return (!si, !sf)
| Cons (Integer n) t ->
si := !si + n; ll := t
| Cons (Real x) t ->
sf := !sf +. x; ll := t
end
done;
absurd
with Break -> (!si, !sf)
end
done;
absurd
let main () =
......
This diff is collapsed.
module Bag
use BuiltIn
use import int.Int
type bag 'a = 'a -> int
......@@ -13,10 +12,10 @@ module Bag
fun _ -> 0
let ghost function add (e: 'a) (b: bag 'a): bag 'a =
fun x -> if BuiltIn.(=) x e then b x + 1 else b x
fun x -> if pure {x = e} then b x + 1 else b x
let ghost function remove (e: 'a) (b: bag 'a): bag 'a =
fun x -> if BuiltIn.(=) x e then b x - 1 else b x
fun x -> if pure {x = e} then b x - 1 else b x
end
......
......@@ -11,34 +11,30 @@ module BinarySearch
(* the code and its specification *)
exception Break int (* raised to exit the loop *)
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int) (v : int) : int
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
= try
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant { 0 <= !l /\ !u < length a }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + div (!u - !l) 2 in
assert { !l <= m <= !u };
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
raise (Break m)
done;
raise Not_found
with Break i ->
i
end
=
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant { 0 <= !l /\ !u < length a }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + div (!u - !l) 2 in
assert { !l <= m <= !u };
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
return m
done;
raise Not_found
end
......@@ -51,7 +47,6 @@ module BinarySearchAnyMidPoint
use import ref.Ref
use import array.Array
exception Break int (* raised to exit the loop *)
exception Not_found (* raised to signal a search failure *)
val midpoint (l:int) (u:int) : int
......@@ -61,26 +56,23 @@ module BinarySearchAnyMidPoint
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
= try
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant { 0 <= !l /\ !u < length a }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = midpoint !l !u in
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
raise (Break m)
done;
raise Not_found
with Break i ->
i
end
=
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant { 0 <= !l /\ !u < length a }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = midpoint !l !u in
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
return m
done;
raise Not_found
end
......@@ -95,7 +87,6 @@ module BinarySearchInt32
(* the code and its specification *)
exception Break int32 (* raised to exit the loop *)
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int32) (v : int32) : int32
......@@ -104,27 +95,24 @@ module BinarySearchInt32
ensures { 0 <= to_int result < to_int a.length /\ a[to_int result] = v }
raises { Not_found ->
forall i:int. 0 <= i < to_int a.length -> a[i] <> v }
= try
let l = ref (of_int 0) in
let u = ref (length a - of_int 1) in
while !l <= !u do
invariant { 0 <= to_int !l /\ to_int !u < to_int a.length }
invariant { forall i : int. 0 <= i < to_int a.length ->
a[i] = v -> to_int !l <= i <= to_int !u }
variant { to_int !u - to_int !l }
let m = !l + (!u - !l) / of_int 2 in
assert { to_int !l <= to_int m <= to_int !u };
if a[m] < v then
l := m + of_int 1
else if a[m] > v then
u := m - of_int 1
else
raise (Break m)
done;
raise Not_found
with Break i ->
i
end
=
let l = ref (of_int 0) in
let u = ref (length a - of_int 1) in
while !l <= !u do
invariant { 0 <= to_int !l /\ to_int !u < to_int a.length }
invariant { forall i : int. 0 <= i < to_int a.length ->
a[i] = v -> to_int !l <= i <= to_int !u }
variant { to_int !u - to_int !l }
let m = !l + (!u - !l) / of_int 2 in
assert { to_int !l <= to_int m <= to_int !u };
if a[m] < v then
l := m + of_int 1
else if a[m] > v then
u := m - of_int 1
else
return m
done;
raise Not_found
end
......
......@@ -7,7 +7,7 @@
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../binomial_heap.mlw" expanded="true">
<theory name="BinomialHeap" sum="a4b20c3f0b661937cb05ebc19298c2ba" expanded="true">
<theory name="BinomialHeap" sum="29e615152758f1877eb6b8f1337e9f22" expanded="true">
<goal name="VC size_nonnneg" expl="VC for size_nonnneg">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="3d8c813c16bfe39e1ebc7795ba216b68">
<theory name="Test_proofinuse" sum="56dbf919cc4930dbaacdba6442726774">
<goal name="VC shift_is_div" expl="VC for shift_is_div">
<proof prover="1" timelimit="1"><result status="valid" time="0.11" steps="111"/></proof>
</goal>
......
......@@ -2,9 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="320a27ff6d5b9e231da1e9f9dee7818c" expanded="true">
<theory name="BraunHeaps" sum="d55c672dc562dbea343cabfcc2fc8ad9" expanded="true">
<goal name="VC le_root" expl="VC for le_root">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
......@@ -23,8 +24,8 @@
<goal name="VC extract" expl="VC for extract">
<proof prover="1"><result status="valid" time="0.97" steps="2514"/></proof>
</goal>
<goal name="VC replace_min" expl="VC for replace_min" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC replace_min" expl="VC for replace_min">
<transf name="split_goal_wp">
<goal name="VC replace_min.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="127"/></proof>
</goal>
......@@ -75,8 +76,8 @@
</goal>
</transf>
</goal>
<goal name="VC merge" expl="VC for merge" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC merge" expl="VC for merge">
<transf name="split_goal_wp">
<goal name="VC merge.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="53"/></proof>
</goal>
......@@ -134,27 +135,27 @@
<proof prover="1"><result status="valid" time="0.02" steps="144"/></proof>
</goal>
<goal name="VC size_height" expl="VC for size_height">
<proof prover="1"><result status="valid" time="0.12" steps="613"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.12" steps="613"/></proof>
</goal>
<goal name="VC inv_height" expl="VC for inv_height" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC inv_height" expl="VC for inv_height">
<transf name="split_goal_wp">
<goal name="VC inv_height.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.07" steps="260"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.07" steps="260"/></proof>
</goal>
<goal name="VC inv_height.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="35"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC inv_height.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC inv_height.4" expl="4. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="VC inv_height.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC inv_height.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="4.97" steps="860"/></proof>
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
......
......@@ -106,7 +106,7 @@
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerIntTest" sum="1abff7712bc37edc4cc97fd8c0c09795" expanded="true">
<theory name="PowerIntTest" sum="ea585215cae636c207832fffd3f1d4a7" expanded="true">
<goal name="Pow_2_2" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
......
......@@ -21,8 +21,6 @@ module Decrease1
variant { j - i }
= if i < j then decrease1_induction a (i+1) j
exception Found
let search (a: array int)
requires { decrease1 a }
ensures {
......@@ -30,18 +28,14 @@ module Decrease1
\/ (0 <= result < length a /\ a[result] = 0 /\
forall j: int. 0 <= j < result -> a[j] <> 0) }
= let i = ref 0 in
try
while !i < length a do
invariant { 0 <= !i }
invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 }
variant { length a - !i }
if a[!i] = 0 then raise Found;
if a[!i] > 0 then i := !i + a[!i] else i := !i + 1
done;
-1
with Found ->
!i
end
while !i < length a do
invariant { 0 <= !i }
invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 }
variant { length a - !i }
if a[!i] = 0 then return !i;
if a[!i] > 0 then i := !i + a[!i] else i := !i + 1
done;
-1
let rec search_rec (a: array int) (i : int)
requires { decrease1 a /\ 0 <= i }
......
......@@ -105,4 +105,4 @@ module DFS
assert { well_colored !marked !busy };
dfs root
end
\ No newline at end of file
end
......@@ -24,8 +24,8 @@ module Compile_aexpr
meta rewrite_def function aexpr_post
let rec compile_aexpr (a:aexpr) : hl 'a
ensures { result <% (trivial_pre,aexpr_post a result.code.length) }
ensures { hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> aexpr_post a result.code.length }
variant { a }
= let c = match a with
| Anum n -> $ iconstf n
......@@ -74,9 +74,9 @@ module Compile_bexpr
meta rewrite_def function exec_cond
let rec compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) : hl 'a
ensures { let len = result.code.length in
result <% (trivial_pre,bexpr_post b cond (len + ofs) len) }
ensures { hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> let len = result.code.length in
bexpr_post b cond (len + ofs) len }
variant { b }
= let c = match b with
| Btrue -> $ if cond then ibranchf ofs else inil ()
......@@ -164,9 +164,8 @@ module Compile_com
(forall pk sk mk. var (VMS pk sk mk) (VMS pi si mi) -> mk = mj)
let rec compile_com (cmd: com) : hl 'a
ensures { hl_correctness result }
ensures { let len = result.code.length in
result <% (com_pre cmd,com_post cmd len) }
ensures { result.pre --> com_pre cmd }
ensures { result.post --> let len = result.code.length in com_post cmd len }
variant { cmd }
= let res = match cmd with
| Cskip -> $ inil ()
......
This diff is collapsed.
......@@ -4,62 +4,62 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../imp.why">
<theory name="Imp" sum="2d3400b438aea0519cb1313c5cfda33e">
<theory name="Imp" sum="4a862357dfae5a0041230517e577addf">
<goal name="ceval_deterministic_aux">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.1.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.2" expl="2.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.2.1" expl="1.">
<proof prover="0"><result status="valid" time="0.33" steps="473"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="224"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.3" expl="3.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.3.1" expl="1.">
<proof prover="0"><result status="valid" time="0.23" steps="391"/></proof>
<proof prover="0"><result status="valid" time="0.23" steps="384"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.4" expl="4.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.4.1" expl="1.">
<proof prover="0"><result status="valid" time="0.06" steps="157"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="146"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.5" expl="5.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.5.1" expl="1.">
<proof prover="0"><result status="valid" time="0.06" steps="153"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.6" expl="6.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.6.1" expl="1.">
<proof prover="0"><result status="valid" time="0.03" steps="50"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.7" expl="7.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.7.1" expl="1.">
<proof prover="0"><result status="valid" time="0.28" steps="444"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="405"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic">
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
</theory>
</file>
......
......@@ -32,19 +32,15 @@ module Compiler_logic
type pre 'a = 'a -> pos -> pred
type post 'a = 'a -> pos -> rel
(* Machine transition valid whatever the global code is. *)
predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2
(* Hoare triples with explicit pre & post *)
type hl 'a = { code: code; ghost pre : pre {'a}; ghost post: post {'a} }
(* (<%): pack the pre/post rewriting.
lock is an artifact to prevent unrolling of
h's definition recursively. *)
let function lock () : (int,int) =
ensures { result = (0,0) }
while false do variant { 0 } () done; (0,0)
predicate (<%) (h:hl 'a) (x:(pre 'a,post 'a)) =
let (pr,ps) = x in
h --> { code = let (_,_) = lock () in h.code; pre = pr; post = ps }
meta rewrite_def predicate (<%)
(* (Total) correctness for hoare triple. *)
invariant { forall x:'a,p ms. pre x p ms ->
exists ms'. post x p ms ms' /\ contextual_irrelevance code p ms ms' }
(* Predicate transformer type. Same auxiliary variables as for
Hoare triples. *)
......@@ -52,20 +48,9 @@ module Compiler_logic
(* Code with backward predicate transformer. *)
type wp 'a = { wcode : code; ghost wp : wp_trans {'a} }
(* Machine transition valid whatever the global code is. *)
predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2
(* (Total) correctness for hoare triple. *)
predicate hl_correctness (cs:hl 'a) =
forall x:'a,p ms. cs.pre x p ms ->
exists ms'. cs.post x p ms ms' /\ contextual_irrelevance cs.code p ms ms'
(* Similar definition for backward predicate transformers *)
predicate wp_correctness (code:wp 'a) =
forall x:'a,p post ms. (code.wp x p post) ms ->
exists ms'. post ms' /\ contextual_irrelevance code.wcode p ms ms'
(* Similar invariant for backward predicate transformers *)
invariant { forall x:'a,p post ms. wp x p post ms ->
exists ms'. post ms' /\ contextual_irrelevance wcode p ms ms' }
(* WP combinator for sequence. Similar to the standard WP calculus
for sequence. The initial machine state is memorized in auxiliary
......@@ -81,10 +66,8 @@ module Compiler_logic
(* Code combinator for sequence, with wp. *)
let (--) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a
requires { wp_correctness s1 /\ wp_correctness s2 }
ensures { result.wcode.length = s1.wcode.length + s2.wcode.length }
ensures { result.wcode.length --> s1.wcode.length + s2.wcode.length }
ensures { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp }
ensures { wp_correctness result }
= let code = s1.wcode ++ s2.wcode in
let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
assert { forall x: 'a, p post ms. res.wp x p post ms ->
......@@ -106,9 +89,8 @@ module Compiler_logic
Similar to WP calculus for (if cond then s). *)
let (%) (s:wp 'a) (ghost cond:pre {'a}) : wp 'a
requires { wp_correctness s }
ensures { result.wp --> fork_wp s.wp cond }
ensures { result.wcode.length = s.wcode.length /\ wp_correctness result }
ensures { result.wcode.length --> s.wcode.length }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
(* WP transformer for hoare triples. *)
......@@ -118,26 +100,23 @@ module Compiler_logic
lemma towp_wp_lemma:
forall pr ps, x:'a, p q ms. towp_wp pr ps x p q ms =
(pr x p ms && (forall ms'. ps x p ms ms' -> q ms'))
meta rewrite lemma towp_wp_lemma
(* Unwrap code with hoare triple into code with wp.
Analogous to procedure call/abstract block. *)
let ($_) (c:hl 'a) : wp 'a
requires { hl_correctness c }
ensures { result.wcode.length = c.code.length }
ensures { result.wcode.length --> c.code.length }
ensures { result.wp --> towp_wp c.pre c.post }
ensures { wp_correctness result }
= { wcode = c.code; wp = towp_wp c.pre c.post }