specs.mlw

module VM_instr_spec

  meta compute_max_steps 0x10000

  use int.Int
  use list.List
  use list.Length
  use vm.Vm
  use state.State
  use state.Reg
  use logic.Compiler_logic
  use bv_op.BV_OP

  function ifun_post (f:machine_state -> machine_state) : post 'a =
    fun _ _ ms ms' -> ms' = f ms
  meta rewrite_def function ifun_post 

  (* General specification builder for determinstic machine
     instructions. *)
  let ifunf (ghost pre:pre 'a) (code_f:code)
    (ghost f:machine_state -> machine_state) : hl 'a
    requires { forall c p. codeseq_at c p code_f ->
        forall x ms. pre x p ms -> transition c ms (f ms) }
    ensures { result.pre --> pre }
    ensures { result.post --> ifun_post f }
    ensures { result.code --> code_f }
  = { pre = pre; code = code_f; post = ifun_post f }

  (* Register based VM instructions *)

  (* Iimm spec *)
  function iimm_post (x:idr) (n:int) : post 'a =
    fun _ p ms ms' -> forall s r m. ms  = VMS p r s m -> ms' = VMS (p+1) (write r x n) s m
  meta rewrite_def function iimm_post

  function iimm_fun (x:idr) (n:int) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p+1) (write r x n) s m
  meta rewrite_def function iimm_fun

  let iimmf (x:idr) (n: int) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> iimm_post x n }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (iimm x n) (iimm_fun x n)) (iimm_post x n)
  
  (* Iload spec *)
  function iload_post (x:idr) (n:id) : post 'a =
    fun _ p ms ms' -> forall s r m. ms  = VMS p r s m -> ms' = VMS (p+1) (write r x m[n]) s m
  meta rewrite_def function iload_post

  function iload_fun (x:idr) (n:id) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p+1) (write r x m[n]) s m
  meta rewrite_def function iload_fun

  let iloadf (x:idr) (n: id) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> iload_post x n }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (iload x n) (iload_fun x n)) (iload_post x n)
  
  (* Istore spec *)
  function istore_post (x:idr) (n:id) : post 'a =
    fun _ p ms ms' -> forall s r m. ms  = VMS p r s m -> ms' = VMS (p+1) r s m[n <- read r x] 
  meta rewrite_def function istore_post

  function istore_fun (x:idr) (n:id) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p+1) r s m[n <- read r x]
  meta rewrite_def function istore_fun

  let istoref (x:idr) (n: id) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> istore_post x n }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (istore x n) (istore_fun x n)) (istore_post x n)
  
  (* Ipush spec *)
  function ipush_post (x:idr) : post 'a =
    fun _ p ms ms' -> forall s r m. ms  = VMS p r s m -> ms' = VMS (p + 1) r (push (read r x) s) m 
  meta rewrite_def function ipush_post

  function ipush_fun (x:idr) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p + 1) r (push (read r x) s) m          
  meta rewrite_def function ipush_fun

  let ipushf (x:idr) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ipush_post x }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (ipushr x) (ipush_fun x)) (ipush_post x)
  
  (* Ipop spec *)
  constant ipop_pre : pre 'a =
    fun _ p ms -> exists n r s m. ms = VMS p r (push n s) m
  meta rewrite_def function ipop_pre

  function ipop_post (x:idr) : post 'a =
    fun _ p ms ms' -> forall s r n m. ms = VMS p r (push n s) m-> ms' = VMS (p + 1) (write r x n) s m
  meta rewrite_def function ipop_post

  function ipop_fun (x:idr) : machine_state -> machine_state =
    fun ms ->
      match ms with
      | VMS p r (Cons n s) m ->  VMS (p + 1) (write r x n) s m
      | _ -> ms (* fail *)
      end      
  meta rewrite_def function ipop_fun

  let ipopf (x:idr) : hl 'a
    ensures { result.pre --> ipop_pre }
    ensures { result.post --> ipop_post x }
    ensures { result.code.length --> 1 }
  = hoare ipop_pre ($ ifunf ipop_pre (ipopr x) (ipop_fun x)) (ipop_post x)
  
  (* Iaddr spec *)
  function iaddr_post (x1 x2 x3:idr) : post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (p+1) (write r x3 (read r x1 + read r x2)) s m
  meta rewrite_def function iaddr_post

  function iaddr_fun (x1 x2 x3:idr) : machine_state -> machine_state =
    fun ms -> 
      let (VMS p r s m) = ms in 
      VMS (p+1) (write r x3 (read r x1 + read r x2)) s m
  meta rewrite_def function iaddr_fun

  let iaddrf (x1 x2 x3: idr) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> iaddr_post x1 x2 x3}
    ensures { result.code.length --> 1 }
  = 
    let c = $ ifunf trivial_pre (iaddr x1 x2 x3) (iaddr_fun x1 x2 x3) in
    hoare trivial_pre c (iaddr_post x1 x2 x3)
  
  (* Iaddur spec *)
  function iaddur_post (x1 x2 x3:idr) : post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (p+1) (write r x3 (bv_add (read r x1) (read r x2))) s m
  meta rewrite_def function iaddur_post

  function iaddur_fun (x1 x2 x3:idr) : machine_state -> machine_state =
    fun ms -> 
      let (VMS p r s m) = ms in 
      VMS (p+1) (write r x3 (bv_add (read r x1) (read r x2))) s m
  meta rewrite_def function iaddur_fun

  let iaddurf (x1 x2 x3: idr) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> iaddur_post x1 x2 x3}
    ensures { result.code.length --> 1 }
  = 
    let c = $ ifunf trivial_pre (iaddur x1 x2 x3) (iaddur_fun x1 x2 x3) in
    hoare trivial_pre c (iaddur_post x1 x2 x3)
  
  (* Isubr spec *)
  function isubr_post (x1 x2 x3:idr) : post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (p + 1) (write r x3 (read r x1 - read r x2)) s m
  meta rewrite_def function isubr_post

  function isubr_fun (x1 x2 x3:idr) : machine_state -> machine_state =
    fun ms -> 
      let (VMS p r s m) = ms in 
      VMS (p + 1) (write r x3 (read r x1 - read r x2)) s m
  meta rewrite_def function isubr_fun

  let isubrf (x1 x2 x3: idr) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> isubr_post x1 x2 x3}
    ensures { result.code.length --> 1 }
  = 
    let c = $ ifunf trivial_pre (isubr x1 x2 x3) (isubr_fun x1 x2 x3) in
    hoare trivial_pre c (isubr_post x1 x2 x3)
  
  (* Isubur spec *)
  function isubur_post (x1 x2 x3:idr) : post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (p+1) (write r x3 (bv_sub (read r x1) (read r x2))) s m
  meta rewrite_def function isubur_post

  function isubur_fun (x1 x2 x3:idr) : machine_state -> machine_state =
    fun ms -> 
      let (VMS p r s m) = ms in 
      VMS (p+1) (write r x3 (bv_sub (read r x1) (read r x2))) s m
  meta rewrite_def function isubur_fun

  let isuburf (x1 x2 x3: idr) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> isubur_post x1 x2 x3}
    ensures { result.code.length --> 1 }
  = 
    let c = $ ifunf trivial_pre (isubur x1 x2 x3) (isubur_fun x1 x2 x3) in
    hoare trivial_pre c (isubur_post x1 x2 x3)
  
  (* Ibeqr spec *)
  function ibeqr_post (x1:idr) (x2:idr) (ofs:int): post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (if read r x1 = read r x2 then p + 1 + ofs else p + 1) r s m
  meta rewrite_def function ibeqr_post

  function ibeqr_fun (x1:idr) (x2:idr) (ofs:int) : machine_state -> machine_state =
    fun ms -> 
    let (VMS p r s m) = ms in 
    VMS (if read r x1 = read r x2 then p + 1 + ofs else p + 1) r s m
  meta rewrite_def function ibeqr_fun

  let ibeqrf (x1:idr) (x2: idr) (ofs:int) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ibeqr_post x1 x2 ofs }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (ibeqr x1 x2 ofs) (ibeqr_fun x1 x2 ofs)) (ibeqr_post x1 x2 ofs)
  
  (* Ibner spec *)
  function ibner_post (x1:idr) (x2:idr) (ofs:int): post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (if read r x1 <> read r x2 then p + 1 + ofs else p + 1) r s m
  meta rewrite_def function ibner_post

  function ibner_fun (x1:idr) (x2:idr) (ofs:int) : machine_state -> machine_state =
    fun ms -> 
    let (VMS p r s m) = ms in 
    VMS (if read r x1 <> read r x2 then p + 1 + ofs else p + 1) r s m
  meta rewrite_def function ibner_fun

  let ibnerf (x1:idr) (x2: idr) (ofs:int) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ibner_post x1 x2 ofs }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (ibner x1 x2 ofs) (ibner_fun x1 x2 ofs)) (ibner_post x1 x2 ofs)
  
  (* Ibler spec *)
  function ibler_post (x1:idr) (x2:idr) (ofs:int): post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (if read r x1 <= read r x2 then p + 1 + ofs else p + 1) r s m
  meta rewrite_def function ibler_post

  function ibler_fun (x1:idr) (x2:idr) (ofs:int) : machine_state -> machine_state =
    fun ms -> 
    let (VMS p r s m) = ms in 
    VMS (if read r x1 <= read r x2 then p + 1 + ofs else p + 1) r s m
  meta rewrite_def function ibler_fun

  let iblerf (x1:idr) (x2: idr) (ofs:int) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ibler_post x1 x2 ofs }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (ibler x1 x2 ofs) (ibler_fun x1 x2 ofs)) (ibler_post x1 x2 ofs)

  (* Ibgtr spec *)
  function ibgtr_post (x1:idr) (x2:idr) (ofs:int): post 'a =
    fun _ p ms ms' -> forall s r m. 
      ms  = VMS p r s m -> 
      ms' = VMS (if read r x1 <= read r x2 then p + 1 else p + 1 + ofs) r s m
  meta rewrite_def function ibgtr_post

  function ibgtr_fun (x1:idr) (x2:idr) (ofs:int) : machine_state -> machine_state =
    fun ms -> 
    let (VMS p r s m) = ms in 
    VMS (if read r x1 <= read r x2 then p + 1 else p + 1 + ofs) r s m
  meta rewrite_def function ibgtr_fun

  let ibgtrf (x1:idr) (x2: idr) (ofs:int) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ibgtr_post x1 x2 ofs }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre (ibgtr x1 x2 ofs) (ibgtr_fun x1 x2 ofs)) (ibgtr_post x1 x2 ofs)
  
  (* original vm *)
  
  (* Iconst spec *)
  function iconst_post (n:int) : post 'a =
    fun _ p ms ms' -> forall s r m. ms  = VMS p r s m -> ms' = VMS (p+1) r (push n s) m
  meta rewrite_def function iconst_post

  function iconst_fun (n:int) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p+1) r (push n s) m
  meta rewrite_def function iconst_fun

  let iconstf (n: int) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> iconst_post n }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post

  (* Ivar spec *)
  function ivar_post (x:id) : post 'a =
    fun _ p ms ms' -> forall r s m. ms = VMS p r s m -> ms' = VMS (p+1) r (push m[x] s) m
  meta rewrite_def function ivar_post

  function ivar_fun (x:id) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p+1) r (push m[x] s) m
  meta rewrite_def function ivar_fun

  let ivarf (x: id) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ivar_post x }
    ensures { result.code.length --> 1 }
  = hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post

  (* Binary arithmetic operators specification (Iadd, Isub, Imul)
     via a generic builder. *)
  type binop = int -> int -> int

  constant ibinop_pre : pre 'a =
    fun _ p ms -> exists n1 n2 r s m. ms = VMS p r (push n2 (push n1 s)) m
  meta rewrite_def function ibinop_pre

  function ibinop_post (op : binop) : post 'a =
   fun _ p ms ms' -> forall n1 n2 r s m. ms = VMS p r (push n2 (push n1 s)) m ->
     ms' = VMS (p+1) r (push (op n1 n2) s) m
  meta rewrite_def function ibinop_post

  function ibinop_fun (op:binop) : machine_state -> machine_state =
    fun ms -> match ms with
      | VMS p r (Cons n2 (Cons n1 s)) m -> VMS (p+1) r (push (op n1 n2) s) m
      | _ -> ms
      end
  meta rewrite_def function ibinop_fun

  let create_binop (code_b:code) (ghost op:binop) : hl 'a
    requires { forall c p. 
      codeseq_at c p code_b ->
      forall n1 n2 r s m. transition c 
        (VMS p r (push n2 (push n1 s)) m)
 	      (VMS (p+1) r (push (op n1 n2) s) m) 
 	  }
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post op }
    ensures { result.code.length --> code_b.length }
  = hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post

  constant plus : binop = fun x y -> x + y
  meta rewrite_def function plus

  constant sub : binop = fun x y -> x - y
  meta rewrite_def function sub

  constant mul : binop = fun x y -> x * y
  meta rewrite_def function mul

  let iaddf () : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post plus }
    ensures { result.code.length --> 1 }
  = create_binop iadd plus
  
  let iadduf () : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post bv_add }
    ensures { result.code.length --> 1 }
  = create_binop iaddu bv_add

  let isubf () : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post sub }
    ensures { result.code.length --> 1 }
  = create_binop isub sub
  
  let isubuf () : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post bv_sub }
    ensures { result.code.length --> 1 }
  = create_binop isubu bv_sub

  (* Inil spec *)
  function inil_post : post 'a =
    fun _ _ ms ms' -> ms = ms'
  meta rewrite_def function inil_post

  let inil () : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> inil_post }
    ensures { result.code.length --> 0 }
  = { pre = trivial_pre; code = Nil; post = inil_post }

  (* Ibranch specification *)
  function ibranch_post (ofs: ofs) : post 'a =
    fun _ p ms ms' -> forall r s m. ms = VMS p r s m -> ms' = VMS (p + 1 + ofs) r s m
  meta rewrite_def function ibranch_post

  function ibranch_fun (ofs:ofs) : machine_state -> machine_state =
    fun ms -> let (VMS p r s m) = ms in VMS (p+1+ofs) r s m
  meta rewrite_def function ibranch_fun

  let ibranchf (ofs:ofs) : hl 'a
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ibranch_post ofs }
    ensures { result.code.length --> 1 }
  = let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in
    hoare trivial_pre cf (ibranch_post ofs)

  (* Conditional jump specification via a generic builder. *)
  type cond = int -> int -> bool

  function icjump_post (cond:cond) (ofs:ofs) : post 'a =
    fun _ p ms ms' -> forall n1 n2 r s m. ms = VMS p r (push n2 (push n1 s)) m ->
      (cond n1 n2 -> ms' = VMS (p + ofs + 1) r s m) /\
      (not cond n1 n2 -> ms' = VMS (p+1) r s m)
  meta rewrite_def function icjump_post

  function icjump_fun (cond:cond) (ofs:ofs) : machine_state -> machine_state =
    fun ms -> match ms with
      | VMS p r (Cons n2 (Cons n1 s)) m ->
        if cond n1 n2 then VMS (p+ofs+1) r s m else VMS (p+1) r s m
      | _ -> ms
      end
  meta rewrite_def function icjump_fun

  let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:ofs) : hl 'a
    requires { forall c p1 n1 n2 r s m. codeseq_at c p1 code_cd ->
      let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in
      transition c (VMS p1 r (push n2 (push n1 s)) m) (VMS p2 r s m) }
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post cond ofs }
    ensures { result.code.length --> code_cd.length }
  = let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
    hoare ibinop_pre c (icjump_post cond ofs)

  (*  binary Boolean operators specification (Ibeq, Ibne, Ible, Ibgt) *)
  constant beq : cond = fun x y -> x = y
  meta rewrite_def function beq

  constant bne : cond = fun x y -> x <> y
  meta rewrite_def function bne

  constant ble : cond = fun x y -> x <= y
  meta rewrite_def function ble

  constant bgt : cond = fun x y -> x > y
  meta rewrite_def function bgt

  let ibeqf (ofs:ofs) : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post beq ofs }
    ensures { result.code.length --> 1 }
  = create_cjump (ibeq ofs) beq ofs

  let ibnef (ofs:ofs) : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post bne ofs }
    ensures { result.code.length --> 1 }
  = create_cjump (ibne ofs) bne ofs

  let iblef (ofs:ofs) : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post ble ofs }
    ensures { result.code.length --> 1 }
  = create_cjump (ible ofs) ble ofs

  let ibgtf (ofs:ofs) : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post bgt ofs }
    ensures { result.code.length --> 1 }
  = create_cjump (ibgt ofs) bgt ofs

  (* Isetvar specification *)
  constant isetvar_pre : pre 'a =
    fun _ p ms -> exists n r s m. ms = VMS p r (push n s) m
  meta rewrite_def function isetvar_pre

  function isetvar_post (x:id) : post 'a =
    fun _ p ms ms' -> forall r s n m.
      ms = VMS p r (push n s) m -> ms' = VMS (p+1) r s m[x <- n]
  meta rewrite_def function isetvar_post

  function isetvar_fun (x:id) : machine_state -> machine_state =
    fun ms -> match ms with
      | VMS p r (Cons n s) m -> VMS (p+1) r s m[x <- n]
      | _ -> ms
      end
  meta rewrite_def function isetvar_fun

  let isetvarf (x: id) : hl 'a
    ensures { result.pre --> isetvar_pre }
    ensures { result.post --> isetvar_post x }
    ensures { result.code.length --> 1 }
  = let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in
    hoare isetvar_pre c (isetvar_post x)

end