Commit 56ad0489 authored by MARCHE Claude's avatar MARCHE Claude

prover: add some missing variants

parent 667b8168
......@@ -16,19 +16,19 @@
go back to the instant t. *)
module Types
use import int.Int
use import array.Array
use import list.List
use import Functions.Func
use import Predicates.Pred
type timestamp 'a = {
time : int ;
size : int ;
ghost table : func int (list 'a) ;
}
type t 'a = {
(* (-1) mean array resizing (doubling in size), i >= 0 mean
update at case i. *)
......@@ -38,11 +38,11 @@ module Types
(* Invariant of stored data. *)
ghost inv : pred 'a ;
}
end
module Logic
use import Types
use import int.Int
use import int.ComputerDivision
......@@ -51,26 +51,26 @@ module Logic
use import list.List
use import Functions.Func
use import Choice.Choice
function func_of_array (a:array ~'a) (def:'a) : func int 'a
axiom func_of_array_def : forall a:array 'a,def:'a,x:int.
func_of_array a def x = if (0 <= x < a.length)
then M.get a.elts x
else def
function current_timestamp (x:t ~'a) : timestamp 'a =
{ time = x.current_time ;
size = x.buffer.length ;
table = func_of_array x.buffer Nil ; }
predicate correct_table (sz:int) (b:func int (list 'a)) =
forall x:int. x >= sz \/ x < 0 -> b x = Nil
function pop (l:list 'a) : list 'a = match l with
| Nil -> default
| Cons x q -> q
end
function unroll (tm:int) (t0:int) (h:list int) (b:func int (list 'a))
(sz:int) : timestamp 'a =
if tm = 0
......@@ -81,7 +81,7 @@ module Logic
then unroll (tm-1) t0 q b (div sz 2)
else unroll (tm-1) t0 q (b[x <- pop (b x)]) sz
end
predicate unroll_correct (tm:int) (h:list int) (b:func int (list 'a)) (sz:int)
= match h with
| Nil -> tm = 0
......@@ -92,23 +92,23 @@ module Logic
else b x <> Nil /\ 0 <= x < sz
/\ unroll_correct (tm-1) q (b[x <- pop (b x)]) sz
end
predicate past_time (t:timestamp 'a) (tb:t 'a) =
tb.current_time >= t.time /\
unroll (tb.current_time - t.time) t.time
tb.history (func_of_array tb.buffer Nil) tb.buffer.length = t
predicate precede (tb1:t 'a) (tb2:t 'a) =
forall t:timestamp 'a. past_time t tb1 -> past_time t tb2
predicate before (t1 t2:timestamp 'a) =
t1.time <= t2.time
predicate list_forall (p:pred 'a) (l:list 'a) = match l with
| Nil -> true
| Cons x q -> p x /\ list_forall p q
end
predicate correct (tb:t 'a) =
(forall t:timestamp 'a. past_time t tb -> t.size > 0) /\
(forall t:timestamp 'a,i:int.
......@@ -117,7 +117,7 @@ module Logic
past_time t tb -> correct_table t.size t.table) /\
unroll_correct tb.current_time tb.history
(func_of_array tb.buffer Nil) tb.buffer.length
(* I MUST INTRODUCE THIS PREDICATE FOR ONLY ONE REASON :
ABUSIVE RECORD DECONSTRUCTION IN ASSERTIONS. *)
predicate backtrack_to (tbold:t 'a) (tbinter:t 'a) (tbnew:t 'a) =
......@@ -129,11 +129,11 @@ module Logic
&& past_time tm tbnew) && (forall tm:timestamp 'a.
past_time tm tbold -> past_time tm tbnew) &&
precede tbold tbnew
end
module Impl
use import Types
use import Logic
use import int.Int
......@@ -144,14 +144,14 @@ module Impl
use import Functions.Func
use import Predicates.Pred
use import Choice.Choice
(* extraction trick to speedup integer operations with
constants. *)
constant mone : int = -1
constant zero : int = 0
constant one : int = 1
constant two : int = 2
let create (ghost p:pred ~'a) : t 'a
ensures { forall t:timestamp 'a.
past_time t result -> t.table = const Nil }
......@@ -167,8 +167,8 @@ module Impl
} in
assert { extensionalEqual (func_of_array res.buffer Nil) (const Nil) } ;
res
(* Internal utility (break some of the invariants),
but useful in practice. *)
let add_event (x:int) (tb:t 'a) : unit
......@@ -178,8 +178,8 @@ module Impl
=
tb.history <- Cons x tb.history ;
tb.current_time <- tb.current_time + one
(* Internal utility. *)
let resize_for (x:int) (tb:t ~'a) : unit
writes { tb }
......@@ -208,6 +208,8 @@ module Impl
tbc.current_time = tb.current_time /\
func_of_array tbc.buffer Nil = func_of_array tb.buffer Nil }
requires { tbc.buffer.length = size }
variant { x - size }
writes { tb.history,tb.current_time,tbc.history,tbc.current_time,tbc.buffer }
ensures { correct tbc }
ensures { tbc.history = tb.history /\
tbc.current_time = tb.current_time /\
......@@ -216,8 +218,6 @@ module Impl
ensures { result > x }
ensures { result >= size }
ensures { precede (old tbc) tbc }
writes { tb.history,tb.current_time,tbc.history,tbc.current_time,tbc.buffer }
variant { x - size }
=
'AuxInit:
assert { past_time (current_timestamp tbc) tbc } ;
......@@ -246,7 +246,7 @@ module Impl
assert { extensionalEqual (func_of_array buf1 Nil)
(func_of_array buf2 Nil) } ;
tb.buffer <- buf2
let iadd (x:int) (b:'a) (tb:t 'a) : unit
writes { tb.history,tb.current_time,tb.buffer.elts }
requires { 0 <= x < tb.buffer.length }
......@@ -271,7 +271,7 @@ module Impl
assert { forall t:timestamp 'a.
past_time t tb <-> past_time t (at tb 'Init) \/ t = current_timestamp tb } ;
assert { precede (at tb 'Init) tb }
let add (x:int) (b:'a) (tb:t ~'a) : unit
writes { tb, tb.buffer.elts }
requires { correct tb }
......@@ -286,8 +286,8 @@ module Impl
if x >= length tb.buffer
then resize_for x tb ;
iadd x b tb
let get (tb:t 'a) (x:int) : list 'a
requires { correct tb }
requires { x >= 0 }
......@@ -298,7 +298,7 @@ module Impl
then Nil
else let res = tb.buffer[x] in
(assert { res = table (current_timestamp tb) x } ; res )
let backtrack (t:timestamp 'a) (tb:t 'a) : unit
writes { tb,tb.buffer.elts }
requires { past_time t tb }
......@@ -318,7 +318,6 @@ module Impl
inv = tb.inv ;
} in
let rec unroll (delta:int) : unit
writes { tb.history,tb.buffer.elts,tbc,tbc.buffer.elts }
requires { correct tbc }
requires { past_time t tbc }
requires { delta >= 0 }
......@@ -327,6 +326,8 @@ module Impl
(forall x:int. 0 <= x < final_size /\ x < tbc.buffer.length ->
func_of_array tbc.buffer Nil x = func_of_array tb.buffer Nil x) }
requires { tb.buffer.length <= final_size }
variant { delta }
writes { tb.history,tb.buffer.elts,tbc,tbc.buffer.elts }
ensures { correct tbc }
ensures { tbc.history = tb.history /\
(forall x:int. 0 <= x < final_size ->
......@@ -337,7 +338,6 @@ module Impl
ensures { precede tbc (old tbc) }
ensures { forall t2:timestamp 'a. before t2 t /\ past_time t2 (old tbc) ->
past_time t2 tbc }
variant { delta }
=
'UInit:
if delta <> zero
......@@ -416,10 +416,10 @@ module Impl
unroll (tm0 - t.time) ;
assert { extensionalEqual (func_of_array tb.buffer Nil)
(func_of_array tbc.buffer Nil) }
val ghost hack_func_of_array (a:array ~'a) (def:'a) : func int 'a
ensures { result = func_of_array a def }
let stamp (tb:t ~'a) : timestamp 'a
requires { correct tb }
ensures { result = current_timestamp tb }
......@@ -429,9 +429,8 @@ module Impl
size = length tb.buffer ;
table = hack_func_of_array tb.buffer Nil ;
}
(* look for the correct syntax :
meta "remove_program" val hack_func_of_array*)
end
end
......@@ -8,17 +8,17 @@ module Types
use import Firstorder_symbol_spec.Spec
type nl_symbol 'b0 = | NLFVar_symbol 'b0
| NLBruijn_symbol int
type nlimpl_symbol =
{ nlrepr_symbol_field : nl_symbol int ;
nlfree_var_symbol_set_abstraction_symbol_field : int ;
ghost model_symbol_field : symbol int ;
}
type cons_symbol = | NLCVar_symbol int
end
module Logic
......@@ -34,15 +34,15 @@ module Logic
match t with | NLFVar_symbol v0 -> one_nat
| NLBruijn_symbol v0 -> one_nat
end
with nlsize_symbol (t:nl_symbol 'b0) : int =
match t with | NLFVar_symbol v0 -> 1 | NLBruijn_symbol v0 -> 1 end
let rec lemma nlsize_positive_lemma_symbol (t:nl_symbol 'b0) : unit
ensures { nlsize_symbol t > 0 }
variant { nat_to_int (nat_nlsize_symbol t) } =
match t with | NLFVar_symbol v0 -> () | NLBruijn_symbol v0 -> () end
(* Abstraction definition axiom :
function shiftb_symbol (bnd:func int (symbol 'b0)) :
func int (symbol (option 'b0)) =
......@@ -54,7 +54,7 @@ module Logic
forall bnd:func int (symbol 'b0), i:int.
eval (shiftb_symbol bnd) i =
if i = 0 then Var_symbol None else rename_symbol (bnd (i-1)) some
let lemma shiftb_compose_lemma_symbol (bnd:func int (symbol 'b0))
(s0:func 'b0 (symbol 'c0)) : unit
ensures { subst_compose_symbol (shiftb_symbol bnd) (olifts_symbol s0) =
......@@ -70,12 +70,12 @@ module Logic
(subst_compose_symbol (shiftb_symbol bnd) (olifts_symbol s0))
(shiftb_symbol (subst_compose_symbol bnd s0))
}
function nlmodel_symbol (t:nl_symbol 'b0) (fr0:func 'b0 (symbol 'c0))
(bnd0:func int (symbol 'c0)) : symbol 'c0 =
match t with | NLFVar_symbol v0 -> fr0 v0 | NLBruijn_symbol v0 -> bnd0 v0
end
let rec lemma nlmodel_subst_commutation_lemma_symbol (t:nl_symbol 'b0)
(fr0:func 'b0 (symbol 'c0)) (bnd0:func int (symbol 'c0))
(s0:func 'c0 (symbol 'd0)) : unit
......@@ -85,7 +85,7 @@ module Logic
= subst_symbol (nlmodel_symbol t fr0 bnd0) s0 }
variant { nlsize_symbol t } =
match t with | NLFVar_symbol v0 -> () | NLBruijn_symbol v0 -> () end
let lemma nlmodel_rename_commutation_lemma_symbol (t:nl_symbol 'b0)
(fr0:func 'b0 (symbol 'c0)) (bnd0:func int (symbol 'c0))
(s0:func 'c0 'd0) : unit
......@@ -96,20 +96,20 @@ module Logic
=
nlmodel_subst_commutation_lemma_symbol t fr0 bnd0
(subst_of_rename_symbol s0)
predicate correct_indexes_symbol (t:nl_symbol 'b0) =
match t with | NLFVar_symbol v0 -> true | NLBruijn_symbol v0 -> v0 >= 0
end
function bound_depth_of_symbol_in_symbol (t:nl_symbol 'b0) : int =
match t with | NLFVar_symbol v0 -> 0 | NLBruijn_symbol v0 -> 1 + v0 end
let rec lemma bound_depth_of_symbol_in_symbol_nonnegative
(t:nl_symbol 'b0) : unit requires { correct_indexes_symbol t }
ensures { bound_depth_of_symbol_in_symbol t >= 0 }
variant { nlsize_symbol t } =
match t with | NLFVar_symbol v0 -> () | NLBruijn_symbol v0 -> () end
let rec lemma model_equal_symbol (t:nl_symbol 'b0)
(fr10:func 'b0 (symbol 'c0)) (fr20:func 'b0 (symbol 'c0))
(bnd10:func int (symbol 'c0)) (bnd20:func int (symbol 'c0)) : unit
......@@ -121,7 +121,7 @@ module Logic
ensures { nlmodel_symbol t fr10 bnd10 = nlmodel_symbol t fr20 bnd20 }
variant { nlsize_symbol t } =
match t with | NLFVar_symbol v0 -> () | NLBruijn_symbol v0 -> () end
predicate nlimpl_symbol_ok (t:nlimpl_symbol) =
nlmodel_symbol t.nlrepr_symbol_field subst_id_symbol
(const (Var_symbol ((-1)))) = t.model_symbol_field
......@@ -129,19 +129,19 @@ module Logic
bound_depth_of_symbol_in_symbol t.nlrepr_symbol_field = 0 /\
(forall x:int. is_symbol_free_var_in_symbol x t.model_symbol_field -> (x)
< (t.nlfree_var_symbol_set_abstraction_symbol_field))
predicate cons_ok_symbol (c:cons_symbol) =
match c with | NLCVar_symbol v0 -> true end
predicate cons_rel_symbol (c:cons_symbol) (t:nlimpl_symbol) =
match c with | NLCVar_symbol v0 -> t.model_symbol_field = Var_symbol v0
end
predicate cons_open_rel_symbol (c:cons_symbol) (t:nlimpl_symbol) =
match c with | NLCVar_symbol v0 -> t.model_symbol_field = Var_symbol v0
end
end
module Impl
......@@ -168,7 +168,7 @@ module Impl
if v0 = x then NLBruijn_symbol i else NLFVar_symbol v0
| NLBruijn_symbol v0 -> NLBruijn_symbol v0
end
let rec unbind_var_symbol_in_symbol (t:nl_symbol int) (i:int)
(x:nl_symbol int) (ghost fr0:func int (symbol 'b0))
(ghost bnd10:func int (symbol 'b0)) (ghost bnd20:func int (symbol 'b0)) :
......@@ -186,8 +186,8 @@ module Impl
if v0 = i then (model_equal_symbol x fr0 fr0 bnd10 bnd20 ; x)
else NLBruijn_symbol v0
end
let rec subst_base_symbol_in_symbol (t:nl_symbol int) (x:int)
let subst_base_symbol_in_symbol (t:nl_symbol int) (x:int)
(u:nl_symbol int) (ghost fr0:func int (symbol 'b0))
(ghost bnd10:func int (symbol 'b0)) (ghost bnd20:func int (symbol 'b0)) :
nl_symbol int requires { correct_indexes_symbol t }
......@@ -205,7 +205,7 @@ module Impl
else NLFVar_symbol v0
| NLBruijn_symbol v0 -> NLBruijn_symbol v0
end
let construct_symbol (c:cons_symbol) : nlimpl_symbol
requires { cons_ok_symbol c } ensures { nlimpl_symbol_ok result }
ensures { cons_rel_symbol c result }
......@@ -217,7 +217,7 @@ module Impl
model_symbol_field = ghost (Var_symbol v0) ;
}
end
let destruct_symbol (t:nlimpl_symbol) : cons_symbol
requires { nlimpl_symbol_ok t } ensures { cons_ok_symbol result }
ensures { cons_rel_symbol result t }
......@@ -226,7 +226,7 @@ module Impl
match t.nlrepr_symbol_field with | NLFVar_symbol v0 -> NLCVar_symbol v0
| NLBruijn_symbol v0 -> absurd
end
let nlsubst_symbol_in_symbol (t:nlimpl_symbol) (x:int) (u:nlimpl_symbol) :
nlimpl_symbol requires { nlimpl_symbol_ok t }
requires { nlimpl_symbol_ok u } ensures { nlimpl_symbol_ok result }
......@@ -286,8 +286,6 @@ module Impl
&& (x2) < (res.nlfree_var_symbol_set_abstraction_symbol_field)
} ;
res
end
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment