imp.mlw.bak

theory Imp

  use state.State
  use bool.Bool
  use int.Int
  use bv_op.BV_OP

  (* ************************ SYNTAX ************************ *)
  type aexpr =
    | Anum int
    | Avar id
    | Aadd aexpr aexpr 
    | Asub aexpr aexpr
    | Aaddu aexpr aexpr
    | Asubu aexpr aexpr

  type bexpr =
    | Btrue
    | Bfalse
    | Bnot bexpr
    | Beq aexpr aexpr
    | Ble aexpr aexpr
    | Band bexpr bexpr
    
  type com =
    | Cskip
    | Cassign id aexpr
    | Cseq com com
    | Cif bexpr com com
    | Cwhile bexpr com


  (* ************************  SEMANTICS ************************ *)
  function aeval  (st:state) (e:aexpr) : int =
    match e with
      | Anum n      -> n
      | Avar x      -> st[x]
      | Aadd e1 e2  -> aeval st e1 + aeval st e2
      | Asub e1 e2  -> aeval st e1 - aeval st e2
      | Aaddu e1 e2 -> bv_add (aeval st e1) (aeval st e2)
      | Asubu e1 e2 -> bv_sub (aeval st e1) (aeval st e2)
    end

  function beval (st:state) (b:bexpr) : bool =
    match b with
      | Btrue      -> true
      | Bfalse     -> false
      | Bnot b'    -> notb (beval st b')
      | Beq a1 a2  -> aeval st a1 = aeval st a2
      | Ble a1 a2  -> aeval st a1 <= aeval st a2  
      | Band b1 b2 -> andb (beval st b1) (beval st b2)
      
    end

  inductive ceval state com state =
    (* skip *)
    | E_Skip : forall m. ceval m Cskip m

    (* assignement *)
    | E_Ass  : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]

    (* sequence *)
    | E_Seq : forall cmd1 cmd2 m0 m1 m2.
        ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2

    (* if then else *)
    | E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
        ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1

    | E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
        ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1

    (* while *)
    | E_WhileEnd : forall cond m body. not beval m cond ->
        ceval m (Cwhile cond body) m

    | E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
        ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
          ceval mi (Cwhile cond body) mf
  
  (* Check for structural equality *)
  let rec eq_a(a b:aexpr) =
    variant { a, b }
    ensures { result = (a = b) }
    match (a, b) with
    | (Anum i1, Anum i2) -> i1 = i2
    | (Avar (Id id1), Avar (Id id2)) -> id1 = id2
    | (Aadd a1 a2, Aadd b1 b2) -> eq_a a1 b1 && eq_a a2 b2
    | (Asub a1 a2, Asub b1 b2) -> eq_a a1 b1 && eq_a a2 b2  
    | (Aaddu a1 a2, Aaddu b1 b2) -> eq_a a1 b1 && eq_a a2 b2
    | (Asubu a1 a2, Asubu b1 b2) -> eq_a a1 b1 && eq_a a2 b2   
    | _ -> false
    end
    
  let rec eq_b(a b:aexpr) =
    variant { a, b }
    ensures { result = (a = b) }
    match (a, b) with
    | Btrue, Btrue -> true
    | Bfalse, Bfalse -> true
    | Bnot x, Bnot y -> eq_b x y
    | Band x y, Band a b -> eq_b x a && eq_b y b
    | Beq x y, Beq a b -> eq_a x a && eq_a y b
    | Ble x y, Ble a b -> eq_a x a && eq_a y b
    | _ -> false
    end


  (* Determinstic semantics *)
  lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
      forall mf2. ([@inversion] ceval mi c mf2) -> mf1 = mf2

  lemma ceval_deterministic : forall c mi mf1 mf2.
      ceval mi c mf1 ->  ceval mi c mf2 -> mf1 = mf2

end