Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 8b002d87 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

removed example wp.mlw which is obsolete

parent 91ca9bd1
theory Imp
(* terms and formulas *)
type datatype = Tint | Tbool
type operator = Oplus | Ominus | Omult | Ole
type ident = int
type term =
| Tconst int
| Tvar ident
| Tderef ident
| Tbin term operator term
type fmla =
| Fterm term
| Fand fmla fmla
| Fnot fmla
| Fimplies fmla fmla
| Flet ident term fmla
| Fforall ident datatype fmla
(* program states: 2 stack env for refs and local vars *)
use import int.Int
use import bool.Bool
type value =
| Vint int
| Vbool bool
use map.Map as IdMap
type var_env = IdMap.map ident value
type ref_env = IdMap.map ident value
type state = {| var_env : var_env; ref_env: ref_env |}
(* semantics of formulas *)
predicate eval_bin (x:value) (op:operator) (y:value) (res:value) =
match x,y with
| Vint x,Vint y ->
match op with
| Oplus -> res = Vint (x+y)
| Ominus -> res = Vint (x-y)
| Omult -> res = Vint (x*y)
| Ole -> res = Vbool (if x <= y then True else False)
end
| _,_ -> false
end
(*
inductive get_env (i:int) (env:list value) (res:value) =
| Get_first:
forall x:value, l:list value. get_env 0 (Cons x l) x
| Get_next:
forall i:int, x r:value, l:list value. i > 0 ->
get_env (i-1) l r -> get_env i (Cons x l) x
*)
predicate get_refenv (i:ident) (e:ref_env) (r:value) =
IdMap.get e i = r
inductive eval_term state term value =
| eval_const :
forall s:state, n:int. eval_term s (Tconst n) (Vint n)
| eval_var :
forall s:state, i:int, res:value.
get_refenv i (var_env s) res -> eval_term s (Tvar i) res
| eval_deref :
forall s:state, i:ident, res:value.
get_refenv i (ref_env s) res -> eval_term s (Tderef i) res
| eval_bin :
forall s:state, op:operator, t1 t2:term, r1 r2 r:value.
eval_term s t1 r1 -> eval_term s t2 r2 ->
eval_bin r1 op r2 r -> eval_term s (Tbin t1 op t2) r
function my_state :state =
{| var_env = IdMap.const (Vint 42);
ref_env = IdMap.const (Vint 0) |}
goal Test13 :
eval_term my_state (Tconst 13) (Vint 13)
goal Test42 :
eval_term my_state (Tvar 0) (Vint 42)
goal Test55 :
eval_term my_state (Tbin (Tvar 0) Oplus (Tconst 13)) (Vint 55)
inductive eval_fmla state fmla bool =
| eval_term:
forall s:state, t:term, b:bool.
eval_term s t (Vbool b) -> eval_fmla s (Fterm t) b
| eval_and:
forall s:state, f1 f2:fmla, b1 b2:bool.
eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
eval_fmla s (Fand f1 f2) (andb b1 b2)
| eval_not:
forall s:state, f:fmla, b:bool.
eval_fmla s f b -> eval_fmla s (Fnot f) (notb b)
| eval_impl:
forall s:state, f1 f2:fmla, b1 b2:bool.
eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
eval_fmla s (Fimplies f1 f2) (implb b1 b2)
| eval_forall_int_true:
forall s:state, x:ident, f:fmla.
(* problem: qu'est-ce qui garanti que s.var_env a exactement
autant de debruijn que f ? *)
(forall n:int. eval_fmla
{| var_env = IdMap.set s.var_env x (Vint n);
ref_env = s.ref_env |}
f True) ->
eval_fmla s (Fforall x Tint f) True
(* substitution *)
function subst_term (e:term) (x:ident) (t:term) : term =
match e with
| Tconst _ -> e
| Tvar _ -> e
| Tderef y -> if x=y then t else e
| Tbin e1 op e2 -> Tbin (subst_term e1 x t) op (subst_term e2 x t)
end
lemma eval_subst_term:
forall s:state, e:term, x:ident, t:term, r v:value.
eval_term s t r ->
eval_term s (subst_term e x t) v <->
eval_term {| var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x r) |}
e v
function subst (f:fmla) (x:ident) (t:term) : fmla =
match f with
| Fterm e -> Fterm (subst_term e x t)
| Fand f1 f2 -> Fand (subst f1 x t) (subst f2 x t)
| Fnot f -> Fnot (subst f x t)
| Fimplies f1 f2 -> Fimplies (subst f1 x t) (subst f2 x t)
| Flet y t' f -> Flet y t' (subst f x t)
| Fforall y ty f -> Fforall y ty (subst f x t)
end
lemma eval_subst:
forall s:state, f:fmla, x:ident, t:term, r:value, b:bool.
eval_fmla s (subst f x t) b <->
eval_fmla {| var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x r) |}
f b
(* statements *)
type stmt =
| Sskip
| Sassign ident term
| Sseq stmt stmt
| Sif term stmt stmt
| Swhile term fmla stmt
lemma check_skip:
forall s:stmt. s=Sskip \/s<>Sskip
(* small-steps semantics for statements *)
inductive one_step state stmt state stmt =
| one_step_assign:
forall s:state, x:ident, e:term, r:value.
eval_term s e r ->
one_step s (Sassign x e)
{| var_env = s.var_env;
ref_env = (IdMap.set s.ref_env x r) |}
Sskip
| one_step_seq:
forall s s':state, i1 i1' i2:stmt.
one_step s i1 s' i1' ->
one_step s (Sseq i1 i2) s' (Sseq i1' i2)
| one_step_seq_skip:
forall s:state, i:stmt.
one_step s (Sseq Sskip i) s i
| one_step_if_true:
forall s:state, e:term, i1 i2:stmt.
eval_term s e (Vbool True) ->
one_step s (Sif e i1 i2) s i1
| one_step_if_false:
forall s:state, e:term, i1 i2:stmt.
eval_term s e (Vbool False) ->
one_step s (Sif e i1 i2) s i2
| one_step_while_true:
forall s:state, e:term, inv:fmla, i:stmt.
eval_fmla s inv True ->
eval_term s e (Vbool True) ->
one_step s (Swhile e inv i) s (Sseq i (Swhile e inv i))
| one_step_while_false:
forall s:state, e:term, inv:fmla, i:stmt.
eval_fmla s inv True ->
eval_term s e (Vbool False) ->
one_step s (Swhile e inv i) s Sskip
goal Ass42 :
let x = 0 in
forall s':state.
one_step my_state (Sassign x (Tconst 42)) s' Sskip ->
IdMap.get s'.ref_env x = Vint 42
goal If42 :
let x = 0 in
forall s1 s2:state, i:stmt.
one_step my_state
(Sif (Tbin (Tvar x) Ole (Tconst 10))
(Sassign x (Tconst 13))
(Sassign x (Tconst 42)))
s1 i ->
one_step s1 i s2 Sskip ->
IdMap.get s2.ref_env x = Vint 42
(*
lemma progress:
forall s:state, i:stmt.
i <> Sskip ->
exists s':state, i':stmt. one_step s i s' i'
*)
(* many steps of execution *)
inductive many_steps state stmt state stmt int =
| many_steps_refl:
forall s:state, i:stmt. many_steps s i s i 0
| many_steps_trans:
forall s1 s2 s3:state, i1 i2 i3:stmt, n:int.
one_step s1 i1 s2 i2 ->
many_steps s2 i2 s3 i3 n ->
many_steps s1 i1 s3 i3 (n+1)
lemma steps_non_neg:
forall s1 s2:state, i1 i2:stmt, n:int.
many_steps s1 i1 s2 i2 n -> n >= 0
lemma many_steps_seq:
forall s1 s3:state, i1 i2:stmt, n:int.
many_steps s1 (Sseq i1 i2) s3 Sskip n ->
exists s2:state, n1 n2:int.
many_steps s1 i1 s2 Sskip n1 /\
many_steps s2 i2 s3 Sskip n2 /\
n = 1 + n1 + n2
predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p True
(* Hoare triples *)
predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
forall s:state. eval_fmla s p True ->
forall s':state, n:int. many_steps s i s' Sskip n ->
eval_fmla s' q True
(* Hoare logic rules *)
lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
lemma assign_rule:
forall q:fmla, x:ident, e:term.
valid_triple (subst q x e) (Sassign x e) q
lemma seq_rule:
forall p q r:fmla, i1 i2:stmt.
valid_triple p i1 r /\ valid_triple r i2 q ->
valid_triple p (Sseq i1 i2) q
lemma if_rule:
forall e:term, p q:fmla, i1 i2:stmt.
valid_triple (Fand p (Fterm e)) i1 q /\
valid_triple (Fand p (Fnot (Fterm e))) i2 q ->
valid_triple p (Sif e i1 i2) q
lemma while_rule:
forall e:term, inv:fmla, i:stmt.
valid_triple (Fand (Fterm e) inv) i inv ->
valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)
lemma consequence_rule:
forall p p' q q':fmla, i:stmt.
valid_fmla (Fimplies p' p) ->
valid_triple p i q ->
valid_fmla (Fimplies q q') ->
valid_triple p' i q'
end
module WP
use import Imp
let rec wp (i:stmt) (q:fmla) =
{ true }
match i with
| Sskip -> q
| Sseq i1 i2 -> wp i1 (wp i2 q)
| Sassign x e -> subst q x e
| Sif e i1 i2 ->
Fand (Fimplies (Fterm e) (wp i1 q))
(Fimplies (Fnot (Fterm e)) (wp i2 q))
| Swhile e inv i ->
Fand inv
((*Fforall*) (Fand
(Fimplies (Fand (Fterm e) inv) (wp i inv))
(Fimplies (Fand (Fnot (Fterm e)) inv) q)))
end
{ valid_triple result i q }
end
(*
Local Variables:
compile-command: "why3ide -I . wp.mlw"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="hoare_logic/wp/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="Coq"
version="8.3pl3"/>
<prover
id="3"
name="Z3"
version="2.19"/>
<file
name="../wp.mlw"
verified="false"
expanded="false">
<theory
name="Imp"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="3" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="Test13"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="86" loccnumb="7" loccnume="13"
sum="7eb664a7173faab60e55760a324ec3b8"
proved="true"
expanded="true"
shape="aeval_termamy_stateaTconstc13aVintc13">
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test42"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="89" loccnumb="7" loccnume="13"
sum="259532cc10eaee2ee4cdf74a6e141bb3"
proved="true"
expanded="true"
shape="aeval_termamy_stateaTvarc0aVintc42">
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test55"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="92" loccnumb="7" loccnume="13"
sum="3110de410d998182706e71c56a8f7014"
proved="false"
expanded="true"
shape="aeval_termamy_stateaTbinaTvarc0aOplusaTconstc13aVintc55">
<proof
prover="2"
timelimit="5"
edited="wp_Imp_Test55_2.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.48"/>
</proof>
</goal>
<goal
name="eval_subst_term"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="130" loccnumb="6" loccnume="21"
sum="61d3cd42889c7d7f446e6ca75f71c7b8"
proved="false"
expanded="true"
shape="aeval_termamk stateavar_envV0asetaref_envV0V2V4V1V5qaeval_termV0asubst_termV1V2V3V5Iaeval_termV0V3V4F">
</goal>
<goal
name="eval_subst"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="148" loccnumb="6" loccnume="16"
sum="05e0a093da7ca03c4f6225fe8474e90a"
proved="false"
expanded="true"
shape="aeval_fmlaamk stateavar_envV0asetaref_envV0V2V4V1V5qaeval_fmlaV0asubstV1V2V3V5F">
</goal>
<goal
name="check_skip"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="165" loccnumb="6" loccnume="16"
sum="43f9a240024fe10ea2893004f1456d99"
proved="true"
expanded="true"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Ass42"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="211" loccnumb="7" loccnume="12"
sum="68d86d357151b57013508d2e18183677"
proved="true"
expanded="true"
shape="Lc0ainfix =agetaref_envV1V0aVintc42Iaone_stepamy_stateaSassignV0aTconstc42V1aSskipF">
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="If42"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="217" loccnumb="7" loccnume="11"
sum="f0ecadcdee6ca483a0436981d29e894d"
proved="false"
expanded="true"
shape="Lc0ainfix =agetaref_envV2V0aVintc42Iaone_stepV1V3V2aSskipIaone_stepamy_stateaSifaTbinaTvarV0aOleaTconstc10aSassignV0aTconstc13aSassignV0aTconstc42V1V3F">
<proof
prover="2"
timelimit="5"
edited="wp_Imp_If42_1.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.59"/>
</proof>
</goal>
<goal
name="steps_non_neg"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="248" loccnumb="6" loccnume="19"
sum="8f61a11a831b83c2aa1be229d509100d"
proved="false"
expanded="true"
shape="ainfix >=V4c0Iamany_stepsV0V2V1V3V4F">
<proof
prover="3"
timelimit="5"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
name="many_steps_seq"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="252" loccnumb="6" loccnume="20"
sum="9cd22e45f080debb5e11cbbf7df57d9d"
proved="false"
expanded="true"
shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
<proof
prover="3"
timelimit="5"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
name="skip_rule"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="272" loccnumb="6" loccnume="15"
sum="c7419cbdb36af28356c42967e8a7fb88"
proved="false"
expanded="true"
shape="avalid_tripleV0aSskipV0F">
</goal>
<goal
name="assign_rule"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="275" loccnumb="6" loccnume="17"
sum="779a47ca63e2a97d4eb3146bf8a03d9b"
proved="false"
expanded="true"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
</goal>
<goal
name="seq_rule"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="279" loccnumb="6" loccnume="14"
sum="dc15b633249d9c5699355d5a63eff3a9"
proved="false"
expanded="true"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
</goal>
<goal
name="if_rule"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="284" loccnumb="6" loccnume="13"
sum="b2404afad60172fea170c8e580317a5d"
proved="false"
expanded="true"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
</goal>
<goal
name="while_rule"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="290" loccnumb="6" loccnume="16"
sum="443e0b0c56a9cbee49e2de672e8036d0"
proved="false"
expanded="true"
shape="avalid_tripleV1aSwhileV0V1V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
</goal>
<goal
name="consequence_rule"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="295" loccnumb="6" loccnume="22"
sum="7fed3b054b052d408bd5137e2e65a702"
proved="false"
expanded="true"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
</goal>
</theory>
<theory
name="WP WP"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="309" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="WP_parameter wp"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="313" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="9cdc33adec5d94c050215a30e74dd9a5"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSwhileVVVavalid_tripleaFandV14aFandaFimpliesaFandaFtermV13V14V16aFimpliesaFandaFnotaFtermV13V14V1V0V1Iavalid_tripleV16V15V14FFF">
<label
name="expl:parameter wp">
</label>
<transf
name="split_goal"
proved="false"
expanded="true">
<goal
name="WP_parameter wp.1"
locfile="hoare_logic/wp/../wp.mlw"
loclnum="313" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="2ebbde0b45c0a4017df93f6636babf85"
proved="true"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSwhileVVVtFF">
<label
name="expl:parameter wp">
</label>
<proof
prover="3"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="val