Skip to content
Snippets Groups Projects
Select Git revision
  • a065e3200f2658eff630d992fd66ee77bc5fc927
  • master default protected
  • usb
  • fresk
4 results

bare3.rs

Blame
  • blocking_semantics4.mlw 29.41 KiB
    
    (** {1 A certified WP calculus} *)
    
    (** {2 A simple imperative language with expressions, syntax and semantics} *)
    
    theory ImpExpr
    
    use import int.Int
    use import int.MinMax
    use import bool.Bool
    use export list.List
    use export list.Append
    use map.Map as IdMap
    
    (** types and values *)
    
    type datatype = TYunit | TYint | TYbool
    type value = Vvoid | Vint int | Vbool bool
    
    (** terms and formulas *)
    
    type operator = Oplus | Ominus | Omult | Ole
    
    (** ident for mutable variables *)
    type mident
    
    
    axiom mident_decide :
      forall m1 m2: mident. m1 = m2 \/ m1 <> m2
    
    (** ident for immutable variables *)
    type ident = { ident_index : int }
    
    constant result : ident
    
    axiom ident_decide :
      forall m1 m2: ident. m1 = m2 \/ m1 <> m2
    
    (** Terms *)
    type term =
      | Tvalue value
      | Tvar ident
      | Tderef mident
      | Tbin term operator term
    
    
    predicate var_occurs_in_term (x:ident) (t:term) =
      match t with
      | Tvalue _  -> false
      |  Tvar i  -> x=i
      |  Tderef _  -> false
      |  Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
      end
    
    (* predicate mvar_occurs_in_term (x:mident) (t:term) = *)
    (*   match t with *)
    (*   | Tvalue _  -> false *)
    (*   |  Tvar i  -> x = i *)
    (*   |  Tderef _  -> false *)
    (*   |  Tbin t1 _ t2 -> mvar_occurs_in_term x t1 \/ mvar_occurs_in_term x t2 *)
    (*   end *)
    
    (* predicate term_inv (t:term) = *)
    (*   forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar *)
    
    function mk_tvalue (v:value) : term =
       Tvalue v
    
    function mk_tvar (i:ident) : term =
       Tvar i
    
    function mk_tderef (r:mident) : term =
       Tderef r
    
    function mk_tbin (t1:term) (o:operator) (t2:term) : term =
        Tbin t1 o t2
    
    (** Formulas *)
    type fmla =
      | Fterm term
      | Fand fmla fmla
      | Fnot fmla
      | Fimplies fmla fmla
      | Flet ident term fmla         (* let id = term in fmla *)
      | Fforall ident datatype fmla  (* forall id : ty, fmla *)
    
    (** Expressions *)
    type expr =
      | Evalue value
      | Ebin expr operator expr
      | Evar ident
      | Ederef mident
      | Eassign mident expr
      | Eseq expr expr
      | Elet ident expr expr
      | Eif expr expr expr
      | Eassert fmla
      | Ewhile expr fmla expr  (* while cond invariant inv body *)
    
    function mk_evalue (v:value) : expr =
       Evalue v
    
    function mk_evar (i:ident) : expr =
       Evar i
    
    function mk_ederef (r:mident) : expr =
       Ederef r
    
    function mk_ebin (e1:expr) (o:operator) (e2:expr) : expr =
        Ebin e1 o e2
    
    (* lemma decide_is_skip: *)
    (*   forall s:stmt. s = Sskip \/ s <> Sskip *)
    
    (** Typing *)
    
    function type_value (v:value) : datatype =
        match v with
          | Vvoid  -> TYunit
          | Vint int ->  TYint
          | Vbool bool -> TYbool
    end
    
    inductive type_operator (op:operator) (ty1 ty2 ty: datatype) =
          | Type_plus : type_operator Oplus TYint TYint TYint
          | Type_minus : type_operator Ominus TYint TYint TYint
          | Type_mult : type_operator Omult TYint TYint TYint
          | Type_le : type_operator Ole TYint TYint TYbool
    
    type type_stack = list (ident, datatype)  (* map local immutable variables to their type *)
    function get_vartype (i:ident) (pi:type_stack) : datatype =
      match pi with
      | Nil -> TYunit
      | Cons (x,ty) r -> if x=i then ty else get_vartype i r
      end
    
    
    type type_env = IdMap.map mident datatype  (* map global mutable variables to their type *)
    function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i
    
    inductive type_term type_env type_stack term datatype =
      | Type_value :
          forall sigma: type_env, pi:type_stack, v:value.
    	type_term sigma pi  (Tvalue v) (type_value v)
      | Type_var :
          forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
            (get_vartype v pi = ty) ->
            type_term sigma pi (Tvar v) ty
      | Type_deref :
          forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
            (get_reftype v sigma = ty) ->
            type_term sigma pi (Tderef v) ty
      | Type_bin :
          forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator,
            ty1 ty2 ty:datatype.
            type_term sigma pi t1 ty1 ->
    	type_term sigma pi t2 ty2 ->
    	type_operator op ty1 ty2 ty ->
            type_term sigma pi (Tbin t1 op t2) ty
    
    inductive type_fmla type_env type_stack fmla =
      | Type_term :
          forall sigma: type_env, pi:type_stack, t:term.
    	type_term sigma pi t TYbool ->
    	type_fmla sigma pi (Fterm t)
      | Type_conj :
          forall sigma: type_env, pi:type_stack, f1 f2:fmla.
    	type_fmla sigma pi f1 ->
            type_fmla sigma pi f2 ->
            type_fmla sigma pi (Fand f1 f2)
      | Type_neg :
          forall sigma: type_env, pi:type_stack, f:fmla.
    	type_fmla sigma pi f ->
            type_fmla sigma pi (Fnot f)
      | Type_implies :
          forall sigma: type_env, pi:type_stack, f1 f2:fmla.
    	type_fmla sigma pi f1 ->
            type_fmla sigma pi f2 ->
            type_fmla sigma pi (Fimplies f1 f2)
      | Type_let :
          forall sigma: type_env, pi:type_stack, x:ident, t:term, f:fmla, ty:datatype.
    	type_term sigma pi t ty ->
            type_fmla sigma (Cons (x,ty) pi) f ->
            type_fmla sigma pi (Flet x t f)
      | Type_forall1 :
          forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
            type_fmla sigma (Cons (x,TYint) pi) f ->
      	type_fmla sigma pi (Fforall x TYint f)
      | Type_forall2 :
          forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
            type_fmla sigma (Cons (x,TYbool) pi) f ->
      	type_fmla sigma pi (Fforall x TYbool f)
      | Type_forall3:
          forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
            type_fmla sigma (Cons (x,TYunit) pi) f ->
      	type_fmla sigma pi (Fforall x TYunit f)
    
    inductive type_expr type_env type_stack expr datatype =
      | Type_Evalue :
          forall sigma: type_env, pi:type_stack, v:value.
    	type_expr sigma pi (Evalue v) (type_value v)
      | Type_Evar :
          forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
            (get_vartype v pi = ty) -> type_expr sigma pi (Evar v) ty
      | Type_Ederef :
          forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
            (get_reftype v sigma = ty) -> type_expr sigma pi (Ederef v) ty
      | Type_Ebinop :
          forall sigma: type_env, pi:type_stack, e1 e2 : expr, op:operator, ty1 ty2 ty:datatype.
            type_expr sigma pi e1 ty1 ->
            type_expr sigma pi e2 ty2 ->
            type_operator op ty1 ty2 ty -> type_expr sigma pi (Ebin e1 op e2) ty
      | Type_seq :
          forall sigma: type_env, pi:type_stack, e1 e2:expr, ty:datatype.
            type_expr sigma pi e1 TYunit ->
    	type_expr sigma pi e2 ty ->
    	type_expr sigma pi (Eseq e1 e2) ty
      | Type_assigns :
          forall sigma: type_env, pi:type_stack, x:mident, e:expr, ty:datatype.
    	(get_reftype x sigma = ty) ->
            type_expr sigma pi e ty ->
            type_expr sigma pi (Eassign x e) TYunit
      | Type_if :
          forall sigma: type_env, pi:type_stack, t e1 e2:expr, ty:datatype.
    	type_expr sigma pi t TYbool ->
    	type_expr sigma pi e1 ty ->
    	type_expr sigma pi e2 ty ->
        	type_expr sigma pi (Eif t e1 e2) ty
      | Type_assert :
          forall sigma: type_env, pi:type_stack, p:fmla.
    	type_fmla sigma pi p ->
        	type_expr sigma pi (Eassert p) TYbool
      | Type_while :
          forall sigma: type_env, pi:type_stack, guard:expr, body:expr, inv:fmla, ty:datatype.
    	type_fmla sigma pi inv ->
            type_expr sigma pi guard TYbool ->
            type_expr sigma pi body ty ->
            type_expr sigma pi (Ewhile guard inv body) ty
      | Type_Elet :
          forall sigma: type_env, pi:type_stack, x:ident, e1 e2:expr, ty1 ty2 :datatype.
    	type_expr sigma pi e1 ty1 ->
            type_expr sigma (Cons (x,ty1) pi) e2 ty2 ->
    	type_expr sigma pi (Elet x e1 e2) ty2
    
    (** Operational semantic *)
    type env = IdMap.map mident value  (* map global mutable variables to their value *)
    function get_env (i:mident) (e:env) : value = IdMap.get e i
    
    type stack = list (ident, value)  (* map local immutable variables to their value *)
    function get_stack (i:ident) (pi:stack) : value =
      match pi with
      | Nil -> Vvoid
      | Cons (x,v) r -> if x=i then v else get_stack i r
      end
    
    lemma get_stack_eq:
      forall x:ident, v:value, r:stack.
        get_stack x (Cons (x,v) r) = v
    
    lemma get_stack_neq:
      forall x i:ident, v:value, r:stack.
        x <> i -> get_stack i (Cons (x,v) r) = get_stack i r
    
    (** semantics of formulas *)
    
    function eval_bin (x:value) (op:operator) (y:value) : value =
      match x,y with
      | Vint x,Vint y ->
         match op with
         | Oplus -> Vint (x+y)
         | Ominus -> Vint (x-y)
         | Omult -> Vint (x*y)
         | Ole -> Vbool (if x <= y then True else False)
         end
      | _,_ -> Vvoid
      end
    
    function eval_term (sigma:env) (pi:stack) (t:term) : value =
      match t with
      | Tvalue v -> v
      |  Tvar id  -> get_stack id pi
      |  Tderef id  -> get_env id sigma
      |  Tbin t1 op t2  ->
         eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
    end
    
    
    lemma eval_bool_term:
      forall sigma:env, pi:stack, sigmat:type_env, pit:type_stack, t:term.
        type_term sigmat pit t TYbool ->
        (* TODO: compatibility sigma, sigmat and pi,pit *)
        exists b:bool.
          eval_term sigma pi t = Vbool b
    
    predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
      match f with
      | Fterm t -> eval_term sigma pi t = Vbool True
      | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
      | Fnot f -> not (eval_fmla sigma pi f)
      | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
      | Flet x t f ->
          eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
      | Fforall x TYint f ->
         forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f
      | Fforall x TYbool f ->
         forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f
      | Fforall x TYunit f ->  eval_fmla sigma (Cons (x,Vvoid) pi) f
      end
    
    
    (* function eval_expr (sigma:env) (pi:stack) (e:expr) : value = *)
    (*   match e with *)
    (*   | Evalue v -> v *)
    (*   | Evar id  -> get_stack id pi *)
    (*   | Ederef id  -> get_env id sigma *)
    (*   | Ebin e1 op e2  -> *)
    (*      eval_bin (eval_expr sigma pi e1) op (eval_expr sigma pi e2) *)
    (*   | Eassign id e1  *)
    (*   | Eseq e1 e2  *)
    (*   | Elet id e1 e2 -> void *)
    (*   | Eif e1 e2 e3 ->  *)
    (*     if ((eval_expr sigma pi e1) = (Vbool True))  *)
    (*     then eval_expr sigma pi e2 *)
    (*     else eval_expr sigma pi e3 *)
    (*   | Eassert f -> eval_fmla f *)
    (*   | Ewhile expr fmla expr  ->  *)
    (* end *)
    
    (** substitution of a reference [r] by a logic variable [v]
       warning: proper behavior only guaranted if [v] is "fresh",
       i.e index(v) > term_maxvar(t) *)
    
    function msubst_term (t:term) (r:mident) (v:ident) : term =
      match t with
      | Tvalue _ | Tvar _  -> t
      | Tderef x -> if r = x then mk_tvar v else t
      | Tbin t1 op t2  ->
          mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v)
      end
    
    function subst_term (t:term) (r:ident) (v:ident) : term =
      match t with
      | Tvalue _ | Tderef _  -> t
      | Tvar x  ->
          if r = x then mk_tvar v else t
      | Tbin t1 op t2  ->
         mk_tbin (subst_term t1 r v) op (subst_term t2 r v)
      end
    
    
    (** [fresh_in_term id t] is true when [id] does not occur in [t] *)
    predicate fresh_in_term (id:ident) (t:term) =
        not (var_occurs_in_term id t)
    
    (* predicate mfresh_in_term (id:mident) (t:term) = *)
    (*     not (mvar_occurs_in_term id t) *)
    
    lemma fresh_in_binop:
      forall t t':term, op:operator, v:ident.
        fresh_in_term v (mk_tbin t op t') ->
          fresh_in_term v t  /\ fresh_in_term v t'
    
    (* lemma eval_subst_term: *)
    (*   forall sigma:env, pi:stack, e:term, x:ident, v:ident. *)
    (*     fresh_in_term v e -> *)
    (*     eval_term sigma pi (subst_term e x v) = *)
    (*     eval_term sigma (Cons (x, (get_stack v pi)) pi) e *)
    
    predicate fresh_in_fmla (id:ident) (f:fmla) =
      match f with
      | Fterm e -> fresh_in_term id e
      | Fand f1 f2   | Fimplies f1 f2 ->
          fresh_in_fmla id f1 /\ fresh_in_fmla id f2
      | Fnot f -> fresh_in_fmla id f
      | Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
      | Fforall y ty f -> id <> y /\ fresh_in_fmla id f
      end
    
    (* predicate mfresh_in_fmla (id:mident) (f:fmla) = *)
    (*   match f with *)
    (*   | Fterm e -> mfresh_in_term id e *)
    (*   | Fand f1 f2   | Fimplies f1 f2 -> *)
    (*       mfresh_in_fmla id f1 /\ mfresh_in_fmla id f2 *)
    (*   | Fnot f -> mfresh_in_fmla id f *)
    (*   | Flet y t f -> id <> y /\ mfresh_in_term id t /\ mfresh_in_fmla id f *)
    (*   | Fforall y ty f -> id <> y /\ mfresh_in_fmla id f *)
    (* end *)
    
    function subst (f:fmla) (x:ident) (v:ident) : fmla =
      match f with
      | Fterm e -> Fterm (subst_term e x v)
      | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v)
      | Fnot f -> Fnot (subst f x v)
      | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v)
      | Flet y t f -> Flet y (subst_term t x v) (subst f x v)
      | Fforall y ty f -> Fforall y ty (subst f x v)
      end
    
    function msubst (f:fmla) (x:mident) (v:ident) : fmla =
      match f with
      | Fterm e -> Fterm (msubst_term e x v)
      | Fand f1 f2 -> Fand (msubst f1 x v) (msubst f2 x v)
      | Fnot f -> Fnot (msubst f x v)
      | Fimplies f1 f2 -> Fimplies (msubst f1 x v) (msubst f2 x v)
      | Flet y t f -> Flet y (msubst_term t x v) (msubst f x v)
      | Fforall y ty f -> Fforall y ty (msubst f x v)
      end
    
    lemma subst_fresh_term :
      forall t:term, x:ident, v:ident.
       fresh_in_term x t -> subst_term t x v = t
    
    (*Needed ???*)
    lemma subst_fresh :
      forall f:fmla, x:ident, v:ident.
       fresh_in_fmla x f -> subst f x v = f
    
    
    (* Not needed *)
    (* lemma let_subst: *)
    (*     forall t:term, f:fmla, x id':ident, id :mident. *)
    (*     msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *)
    
    lemma eval_msubst_term:
      forall e:term, sigma:env, pi:stack, x:mident, v:ident.
        fresh_in_term v e ->
        eval_term sigma pi (msubst_term e x v) =
        eval_term (IdMap.set sigma x (get_stack v pi)) pi e
    
    (* Need it for monotonicity and wp_reduction *)
    lemma eval_msubst:
      forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
        fresh_in_fmla v f ->
        (eval_fmla sigma pi (msubst f x v) <->
         eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
    
    (* lemma eval_subst: *)
    (*   forall f:fmla, sigma:env, pi:stack, x:ident, v:ident. *)
    (*     fresh_in_fmla v f -> *)
    (*     (eval_fmla sigma pi (subst f x v) <-> *)
    (*      eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)
    
    lemma eval_swap_term:
    forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
    eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
    
    lemma eval_swap_term_2:
      forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
        id1 <> id2 ->
        (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t =
        eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t)
    
    lemma eval_swap:
      forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
        id1 <> id2 ->
        (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
        eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
    
    lemma eval_swap_2:
      forall f:fmla, id1 id2:ident, v1 v2:value.
        id1 <> id2 ->
          forall sigma:env, pi:stack.
        (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
        eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)
    
    lemma eval_term_change_free :
      forall t:term, sigma:env, pi:stack, id:ident, v:value.
        fresh_in_term id t ->
        eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
    
     (* Need it for monotonicity*)
    lemma eval_change_free :
      forall f:fmla, id:ident, v:value.
        fresh_in_fmla id f ->
          forall sigma:env, pi:stack.
        (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
    
    (** [valid_fmla f] is true when [f] is valid in any environment *)
      predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p
    
    (* Not needed *)
    (* axiom msubst_implies : *)
    (* forall p q:fmla. *)
    (*   valid_fmla (Fimplies p q) -> *)
    (*   forall sigma:env, pi:stack, x:mident, id:ident. *)
    (*     fresh_in_fmla id (Fand p q) ->  *)
    (*     eval_fmla sigma (Cons (id, (get_env x sigma)) pi) (Fimplies (msubst p x id) (msubst q x id))  *)
    
    (** let id' = t in f[id <- id'] <=> let id = t in f*)
    (* Not needed *)
    (* lemma let_equiv : *)
    (*   forall id:ident, id':ident, t:term, f:fmla. *)
    (*     forall sigma:env, pi:stack. *)
    (*       fresh_in_fmla id' f -> *)
    (* 	eval_fmla sigma pi (Flet id' t (subst f id id')) *)
    (* 	 -> eval_fmla sigma pi (Flet id t f) *)
    
    (* lemma let_implies : *)
    (*   forall id:ident, t:term, p q:fmla. *)
    (*     valid_fmla (Fimplies p q) -> *)
    (*     valid_fmla (Fimplies (Flet id t p) (Flet id t q)) *)
    
    predicate fresh_in_expr (id:ident) (e:expr) =
      match e with
      | Evalue _ -> true
      | Ebin e1 op e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
      | Evar v -> id <> v
      | Ederef _ -> true
      | Eassign x e -> fresh_in_expr id e
      | Eseq e1 e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
      | Elet v e1 e2 -> id <> v /\ fresh_in_expr id e1 /\ fresh_in_expr id e2
      | Eif e1 e2 e3 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 /\ fresh_in_expr id e3
      | Eassert f -> fresh_in_fmla id f
      | Ewhile cond inv body -> fresh_in_expr id cond /\ fresh_in_fmla id inv /\ fresh_in_expr id body
      end
    
    constant void : expr = Evalue Vvoid
    
    (** small-steps semantics for expressions *)
    
    inductive one_step env stack expr env stack expr =
    
      | one_step_var:
          forall sigma:env, pi:stack, v:ident.
            one_step sigma pi (Evar v) sigma pi (Evalue (get_stack v pi))
    
      | one_step_deref:
          forall sigma:env, pi:stack, v:mident.
            one_step sigma pi (Ederef v) sigma pi (Evalue (get_env v sigma))
    
      | one_step_bin_ctxt1:
          forall sigma sigma':env, pi pi':stack, op:operator,
            e1 e1' e2:expr.
            one_step sigma pi e1 sigma' pi' e1' ->
              one_step sigma pi (Ebin e1 op e2) sigma' pi' (Ebin e1' op e2)
    
      | one_step_bin_ctxt2:
          forall sigma sigma':env, pi pi':stack, op:operator, v1:value, e2 e2':expr.
            one_step sigma pi e2 sigma' pi' e2' ->
              one_step sigma pi (Ebin (Evalue v1) op e2) sigma' pi' (Ebin (Evalue v1) op e2')
    
      | one_step_bin_value:
          forall sigma :env, pi :stack, op:operator, v1 v2:value.
            one_step sigma pi (Ebin (Evalue v1) op (Evalue v2)) sigma pi (Evalue (eval_bin v1 op v2))
    
     | one_step_assign_ctxt:
         forall sigma sigma':env, pi pi':stack, x:mident, e e':expr.
           one_step sigma pi e sigma' pi' e' ->
           one_step sigma pi (Eassign x e) sigma' pi' (Eassign x e')
    
      | one_step_assign_value:
          forall sigma sigma':env, pi:stack, x:mident, v:value.
            sigma' = IdMap.set sigma x v ->
        one_step sigma pi (Eassign x (Evalue v)) sigma' pi void
    
      | one_step_seq_ctxt:
          forall sigma sigma':env, pi pi':stack, e1 e1' e2:expr.
            one_step sigma pi e1 sigma' pi' e1' ->
              one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1' e2)
    
      | one_step_seq_value:
          forall sigma:env, pi:stack, e:expr.
            one_step sigma pi (Eseq void e) sigma pi e
    
      | one_step_let_ctxt:
          forall sigma sigma':env, pi pi':stack, id:ident, e1 e1' e2:expr.
            one_step sigma pi e1 sigma' pi' e1' ->
              one_step sigma pi (Elet id e1 e2) sigma' pi' (Elet id e1' e2)
    
      | one_step_let_value:
          forall sigma:env, pi:stack, id:ident, v:value, e:expr.
            one_step sigma pi (Elet id (Evalue v) e) sigma (Cons (id,v) pi) e
    
      | one_step_if_ctxt:
          forall sigma sigma':env, pi pi':stack, e1 e1' e2 e3:expr.
            one_step sigma pi e1 sigma' pi' e1' ->
              one_step sigma pi (Eif e1 e2 e3) sigma' pi' (Eif e1' e2 e3)
    
      | one_step_if_true:
          forall sigma:env, pi:stack, e1 e2:expr.
            one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1
    
      | one_step_if_false:
          forall sigma:env, pi:stack, e1 e2 :expr.
            one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2
    
      | one_step_assert:
          forall sigma:env, pi:stack, f:fmla.
            (* blocking semantics *)
            eval_fmla sigma pi f ->
              one_step sigma pi (Eassert f) sigma pi void
    
      | one_step_while_true:
          forall sigma:env, pi:stack, cond body:expr, inv:fmla.
            (* blocking semantics *)
            eval_fmla sigma pi inv ->
            one_step sigma pi (Ewhile (Evalue (Vbool True)) inv body) sigma pi
            (Eseq body (Ewhile cond inv body))
    
      | one_step_while_false:
          forall sigma:env, pi:stack, inv:fmla, body:expr.
            (* blocking semantics *)
            eval_fmla sigma pi inv ->
            one_step sigma pi (Ewhile (Evalue (Vbool False)) inv body) sigma pi void
    
     (** many steps of execution *)
    
     inductive many_steps env stack expr env stack expr int =
       | many_steps_refl:
         forall sigma:env, pi:stack, s:expr. many_steps sigma pi s sigma pi s 0
       | many_steps_trans:
         forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:expr, n:int.
           n > 0 -> one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
           many_steps sigma2 pi2 s2 sigma3 pi3 s3 (n - 1) ->
           many_steps sigma1 pi1 s1 sigma3 pi3 s3 n
    
    lemma steps_non_neg:
      forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:expr, n:int.
        many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0
    
    (* Used by Hoare_logic/seq_rule*)
      lemma many_steps_seq:
        forall sigma1 sigma3:env, pi1 pi3:stack, e1 e2:expr, n:int.
          many_steps sigma1 pi1 (Eseq e1 e2) sigma3 pi3 void n ->
          exists sigma2:env, pi2:stack, n1 n2:int.
            many_steps sigma1 pi1 e1 sigma2 pi2 void n1 /\
            many_steps sigma2 pi2 e2 sigma3 pi3 void n2 /\
            n = 1 + n1 + n2
    
     (* lemma one_step_change_free : *)
     (*  forall s s':stmt, sigma sigma':env, pi pi':stack, id:ident, v:value. *)
     (*    fresh_in_stmt id s -> *)
     (*    one_step sigma (Cons (id,v) pi) s sigma' pi' s' -> *)
     (*    one_step sigma pi s sigma' pi' s' *)
    
    
    (** {3 Hoare triples} *)
    
    (** partial correctness *)
    predicate valid_triple (p:fmla) (e:expr) (q:fmla) =
        forall sigma:env, pi:stack. eval_fmla sigma pi p ->
          forall sigma':env, pi':stack, n:int.
            many_steps sigma pi e sigma' pi' void n ->
              eval_fmla sigma' pi' q
    
    (*** total correctness *)
    predicate total_valid_triple (p:fmla) (e:expr) (q:fmla) =
        forall sigma:env, pi:stack. eval_fmla sigma pi p ->
          exists sigma':env, pi':stack, n:int.
            many_steps sigma pi e sigma' pi' void n /\
            eval_fmla sigma' pi' q
    
    end
    
    
    theory TestSemantics
    
    use import ImpExpr
    
    function my_sigma : env = IdMap.const (Vint 0)
    constant x : ident
    constant y : mident
    
    function my_pi : stack = Cons (x, Vint 42) Nil
    
    goal Test13 :
      eval_term my_sigma my_pi (mk_tvalue (Vint 13)) = Vint 13
    
    goal Test13expr :
      many_steps my_sigma my_pi (Evalue (Vint 13)) my_sigma my_pi (Evalue (Vint 13)) 0
    
    goal Test42 :
      eval_term my_sigma my_pi (Tvar x) = Vint 42
    
    goal Test42expr :
      one_step my_sigma my_pi (Evar x) my_sigma my_pi (Evalue (Vint 42))
    
    goal Test0 :
      eval_term my_sigma my_pi (Tderef y) = Vint 0
    
    goal Test0expr :
      one_step my_sigma my_pi (Ederef y) my_sigma my_pi (Evalue (Vint 0))
    
    goal Test55 :
      eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55
    
    goal Test55expr :
      many_steps my_sigma my_pi (Ebin (Evar x) Oplus (Evalue (Vint 13))) my_sigma my_pi (Evalue (Vint 55)) 2
    
    goal Ass42 :
      forall sigma':env, pi':stack.
        one_step my_sigma my_pi (Eassign y (Evalue (Vint 42))) sigma' pi' void ->
          IdMap.get sigma' y = Vint 42
    
    goal If42 :
        forall sigma1 sigma2:env, pi1 pi2:stack, e:expr.
          one_step my_sigma my_pi
            (Eif (Ebin (Ederef y) Ole (Evalue (Vint 10)))
                 (Eassign y (Evalue (Vint 13)))
                 (Eassign y (Evalue (Vint 42))))
            sigma1 pi1 e ->
          one_step sigma1 pi1 e sigma2 pi2 void ->
            IdMap.get sigma2 y = Vint 13
    
    end
    
    (** {2 Hoare logic} *)
    
    theory HoareLogic
    
    use import ImpExpr
    
    
    (** Hoare logic rules (partial correctness) *)
    
    lemma consequence_rule:
      forall p p' q q':fmla, s:expr.
      valid_fmla (Fimplies p' p) ->
      valid_triple p s q ->
      valid_fmla (Fimplies q q') ->
      valid_triple p' s q'
    
    lemma skip_rule:
      forall q:fmla. valid_triple q void q
    
    (* lemma assign_rule: *)
    (*   forall p:fmla, x:mident, id:ident, t:term. *)
    (*   fresh_in_fmla id p -> *)
    (*   valid_triple (Flet id t (msubst p x id)) (Eassign x t) p *)
    
    lemma seq_rule:
      forall p q r:fmla, e1 e2:expr.
      valid_triple p e1 r /\ valid_triple r e2 q ->
      valid_triple p (Eseq e1 e2) q
    
    (* lemma if_rule: *)
    (*   forall t:term, p q:fmla, e1 e2:expr. *)
    (*   valid_triple (Fand p (Fterm t)) e1 q /\ *)
    (*   valid_triple (Fand p (Fnot (Fterm t))) e2 q -> *)
    (*   valid_triple p (Eif t e1 e2) q *)
    
    lemma assert_rule:
      forall f p:fmla. valid_fmla (Fimplies p f) ->
      valid_triple p (Eassert f) p
    
    lemma assert_rule_ext:
      forall f p:fmla.
      valid_triple (Fimplies f p) (Eassert f) p
    
    (*
    lemma while_rule:
      forall e:term, inv:fmla, i:expr.
      valid_triple (Fand (Fterm e) inv) i inv ->
      valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)
    
    lemma while_rule_ext:
      forall e:term, inv inv':fmla, i:expr.
      valid_fmla (Fimplies inv' inv) ->
      valid_triple (Fand (Fterm e) inv') i inv' ->
      valid_triple inv' (Swhile e inv i) (Fand (Fnot (Fterm e)) inv')
    *)
    
    end
    
    (** {2 WP calculus} *)
    
    theory WP
    
    use import ImpExpr
    use import bool.Bool
    
    use set.Set
    
    (** [assigns sigma W sigma'] is true when the only differences between
        [sigma] and [sigma'] are the value of references in [W] *)
    
    predicate assigns (sigma:env) (a:Set.set mident) (sigma':env) =
      forall i:mident. not (Set.mem i a) ->
        IdMap.get sigma i = IdMap.get sigma' i
    
    lemma assigns_refl:
      forall sigma:env, a:Set.set mident. assigns sigma a sigma
    
    lemma assigns_trans:
      forall sigma1 sigma2 sigma3:env, a:Set.set mident.
        assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
        assigns sigma1 a sigma3
    
    lemma assigns_union_left:
      forall sigma sigma':env, s1 s2:Set.set mident.
        assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'
    
    lemma assigns_union_right:
      forall sigma sigma':env, s1 s2:Set.set mident.
        assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
    
    (** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
    predicate expr_writes (s:expr) (w:Set.set mident) =
      match s with
      | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
      | Eassign id _ -> Set.mem id w
      | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
      | Eif e1 e2 e3 -> expr_writes e1 w /\ expr_writes e2 w /\ expr_writes e3 w
      | Ewhile cond  _ body -> expr_writes cond w /\ expr_writes body w
      | Ebin e1 o e2 -> expr_writes e1 w /\ expr_writes e2 w
      | Elet id e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
      end
    
      function fresh_from (f:fmla) (s:expr) : ident
    
    
      (* Need it for monotonicity*)
      axiom fresh_from_fmla: forall s:expr, f:fmla.
         fresh_in_fmla (fresh_from f s) f
    
      axiom fresh_from_expr: forall s:expr, f:fmla.
         fresh_in_expr (fresh_from f s) s
    
      function abstract_effects (s:expr) (f:fmla) : fmla
    
      axiom abstract_effects_generalize :
         forall sigma:env, pi:stack, s:expr, f:fmla.
            eval_fmla sigma pi (abstract_effects s f) ->
            eval_fmla sigma pi f
    
      axiom abstract_effects_monotonic :
         forall s:expr, f:fmla.
            forall sigma:env, pi:stack. eval_fmla sigma pi f ->
            forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s f)
    
      function wp (e:expr) (q:fmla) : fmla =
        match e with
        | Evalue v -> Flet result (Tvalue v) q
        | Evar v -> Flet result (Tvar v) q
        | Ederef v -> Flet result (Tderef v) q
        | Eassert f ->
            (* asymmetric and *)
            Fand f (Fimplies f q)
        | Eseq e1 e2 -> wp e1 (wp e2 q)
        | Elet id e1 e2 -> wp e1 (Flet id (Tvar result) (wp e2 q))
        | Ebin e1 op e2 ->
           let t1 = fresh_from q e in
           let t2 = fresh_from (Fand (Fterm (Tvar t1)) q) e in
           let q' = Flet result (Tbin (Tvar t1) op (Tvar t2)) q in
           let f = wp e2 (Flet t2 (Tvar result) q') in
           wp e1 (Flet t1 (Tvar result) f)
           (* let wp_op = subst q (Tvar result) (Tbin (Tvar t1) op (Tvar t2)) in *)
           (* let wp2 = (subst (wp e2 wp_op) t2 (Tvar result)) in *)
           (* (subst (wp e1 wp2) t1 (Tvar result)) *)
        | Eassign x e ->
            let id = fresh_from q e in
            let q' = Flet result (Tvalue Vvoid) q in
            wp e (Flet id (Tvar result) (msubst q' x id))
        | Eif e1 e2 e3 ->
            let f =
              Fand (Fimplies (Fterm (Tvar result)) (wp e2 q))
                (Fimplies (Fnot (Fterm (Tvar result))) (wp e3 q))
            in
            wp e1 f
        | Ewhile cond inv body ->
            Fand inv
              (abstract_effects body
                (wp cond
                 (Fand
                  (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv))
                  (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q))))
    
        end
    
      axiom abstract_effects_writes :
         forall sigma:env, pi:stack, s:expr, q:fmla.
            eval_fmla sigma pi (abstract_effects s q) ->
            eval_fmla sigma pi (wp s (abstract_effects s q))
    
    
      (* lemma wp_subst: *)
      (*   forall e:expr, q:fmla, id :mident, id':ident. *)
      (*   fresh_in_stmt id e -> *)
      (*     subst (wp e q) id id' = wp e (subst q id id') *)
    
      lemma monotonicity:
        forall s:expr, p q:fmla.
          valid_fmla (Fimplies p q)
         ->	valid_fmla (Fimplies (wp s p) (wp s q) )
    
      lemma distrib_conj:
        forall s:expr, sigma:env, pi:stack, p q:fmla.
         (eval_fmla sigma pi (wp s p)) /\
         (eval_fmla sigma pi (wp s q)) ->
         eval_fmla sigma pi (wp s (Fand p q))
    
      lemma wp_reduction:
        forall sigma sigma':env, pi pi':stack, s s':expr.
        one_step sigma pi s sigma' pi' s' ->
        forall q:fmla.
          eval_fmla sigma pi (wp s q) ->
          eval_fmla sigma' pi' (wp s' q)
    
      predicate is_value (e:expr) =
        match e with
        | Evalue _ -> true
        | _ -> false
        end
    
      lemma decide_value :
        forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v
    
      lemma bool_value:
        forall v:value, sigmat: type_env, pit:type_stack.
          type_expr sigmat pit (Evalue v) TYbool ->
              (v = Vbool False) \/ (v = Vbool True)
    
      lemma unit_value:
        forall v:value, sigmat: type_env, pit:type_stack.
          type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid
    
      lemma progress:
        forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla.
          type_expr sigmat pit e ty ->
          type_fmla sigmat (Cons(result, ty) pit) q ->
          not is_value e ->
          eval_fmla sigma pi (wp e q) ->
          exists sigma':env, pi':stack, e':expr.
          one_step sigma pi e sigma' pi' e'
    
    end
    
    
    (***
    Local Variables:
    compile-command: "why3ide blocking_semantics4.mlw"
    End:
    *)