module VM_instr_spec

  meta compute_max_steps 0x10000

  use import int.Int
  use import list.List
  use import list.Length
  use import vm.Vm
  use import state.State
  use import logic.Compiler_logic

  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 }

  (* Iconst spec *)
  function iconst_post (n:int) : post 'a =
    fun _ p ms ms' -> forall s m. ms  = VMS p s m -> ms' = VMS (p+1) (push n s) m
  meta rewrite_def function iconst_post

  function iconst_fun (n:int) : machine_state -> machine_state =
    fun ms -> let (VMS p s m) = ms in VMS (p+1) (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 s m. ms = VMS p s m -> ms' = VMS (p+1) (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 s m) = ms in VMS (p+1) (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 s m. ms = VMS p (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 s m. ms = VMS p (push n2 (push n1 s)) m ->
     ms' = VMS (p+1) (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 (Cons n2 (Cons n1 s)) m -> VMS (p+1) (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 s m. transition c (VMS p (push n2 (push n1 s)) m)
 	                                 (VMS (p+1) (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 isubf () : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post sub }
    ensures { result.code.length --> 1 }
  = create_binop isub sub

  let imulf () : hl 'a
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post mul }
    ensures { result.code.length --> 1 }
  = create_binop imul mul

  (* 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 s m. ms = VMS p s m -> ms' = VMS (p + 1 + ofs) s m
  meta rewrite_def function ibranch_post

  function ibranch_fun (ofs:ofs) : machine_state -> machine_state =
    fun ms -> let (VMS p s m) = ms in VMS (p+1+ofs) 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 s m. ms = VMS p (push n2 (push n1 s)) m ->
      (cond n1 n2 -> ms' = VMS (p + ofs + 1) s m) /\
      (not cond n1 n2 -> ms' = VMS (p+1) 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 (Cons n2 (Cons n1 s)) m ->
        if cond n1 n2 then VMS (p+ofs+1) s m else VMS (p+1) 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 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 (push n2 (push n1 s)) m) (VMS p2 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 s m. ms = VMS p (push n s) m
  meta rewrite_def function isetvar_pre

  function isetvar_post (x:id) : post 'a =
    fun _ p ms ms' -> forall s n m.
      ms = VMS p (push n s) m -> ms' = VMS (p+1) 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 (Cons n s) m -> VMS (p+1) 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