Commit d0fdf426 authored by Martin Clochard's avatar Martin Clochard
Browse files

(WIP) Formalisation de la logique de Why3/API: refonte en cours

parent e88d56f8
module Ctx
(* Variable contexts. *)
use import support.HO
type context 'p 'l
function c_ldom (context 'p 'l) : 'l -> bool
function c_pdom (context 'p 'l) : 'p -> bool
function c_ltp (context 'p 'l) : 'l -> 'p
function c_ptl (context 'p 'l) : 'p -> 'l
axiom context_inv : forall c:context 'p 'l.
maps_to c.c_ldom c.c_ltp c.c_pdom /\
maps_to c.c_pdom c.c_ptl c.c_ldom /\
(forall x. c.c_ldom x -> c.c_ptl (c.c_ltp x) = x) /\
(forall x. c.c_pdom x -> c.c_ltp (c.c_ptl x) = x)
predicate context_inj (c1:context 'p 'l1) (f:'l1 -> 'l2) (c2:context 'p 'l2) =
forall x. c1.c_pdom x -> c2.c_pdom x /\ c2.c_ptl x = f (c1.c_ptl x)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../context.mlw" expanded="true">
<theory name="Ctx" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
</file>
</why3session>
module Not_found
exception Not_found
end
module FMap
use import support.HO
use import support.Finite
use import Not_found
use import option.Option
use mach.peano.Peano as P
(* Program representation of a key. *)
type key
(* Logic representation of a key. The model projection need to be known
here to recover the right modelisation as the assocation maps
depends only on that part of the key. *)
type key_l
function k_m key : key_l
(* Finite associaton table. *)
type t 'a
function domain (t 'a) : key_l -> bool
function bindings (t 'a) : key_l -> 'a
axiom t_inv : forall m:t 'a. finite m.domain
(* Immediate implementation of sets on top of fmap. *)
type s = t unit
val empty () : t 'a
ensures { result.domain = none }
val is_empty (m:t 'a) : bool
ensures { result -> m.domain = none }
ensures { forall x. m.domain x -> not result }
val mem (x:key) (m:t 'a) : bool
ensures { result <-> m.domain (k_m x) }
val add (x:key) (b:'a) (m:t 'a) : t 'a
ensures { result.domain = update m.domain x.k_m true }
ensures { result.bindings = update m.bindings x.k_m b }
val singleton (x:key) (b:'a) : t 'a
ensures { result.domain = update none x.k_m true }
ensures { result.bindings x.k_m = b }
val remove (x:key) (m:t 'a) : t 'a
ensures { result.domain = update m.domain x.k_m false }
ensures { result.bindings = m.bindings }
val cardinal (m:t 'a) : P.t
ensures { finite m.domain }
ensures { result.P.v = cardinal m.domain }
val find (x:key) (m:t 'a) : 'a
ensures { m.domain x.k_m /\ m.bindings x.k_m = result }
raises { Not_found -> not m.domain x.k_m }
val set_union (m1 m2:t 'a) : t 'a
ensures { forall x. result.domain x <-> m1.domain x \/ m2.domain x }
ensures { result.bindings = ho_ite m1.domain m1.bindings m2.bindings }
val set_inter (m1 m2:t 'a) : t 'a
ensures { forall x. result.domain x <-> m1.domain x /\ m2.domain x }
ensures { result.bindings = m1.bindings }
val set_diff (m1 m2:t 'a) : t 'a
ensures { forall x. result.domain x <-> m1.domain x /\ not m2.domain x }
ensures { result.bindings = m1.bindings }
val set_submap (m1 m2:t 'a) : bool
ensures { result <-> subset m1.domain m2.domain }
val set_disjoint (m1 m2:t 'a) : bool
ensures { result <-> forall x. not (m1.domain x /\ m2.domain x) }
val set_equal (m1 m2:t 'a) : bool
ensures { result -> m1.domain = m2.domain }
ensures { forall x. m1.domain x <> m2.domain x -> not result }
val find_def (d:'a) (x:key) (m:t 'a) : 'a
ensures { m.domain x.k_m -> result = m.bindings x.k_m }
ensures { not m.domain x.k_m -> result = d }
val find_opt (x:key) (m:t 'a) : option 'a
ensures { m.domain x.k_m -> result = Some (m.bindings x.k_m) }
ensures { not m.domain x.k_m -> result = None }
ensures { match result with
| None -> not m.domain x.k_m
| Some u -> u = m.bindings x.k_m
end }
val domain (m:t 'a) : s
ensures { result.domain = m.domain }
val is_num_elt (n:P.t) (m:t 'a) : bool
ensures { finite m.domain }
ensures { result <-> cardinal m.domain = n.P.v }
type enumeration 'a
function e_domain (enumeration 'a) : key_l -> bool
function e_bindings (enumeration 'a) : key_l -> 'a
function e_first (enumeration 'a) : key_l
axiom e_inv : forall e:enumeration 'a.
not e.e_domain e.e_first -> e.e_domain = none
val val_enum (e:enumeration 'a) : option (key,'a)
ensures { match result with
| None -> e.e_domain = none
| Some (k0,v) -> k0.k_m = e.e_first /\ v = e.e_bindings k0.k_m /\
e.e_domain k0.k_m
end }
val start_enum (m:t 'a) : enumeration 'a
ensures { result.e_domain = m.domain }
ensures { result.e_bindings = m.bindings }
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../extmap.mlw" expanded="true">
<theory name="Not_found" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="FMap" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
</file>
</why3session>
(* Very, very abstract views of strings & Why3 locations:
they are. *)
module String
type string
end
module Loc
type position
end
module Label
use import String
use import Loc
type label model { lab_string : string }
val lab_equal (l1 l2:label) : bool
ensures { result -> l1 = l2 }
ensures { l1.lab_string = l2.lab_string -> result }
val create_label (s:string) : label
ensures { result.lab_string = s }
val lab_string (l:label) : string
ensures { result = l.lab_string }
clone extmap.FMap as Mlab with
type key = label,
type key_l = string,
function k_m = lab_string
end
module Ident
use import int.Int
use import String
use import Loc
use import Label
use import option.Option
use import list.List
use import support.HO
(* Abstract name type. *)
type ident_name
(* Not present in Why3: ghost information allowing to know the
identifier class.
Justification: Why3 library make use of the fact that the same identifier
may be used for only one class of variable: variable symbol,
type symbol, function/predicate symbol, proposition symbol, and
maybe others. This fact is used to build maps that are the reunion of
disjoint maps over those categories. *)
type id_class model { id_class_name : ident_name }
(* Type of set of all classes build yet, and of snapshots
of such classes. Correctness of such specification can be
justified via the use of history invariants (this trick is a mere coding
of it)
Important note about this trick: any mean of countourning the fact
that program values of type id_class are build using this interface
would break its safety. In practice, this impose limitation about
calls to logic function in (ghost) code, (axiomatized default/choice break
this property when applied to non-pure logic type such as id_class).
In this setup, the safe logic functions calls in (ghost) code are:
- any call that instantiate polymorphic variables using
pure logic types only (does not interfere with the program world).
- any call to a logic function defined on top of safe logic functions
(can be lifted to the program world).
- projections & constructors (present in the program world).
*)
type id_class_set model { mutable id_classes : id_class -> bool }
type id_class_snapshot model { id_classes_s : id_class -> bool }
val ghost idcls : id_class_set
val ghost id_class_snapshot () : id_class_snapshot
ensures { result.id_classes_s = idcls.id_classes }
val ghost id_classes_growth (id0:id_class_snapshot) : unit
ensures { subset id0.id_classes_s idcls.id_classes }
val ghost id_class_inv (idc:id_class) : unit
ensures { idcls.id_classes idc }
val ghost fresh_id_class () : id_class
writes { idcls }
ensures { not (old idcls).id_classes result }
ensures { subset (old idcls).id_classes idcls.id_classes }
ensures { idcls.id_classes result }
(* Projection. *)
function idn_string ident_name : string
type ident model {
id_name : ident_name;
id_label : string -> bool;
id_loc : option position;
(* Not present in Why3 (because ghost): classes to which the identifier
belong, ordered. This allow to build hierarchies of disjoint name
generators on top of identifiers, while being able to easily recover the
disjointness property. *)
id_class : list id_class;
}
function id_string (i:ident) : string = i.id_name.idn_string
val id_string (i:ident) : string
ensures { result = i.id_string }
val id_label (i:ident) : Mlab.s
ensures { result.Mlab.domain = i.id_label }
val id_loc (i:ident) : option position
ensures { result = i.id_loc }
type preid = {
pre_name : string;
pre_label : Mlab.s;
pre_loc : option position;
}
(* Similar mechanism for identifier generation. *)
type id_set model { mutable ids : ident_name -> bool }
type id_set_snapshot model { ids_s : ident_name -> bool }
val ghost ids : id_set
val ghost id_set_snapshot () : id_set_snapshot
ensures { result.ids_s = ids.ids }
val ghost id_set_growth (id0:id_set_snapshot) : unit
ensures { subset id0.ids_s ids.ids }
val ghost id_inv (i:ident) : unit
ensures { ids.ids i.id_name }
val id_equal (i1 i2:ident) : bool
ensures { result -> i1 = i2 }
ensures { i1.id_name = i2.id_name -> result }
val id_register (ghost idc:list id_class) (p:preid) : ident
writes { ids }
ensures { result.id_string = p.pre_name }
ensures { result.id_label = p.pre_label.Mlab.domain }
ensures { result.id_loc = p.pre_loc }
ensures { result.id_class = idc }
ensures { not (old ids).ids result.id_name }
ensures { subset (old ids).ids ids.ids }
ensures { ids.ids result.id_name }
clone extmap.FMap as Mid with
type key = ident,
type key_l = ident_name,
function k_m = id_name
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../ident.mlw" expanded="true">
<theory name="String" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Loc" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Label" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Ident" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
</file>
</why3session>
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../logic_impl.mlw" expanded="true">
<theory name="Ident" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Ty" sum="e6b1a0dadb3900c32ea41aeb7e9bfa0c" expanded="true">
<goal name="WP_parameter sig_world_inv" expl="VC for sig_world_inv" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="102"/></proof>
</goal>
<goal name="WP_parameter tyl_inv" expl="VC for tyl_inv">
<proof prover="0"><result status="valid" time="0.19" steps="300"/></proof>
</goal>
</theory>
<theory name="Term" sum="b19687c0bc7def2d6a9d5eca04977811">
<goal name="WP_parameter vl_ty_len_nth" expl="VC for vl_ty_len_nth">
<transf name="split_goal_wp">
<goal name="WP_parameter vl_ty_len_nth.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.06" steps="24"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="128"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="29"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
module Decl
use import logic_syntax.Defs
use import list.List
use import option.Option
use import support.HOList
use import support.PartialMap
(* Abstract infinite type for proposition symbols. *)
type prsymbol
function prsymbol_from_index (n:int) : prsymbol
axiom prsymbol_from_index_injective : forall n m.
prsymbol_from_index n = prsymbol_from_index m -> n = m
meta infinite_type type prsymbol
(* Constructor: logical symbol for the constructor itself, and
optional names for projections. *)
type constructor = (lsymbol,pmap int lsymbol)
(* datatype declaration: type symbol, constructors. *)
type data_decl = (ty_symbol,list constructor)
(* Logical symbol declaration: name and definition. *)
type logic_decl = (lsymbol,term int)
(* (co)inductive declaration: Ind is for least fixpoint, CoInd for
greatest one. *)
type ind_sign = Ind | CoInd
(* Inductive declaration: predicate name, signature, list of named
clauses. *)
type clause = (prsymbol,term closed)
type ind_decl = (lsymbol,list clause)
(* Kind of proposition.
lemma = prove & use, axiom = use, goal = prove, skip = do nothing. *)
type prop_kind =
| Plemma
| Paxiom
| Pgoal
| Pskip
(* Declaration. *)
type decl =
(* Abstract type symbol. *)
| DType ty_symbol
(* Algebraic datatype. *)
| DData (list data_decl)
(* Abstract logic symbol. *)
| DParam lsymbol
(* Mutually recursive logic definition. *)
| DLogic (list logic_decl)
(* (co)inductive predicate definition. *)
| DInd ind_sign (list ind_decl)
(* Proposition. *)
| DProp prop_kind prsymbol (term closed)
(* Names defined by declarations. *)
predicate data_decl_tys (tys:ty_symbol) (d:data_decl) =
let (tys2,_) = d in tys = tys2
predicate decl_tys (d:decl) (tys:ty_symbol) = match d with
| DType tys2 -> tys = tys2
| DData dl -> exist (data_decl_tys tys) dl
| _ -> false
end
predicate constructor_ls (ls0:lsymbol) (c:constructor) =
let (ls,pm) = c in ls = ls0 \/ exists n. pm n = Some ls0
predicate constructor_constr (ls0:lsymbol) (c:constructor) =
let (ls,_) = c in ls = ls0
predicate data_decl_ls (ls0:lsymbol) (d:data_decl) = let (_,cn) = d in
exist (constructor_ls ls0) cn
predicate data_decl_constr (ls0:lsymbol) (d:data_decl) = let (_,cn) = d in
exist (constructor_constr ls0) cn
predicate decl_constr (d:decl) (ls0:lsymbol) = match d with
| DData dl -> exist (data_decl_constr ls0) dl
| _ -> false
end
predicate is_fst (ls0:'a) (p:('a,'b)) =
let (ls1,_) = p in ls0 = ls1
predicate decl_ls (d:decl) (ls0:lsymbol) = match d with
| DParam ls -> ls = ls0
| DData dl -> exist (data_decl_ls ls0) dl
| DLogic ld -> exist (is_fst ls0) ld
| DInd _ idl -> exist (is_fst ls0) idl
| _ -> false
end
predicate ind_decl_prs (prs0:prsymbol) (id:(lsymbol,list clause)) =
let (_,cls) = id in exist (is_fst prs0) cls
predicate decl_prs (d:decl) (prs0:prsymbol) = match d with
| DProp _ prs _ -> prs0 = prs
| DInd _ idl -> exist (ind_decl_prs prs0) idl
| _ -> false
end
predicate logic_decl_no_conflict (ld:list logic_decl) = match ld with
| Nil -> true
| Cons (ls,_) q -> not exist (is_fst ls) q /\ logic_decl_no_conflict q
end
(*
(* No conflict between declared names. *)
predicate decl_no_conflict (d:decl) = match d with
| DData dl ->
| DLogic ld -> logic_decl_no_conflict ld
| DInd _ idl -> ind_decl_no_conflict idl
end*)
(* Domain of declared symbols for terms. *)
type syms_dom = {
d_tys : ty_symbol -> bool;
d_ls : lsymbol -> bool;
d_constr : lsymbol -> bool;
}
end
(*
(* Need a modelisation of tasks.
Base idea: task = Well-founded stack of
environments obtained by successive declaration
extension.
So in the modelisation part, we need:
- Declarations & their semantics.
- Declaration environments & semantics again.
*)
module Decl
use import logic_syntax.Defs
use import logic_syntax.VarsIn
use import support.HO
use import support.PartialMap
use import support.Choice
use import logic_typing.Env
use import option.Option
use import int.Int
use import list.List
use import list.Length
(* Abstract infinite type for proposition symbols. *)
type prsymbol
function prsymbol_from_index (n:int) : prsymbol
axiom prsymbol_from_index_injective : forall n m.
prsymbol_from_index n = prsymbol_from_index m -> n = m
meta infinite_type type prsymbol
(* Constructor: logical symbol for constructor,
and optional names for projections. *)
type constructor = (lsymbol,pmap int lsymbol)
(* Datatype declaration: type symbol, constructors. *)
type data_decl = (ty_symbol,list constructor)
(* Logical declaration: logical symbol name,type arity,signature,
definition. *)
type logic_decl = (lsymbol,term int)
(* Inductive declaration sign: inductive (least fixpoint) or coinductive
(greatest fixpoint). *)
type ind_sign = Ind | Coind
(* Inductive declaration: predicate name, signature, list of
named clauses. *)
type ind_decl = (lsymbol,list (prsymbol,term closed))
type prop_kind =
| Plemma
| Paxiom
| Pgoal
| Pskip
type decl =
| Dtype ty_symbol
| Ddata (list data_decl)
| Dparam lsymbol
| Dlogic (list logic_decl)
| Dind ind_sign (list ind_decl)
| Dprop prop_kind prsymbol (term closed)
predicate data_decl_ty_symbols (dl:list data_decl) (tys:ty_symbol) =
match dl with
| Nil -> false
| Cons (tys2,_) q -> tys = tys2 \/ data_decl_ty_symbols q tys
end
predicate decl_ty_symbols (d:decl) (tys:ty_symbol) = match d with
| Dtype tys2 -> tys = tys2
| Ddata dl -> data_decl_ty_symbols dl tys
| _ -> false
end
predicate constructor_lsymbols (cl:list constructor) (ls:lsymbol) =
match cl with
| Nil -> false
| Cons (cn,pm) q -> ls = cn \/ constructor_lsymbols q ls \/
exists n. pm n = Some ls
end
predicate constructor_names (cl:list constructor) (ls:lsymbol) =
match cl with
| Nil -> false
| Cons (cn,_) q -> ls = cn \/ constructor_names q ls
end
predicate data_decl_lsymbols (dl:list data_decl) (ls:lsymbol) =
match dl with
| Nil -> false
| Cons (_,cl) q -> constructor_lsymbols cl ls \/
data_decl_lsymbols q ls
end
predicate logic_decl_lsymbols (dl:list logic_decl) (ls:lsymbol) =