(** {1 A certified WP calculus} *)

(** {2 A simple imperative language, syntax and semantics} *)

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

use import int.Int
use import bool.Bool

type value =
  | Vint int
  | Vbool bool

use map.Map as IdMap
type env = IdMap.map ident value

(** 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
  | _,_ -> Vbool False
  end

function get_env (i:ident) (e:env) : value = IdMap.get e i

function eval_term (sigma:env) (pi:env) (t:term) : value =
  match t with
  | Tconst n -> Vint n
  | Tvar id -> get_env 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

predicate eval_fmla (sigma:env) (pi:env) (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 (IdMap.set pi x (eval_term sigma pi t)) f
  | Fforall x Tint f ->
     forall n:int. eval_fmla sigma (IdMap.set pi x (Vint n)) f
  | Fforall x Tbool f ->
     forall b:bool.
        eval_fmla sigma (IdMap.set pi x (Vbool b)) f
  end

(** substitution of a reference `r` by a logic variable `v`
   warning: proper behavior only guaranted if `v` is fresh *)

let rec function subst_term (e:term) (r:ident) (v:ident) : term =
  match e with
  | Tconst _ -> e
  | Tvar _ -> e
  | Tderef x -> if r=x then Tvar v else e
  | Tbin e1 op e2 -> Tbin (subst_term e1 r v) op (subst_term e2 r v)
  end

predicate fresh_in_term (id:ident) (t:term) =
  match t with
  | Tconst _ -> true
  | Tvar v -> id <> v
  | Tderef _ -> true
  | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2
  end

lemma eval_subst_term:
  forall sigma pi:env, e:term, x:ident, v:ident.
    fresh_in_term v e ->
    eval_term sigma pi (subst_term e x v) =
    eval_term (IdMap.set sigma x (IdMap.get pi v)) pi e

lemma eval_term_change_free :
  forall t:term, sigma pi:env, id:ident, v:value.
    fresh_in_term id t ->
    eval_term sigma (IdMap.set pi id v) t = eval_term sigma pi t

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 _ f -> id <> y /\ fresh_in_fmla id f
  end

let rec 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


lemma eval_subst:
  forall f:fmla, sigma pi:env, x:ident, v:ident.
    fresh_in_fmla v f ->
    (eval_fmla sigma pi (subst f x v) <->
     eval_fmla (IdMap.set sigma x (IdMap.get pi v)) pi f)

lemma eval_swap:
  forall f:fmla, sigma pi:env, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_fmla sigma (IdMap.set (IdMap.set pi id1 v1) id2 v2) f <->
    eval_fmla sigma (IdMap.set (IdMap.set pi id2 v2) id1 v1) f)

lemma eval_change_free :
  forall f:fmla, sigma pi:env, id:ident, v:value.
    fresh_in_fmla id f ->
    (eval_fmla sigma (IdMap.set pi id v) f <-> eval_fmla sigma pi f)

(* statements *)

type stmt =
  | Sskip
  | Sassign ident term
  | Sseq stmt stmt
  | Sif term stmt stmt
  | Sassert fmla
  | Swhile term fmla stmt

lemma check_skip:
  forall s:stmt. s=Sskip \/s<>Sskip

(** small-steps semantics for statements *)

inductive one_step env env stmt env env stmt =

  | one_step_assign:
      forall sigma pi:env, x:ident, e:term.
        one_step sigma pi (Sassign x e)
                 (IdMap.set sigma x (eval_term sigma pi e)) pi
                 Sskip

  | one_step_seq:
      forall sigma pi sigma' pi':env, i1 i1' i2:stmt.
        one_step sigma pi i1 sigma' pi' i1' ->
          one_step sigma pi (Sseq i1 i2) sigma' pi' (Sseq i1' i2)

  | one_step_seq_skip:
      forall sigma pi:env, i:stmt.
        one_step sigma pi (Sseq Sskip i) sigma pi i

  | one_step_if_true:
      forall sigma pi:env, e:term, i1 i2:stmt.
        eval_term sigma pi e = (Vbool True) ->
          one_step sigma pi (Sif e i1 i2) sigma pi i1

  | one_step_if_false:
      forall sigma pi:env, e:term, i1 i2:stmt.
        eval_term sigma pi e = (Vbool False) ->
          one_step sigma pi (Sif e i1 i2) sigma pi i2

  | one_step_assert:
      forall sigma pi:env, f:fmla.
        eval_fmla sigma pi f ->
          one_step sigma pi (Sassert f) sigma pi Sskip

  | one_step_while_true:
      forall sigma pi:env, e:term, inv:fmla, i:stmt.
        eval_fmla sigma pi inv ->
        eval_term sigma pi e = (Vbool True) ->
          one_step sigma pi (Swhile e inv i) sigma pi (Sseq i (Swhile e inv i))

  | one_step_while_false:
      forall sigma pi:env, e:term, inv:fmla, i:stmt.
        eval_fmla sigma pi inv ->
        eval_term sigma pi e = (Vbool False) ->
          one_step sigma pi (Swhile e inv i) sigma pi Sskip

(***

  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 env env stmt env env stmt int =
   | many_steps_refl:
     forall sigma pi:env, i:stmt. many_steps sigma pi i sigma pi i 0
   | many_steps_trans:
     forall sigma1 pi1 sigma2 pi2 sigma3 pi3:env, i1 i2 i3:stmt, n:int.
       one_step sigma1 pi1 i1 sigma2 pi2 i2 ->
       many_steps sigma2 pi2 i2 sigma3 pi3 i3 n ->
       many_steps sigma1 pi1 i1 sigma3 pi3 i3 (n+1)

lemma steps_non_neg:
  forall sigma1 pi1 sigma2 pi2:env, i1 i2:stmt, n:int.
    many_steps sigma1 pi1 i1 sigma2 pi2 i2 n -> n >= 0

lemma many_steps_seq:
  forall sigma1 pi1 sigma3 pi3:env, i1 i2:stmt, n:int.
    many_steps sigma1 pi1 (Sseq i1 i2) sigma3 pi3 Sskip n ->
    exists sigma2 pi2:env, n1 n2:int.
      many_steps sigma1 pi1 i1 sigma2 pi2 Sskip n1 /\
      many_steps sigma2 pi2 i2 sigma3 pi3 Sskip n2 /\
      n = 1 + n1 + n2



predicate valid_fmla (p:fmla) = forall sigma pi:env. eval_fmla sigma pi p

(** {3 Hoare triples} *)

(** partial correctness *)
predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
    forall sigma pi:env. eval_fmla sigma pi p ->
      forall sigma' pi':env, n:int. many_steps sigma pi i sigma' pi' Sskip n ->
        eval_fmla sigma' pi' q

(*** total correctness *)
(***
predicate total_valid_triple (p:fmla) (i:stmt) (q:fmla) =
    forall s:state. eval_fmla s p ->
      exists s':state, n:int. many_steps s i s' Sskip n /\
        eval_fmla s' q
*)

end


theory TestSemantics

use import Imp
use import map.Const

function my_sigma : env = Const.const (Vint 0)
function my_pi : env = Const.const (Vint 42)

goal Test13 :
  eval_term my_sigma my_pi (Tconst 13) = Vint 13

goal Test42 :
  eval_term my_sigma my_pi (Tvar 0) = Vint 42

goal Test0 :
  eval_term my_sigma my_pi (Tderef 0) = Vint 0

goal Test55 :
  eval_term my_sigma my_pi (Tbin (Tvar 0) Oplus (Tconst 13)) = Vint 55

goal Ass42 :
    let x = 0 in
    forall sigma' pi':env.
      one_step my_sigma my_pi (Sassign x (Tconst 42)) sigma' pi' Sskip ->
        IdMap.get sigma' x = Vint 42

goal If42 :
    let x = 0 in
    forall sigma1 pi1 sigma2 pi2:env, i:stmt.
      one_step my_sigma my_pi
        (Sif (Tbin (Tderef x) Ole (Tconst 10))
             (Sassign x (Tconst 13))
             (Sassign x (Tconst 42)))
        sigma1 pi1 i ->
      one_step sigma1 pi1 i sigma2 pi2 Sskip ->
        IdMap.get sigma2 x = Vint 13

end

(** {2 Hoare logic} *)

theory HoareLogic

use import Imp


(** Hoare logic rules (partial correctness) *)

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'

lemma skip_rule:
  forall q:fmla. valid_triple q Sskip q

lemma assign_rule:
  forall q:fmla, x id:ident, e:term.
  fresh_in_fmla id q ->
  valid_triple (Flet id e (subst q x id)) (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 assert_rule:
  forall f p:fmla. valid_fmla (Fimplies p f) ->
  valid_triple p (Sassert f) p

lemma assert_rule_ext:
  forall f p:fmla.
  valid_triple (Fimplies f p) (Sassert f) p

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 while_rule_ext:
  forall e:term, inv inv':fmla, i:stmt.
  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')

(*** frame rule ? *)

end

(** {2 WP calculus} *)

module WP

use import Imp

use set.Fset as Set

predicate assigns (sigma:env) (a:Set.set ident) (sigma':env) =
  forall i:ident. not (Set.mem i a) ->
    IdMap.get sigma i = IdMap.get sigma' i

lemma assigns_refl:
  forall sigma:env, a:Set.set ident. assigns sigma a sigma

lemma assigns_trans:
  forall sigma1 sigma2 sigma3:env, a:Set.set ident.
    assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
    assigns sigma1 a sigma3

lemma assigns_union_left:
  forall sigma sigma':env, s1 s2:Set.set ident.
    assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'

lemma assigns_union_right:
  forall sigma sigma':env, s1 s2:Set.set ident.
    assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'


predicate stmt_writes (i:stmt) (w:Set.set ident) =
  match i with
  | Sskip | Sassert _ -> true
  | Sassign id _ -> Set.mem id w
  | Sseq s1 s2 | Sif _ s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
  | Swhile _ _ s -> stmt_writes s w
  end


  let rec compute_writes (s:stmt) : Set.set ident
   ensures {
     forall sigma pi sigma' pi':env, n:int.
       many_steps sigma pi s sigma' pi' Sskip n ->
       assigns sigma result sigma' }
   variant { s }
  = match s with
    | Sskip -> Set.empty
    | Sassign i _ -> Set.singleton i
    | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
    | Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
    | Swhile _ _ s -> compute_writes s
    | Sassert _ -> Set.empty
    end

  val fresh_from_fmla (q:fmla) : ident
    ensures { fresh_in_fmla result q }

  val abstract_effects (i:stmt) (f:fmla) : fmla
    ensures { forall sigma pi:env. eval_fmla sigma pi result ->
        eval_fmla sigma pi f /\
(***
        forall sigma':env, w:Set.set ident.
        stmt_writes i w /\ assigns sigma w sigma' ->
        eval_fmla sigma' pi result
*)
        forall sigma' pi':env, n:int.
           many_steps sigma pi i sigma' pi' Sskip n ->
           eval_fmla sigma' pi' result
     }

  use import HoareLogic

  let rec wp (i:stmt) (q:fmla)
    ensures { valid_triple result i q }
    variant { i }
  = match i with
    | Sskip -> q
    | Sseq i1 i2 -> wp i1 (wp i2 q)
    | Sassign x e ->
        let id = fresh_from_fmla q in Flet id e (subst q x id)
    | Sif e i1 i2 ->
        Fand (Fimplies (Fterm e) (wp i1 q))
             (Fimplies (Fnot (Fterm e)) (wp i2 q))
    | Sassert f ->
       Fimplies f q (* liberal wp, no termination required *)
       (* Fand f q *) (* strict wp, termination required *)
    | Swhile e inv i ->
        Fand inv
          (abstract_effects i
            (Fand
                (Fimplies (Fand (Fterm e) inv) (wp i inv))
                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))

    end


end



(***
Local Variables:
compile-command: "why3ide wp2.mlw"
End:
*)