Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 3a716828 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

lemma functions

a lemma function is introduced with 'let lemma f' or 'let rec lemma f'
it is a ghost function
it must have return type unit and read-only effects
it introduces a goal (its WP), followed by an axiom
  forall args/reads, precondition => postcondition
parent c1537ce3
......@@ -1080,9 +1080,9 @@ new_pdecl:
;
pdecl:
| LET ghost lident_rich labels fun_defn
| LET top_ghost lident_rich labels fun_defn
{ Dlet (add_lab $3 $4, $2, $5) }
| LET ghost lident_rich labels EQUAL fun_expr
| LET top_ghost lident_rich labels EQUAL fun_expr
{ Dlet (add_lab $3 $4, $2, $6) }
| LET REC list1_rec_defn
{ Dletrec $3 }
......@@ -1130,7 +1130,7 @@ list1_rec_defn:
;
rec_defn:
| ghost lident_rich labels list1_binder opt_cast spec EQUAL spec expr
| top_ghost lident_rich labels list1_binder opt_cast spec EQUAL spec expr
{ floc (), add_lab $2 $3, $1, $4, (cast_body $5 $9, spec_union $6 $8) }
;
......@@ -1454,6 +1454,12 @@ ghost:
| GHOST { true }
;
top_ghost:
| /* epsilon */ { Gnone }
| GHOST { Gghost }
| LEMMA { Glemma }
;
/*
Local Variables:
compile-command: "unset LANG; make -C ../.."
......
......@@ -46,6 +46,7 @@ type pty =
| PPTtuple of pty list
type ghost = bool
type top_ghost = Gnone | Gghost | Glemma
type binder = loc * ident option * ghost * pty option
type param = loc * ident option * ghost * pty
......@@ -242,12 +243,12 @@ and expr_desc =
| Eabstract of triple
| Enamed of label * expr
and letrec = loc * ident * ghost * binder list * triple
and letrec = loc * ident * top_ghost * binder list * triple
and triple = expr * spec
type pdecl =
| Dlet of ident * ghost * expr
| Dlet of ident * top_ghost * expr
| Dletrec of letrec list
| Dparam of ident * ghost * type_v
| Dexn of ident * pty
......
......@@ -327,19 +327,14 @@ let pdecl_ns uc d = match d.pd_node with
| PDrec fdl -> List.fold_left add_rec uc fdl
| PDexn xs -> add_exn uc xs
(* FIXME: move the choice to Mlw_wp and make it dynamic, not start-time *)
let if_fast_wp f1 f2 x = if Debug.test_flag Mlw_wp.fast_wp then f1 x else f2 x
let wp_val = if_fast_wp Mlw_wp.fast_wp_val Mlw_wp.wp_val
let wp_let = if_fast_wp Mlw_wp.fast_wp_let Mlw_wp.wp_let
let wp_rec = if_fast_wp Mlw_wp.fast_wp_rec Mlw_wp.wp_rec
let pdecl_vc env km th d = match d.pd_node with
let pdecl_vc ~wp env km th d = match d.pd_node with
| PDtype _ | PDdata _ | PDexn _ -> th
| PDval lv -> wp_val env km th lv
| PDlet ld -> wp_let env km th ld
| PDrec rd -> wp_rec env km th rd
| PDval lv -> Mlw_wp.wp_val ~wp env km th lv
| PDlet ld -> Mlw_wp.wp_let ~wp env km th ld
| PDrec rd -> Mlw_wp.wp_rec ~wp env km th rd
let pdecl_vc uc d = add_to_theory (pdecl_vc uc.muc_env uc.muc_known) uc d
let pdecl_vc ~wp uc d =
add_to_theory (pdecl_vc ~wp uc.muc_env uc.muc_known) uc d
let pure_data_decl tdl =
let proj pj = Opt.map (fun pls -> pls.pl_ls) pj in
......@@ -359,7 +354,7 @@ let add_pdecl ~wp uc d =
muc_local = Sid.union uc.muc_local d.pd_news }
in
let uc = pdecl_ns uc d in
let uc = if wp then pdecl_vc uc d else uc in
let uc = pdecl_vc ~wp uc d in
let uc = add_to_theory pdecl_pure uc d in
uc
......
......@@ -579,6 +579,15 @@ let eff_is_empty e =
(* eff_compar is not a side effect *)
not e.eff_diverg
let eff_is_read_only e =
Sreg.is_empty e.eff_writes &&
Sexn.is_empty e.eff_raises &&
Sreg.is_empty e.eff_ghostw &&
Sexn.is_empty e.eff_ghostx &&
Mreg.is_empty e.eff_resets &&
(* eff_compar is not a side effect *)
not e.eff_diverg
let eff_equal e1 e2 =
Sreg.equal e1.eff_reads e2.eff_reads &&
Sreg.equal e1.eff_writes e2.eff_writes &&
......
......@@ -237,6 +237,7 @@ val eff_full_inst : ity_subst -> effect -> effect
val eff_filter : varset -> effect -> effect
val eff_is_empty : effect -> bool
val eff_is_read_only: effect -> bool
(** specification *)
......
......@@ -484,6 +484,13 @@ and dtype_v denv = function
(* expressions *)
let add_lemma_label ~top id = function
| Gnone -> id, false
| Gghost -> id, true
| Glemma when not top ->
errorm ~loc:id.id_loc "lemma functions are only allowed at toplevel"
| Glemma -> { id with id_lab = Lstr Mlw_wp.lemma_label :: id.id_lab }, true
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
let de_app _loc e el =
......@@ -561,7 +568,7 @@ and de_desc denv loc = function
let e2 = dexpr denv e2 in
DElet (id, gh, e1, e2), e2.de_type
| Ptree.Eletrec (fdl, e1) ->
let fdl = dletrec denv fdl in
let fdl = dletrec ~top:false denv fdl in
let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
let denv = List.fold_left add_one denv fdl in
let e1 = dexpr denv e1 in
......@@ -727,7 +734,7 @@ and de_desc denv loc = function
expected_type e1 dity_unit;
DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
and dletrec denv fdl =
and dletrec ~top denv fdl =
(* add all functions into the environment *)
let add_one denv (_,id,_,bl,_) =
let argl = List.map (fun _ -> create_type_variable ()) bl in
......@@ -742,6 +749,7 @@ and dletrec denv fdl =
let denvl = List.map2 bind_one fdl dvtyl in
(* then type-check the bodies *)
let type_one (loc,id,gh,_,tr) (denv,bl,tyl,tyv) =
let id, gh = add_lemma_label ~top id gh in
let tr, (argl, res) = dtriple denv tr in
if argl <> [] then errorm ~loc
"The body of a recursive function must be a first-order value";
......@@ -943,8 +951,8 @@ and rletrec denv fdl =
let dexpr denv e =
rexpr denv (dexpr denv e)
let dletrec denv fdl =
rletrec denv (dletrec denv fdl)
let dletrec ~top denv fdl =
rletrec denv (dletrec ~top denv fdl)
(** stage 2 *)
......@@ -2031,6 +2039,7 @@ let add_decl ~wp loc uc d =
let add_pdecl ~wp loc uc = function
| Dlet (id, gh, e) ->
let id, gh = add_lemma_label ~top:true id gh in
let e = dexpr (create_denv uc) e in
let pd = match e.de_desc with
| DEfun (bl, tr) ->
......@@ -2044,7 +2053,7 @@ let add_pdecl ~wp loc uc = function
create_let_decl def in
add_pdecl_with_tuples ~wp uc pd
| Dletrec fdl ->
let fdl = dletrec (create_denv uc) fdl in
let fdl = dletrec ~top:true (create_denv uc) fdl in
let fdl = expr_rec (create_lenv uc) fdl in
let pd = create_rec_decl fdl in
add_pdecl_with_tuples ~wp uc pd
......
......@@ -28,6 +28,8 @@ let no_track = Debug.register_flag "wp_no_track"
let no_eval = Debug.register_flag "wp_no_eval"
~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."
let lemma_label = Ident.create_label "why3:lemma"
(** Marks *)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
......@@ -1134,3 +1136,50 @@ let fast_wp_rec env km th fdl =
List.fold_left2 add_one th fdl fl
let fast_wp_val _env _km th _lv = th
(* Select either traditional or fast WP *)
let if_fast_wp f1 f2 x = if Debug.test_flag fast_wp then f1 x else f2 x
let wp_val = if_fast_wp fast_wp_val wp_val
let wp_let = if_fast_wp fast_wp_let wp_let
let wp_rec = if_fast_wp fast_wp_rec wp_rec
(* Lemma functions *)
let wp_val ~wp env kn th ls = if wp then wp_val env kn th ls else th
let wp_let ~wp env kn th ld = if wp then wp_let env kn th ld else th
let wp_rec ~wp env kn th fdl =
let th = if wp then wp_rec env kn th fdl else th in
let add_one th { fun_ps = ps; fun_lambda = l } =
let name = ps.ps_name in
if Slab.mem lemma_label name.id_label then
let loc = name.id_loc in
let spec = ps.ps_aty.aty_spec in
if not (eff_is_read_only spec.c_effect) then
Loc.errorm ?loc "lemma functions can not have effects";
if not (ity_equal (ity_of_expr l.l_expr) ity_unit) then
Loc.errorm ?loc "lemma functions must return unit";
let env = mk_env env kn th in
let lab = fresh_mark () in
let add_arg sbs pv = ity_match sbs pv.pv_ity pv.pv_ity in
let subst = List.fold_left add_arg ps.ps_subst l.l_args in
let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
let args = List.map (fun pv -> pv.pv_vs) l.l_args in
let q = old_mark lab spec.c_post in
let f = wp_expr env e_void q Mexn.empty in
let f = wp_implies spec.c_pre (erase_mark lab f) in
let f = wp_forall args (quantify env regs f) in
let f = t_forall_close (Mvs.keys f.t_vars) [] f in
let lkn = Theory.get_known th in
let f = if Debug.test_flag no_track then f else track_values lkn kn f in
let f = if Debug.test_flag no_eval then f else
Eval_match.eval_match ~inline:Eval_match.inline_nonrec_linear lkn f in
let pr = create_prsymbol (id_clone name) in
let d = create_prop_decl Paxiom pr f in
Theory.add_decl th d
else
th
in
List.fold_left add_one th fdl
......@@ -17,6 +17,8 @@ open Mlw_expr
(** WP-only builtins *)
val lemma_label : Ident.label
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
......@@ -39,16 +41,11 @@ val full_invariant :
(** Weakest preconditions *)
val wp_val: Env.env -> known_map -> theory_uc -> let_sym -> theory_uc
val wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
(** Efficient weakest preconditions *)
val fast_wp: Debug.flag
val wp_val:
wp:bool -> Env.env -> known_map -> theory_uc -> let_sym -> theory_uc
val wp_let:
wp:bool -> Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val wp_rec:
wp:bool -> Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
val fast_wp_val: Env.env -> known_map -> theory_uc -> let_sym -> theory_uc
val fast_wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val fast_wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
module LemmaFunction1
use import int.Int
use import ref.Refint
function fact int : int
axiom fact0 : fact 0 = 1
axiom factn : forall n: int. n > 0 -> fact n = n * fact (n - 1)
let rec lemma f (n: int) : unit variant {n}
requires { n >= 0 }
ensures { fact n >= 1 }
=
if n > 0 then f (n-1)
goal g: fact 42 >= 1
end
module LemmaFunction2
use import int.Int
use import array.Array
use import array.ArraySum
let rec lemma sum_nonneg (a: array int) (l u: int) : unit
requires { 0 <= l <= u <= length a }
requires { forall i: int. 0 <= i < length a -> a[i] >= 0 }
variant { u-l }
ensures { sum a l u >= 0 }
=
if u > l then sum_nonneg a (l+1) u
goal g1:
forall a: array int.
(forall i: int. 0 <= i < length a -> a[i] >= 0) ->
sum a 0 (length a) >= 0
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