examples/double_wp/specs.mlw

   1
   2 module VM_instr_spec
   3
   4   meta compute_max_steps 0x10000
   5
   6   use int.Int
   7   use list.List
   8   use list.Length
   9   use vm.Vm
  10   use state.State
  11   use logic.Compiler_logic
  12
  13   function ifun_post (f:machine_state -> machine_state) : post 'a =
  14     fun _ _ ms ms' -> ms' = f ms
  15   meta rewrite_def function ifun_post
  16
  17   (* General specification builder for determinstic machine
  18      instructions. *)
  19   let ifunf (ghost pre:pre 'a) (code_f:code)
  20     (ghost f:machine_state -> machine_state) : hl 'a
  21     requires { forall c p. codeseq_at c p code_f ->
  22         forall x ms. pre x p ms -> transition c ms (f ms) }
  23     ensures { result.pre --> pre }
  24     ensures { result.post --> ifun_post f }
  25     ensures { result.code --> code_f }
  26   = { pre = pre; code = code_f; post = ifun_post f }
  27
  28   (* Iconst spec *)
  29   function iconst_post (n:int) : post 'a =
  30     fun _ p ms ms' -> forall s m. ms  = VMS p s m -> ms' = VMS (p+1) (push n s) m
  31   meta rewrite_def function iconst_post
  32
  33   function iconst_fun (n:int) : machine_state -> machine_state =
  34     fun ms -> let (VMS p s m) = ms in VMS (p+1) (push n s) m
  35   meta rewrite_def function iconst_fun
  36
  37   let iconstf (n: int) : hl 'a
  38     ensures { result.pre --> trivial_pre }
  39     ensures { result.post --> iconst_post n }
  40     ensures { result.code.length --> 1 }
  41   = hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post
  42
  43   (* Ivar spec *)
  44   function ivar_post (x:id) : post 'a =
  45     fun _ p ms ms' -> forall s m. ms = VMS p s m -> ms' = VMS (p+1) (push m[x] s) m
  46   meta rewrite_def function ivar_post
  47
  48   function ivar_fun (x:id) : machine_state -> machine_state =
  49     fun ms -> let (VMS p s m) = ms in VMS (p+1) (push m[x] s) m
  50   meta rewrite_def function ivar_fun
  51
  52   let ivarf (x: id) : hl 'a
  53     ensures { result.pre --> trivial_pre }
  54     ensures { result.post --> ivar_post x }
  55     ensures { result.code.length --> 1 }
  56   = hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post
  57
  58   (* Binary arithmetic operators specification (Iadd, Isub, Imul)
  59      via a generic builder. *)
  60   type binop = int -> int -> int
  61
  62   constant ibinop_pre : pre 'a =
  63     fun _ p ms -> exists n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m
  64   meta rewrite_def function ibinop_pre
  65
  66   function ibinop_post (op : binop) : post 'a =
  67    fun _ p ms ms' -> forall n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m ->
  68      ms' = VMS (p+1) (push (op n1 n2) s) m
  69   meta rewrite_def function ibinop_post
  70
  71   function ibinop_fun (op:binop) : machine_state -> machine_state =
  72     fun ms -> match ms with
  73       | VMS p (Cons n2 (Cons n1 s)) m -> VMS (p+1) (push (op n1 n2) s) m
  74       | _ -> ms
  75       end
  76   meta rewrite_def function ibinop_fun
  77
  78   let create_binop (code_b:code) (ghost op:binop) : hl 'a
  79     requires { forall c p. codeseq_at c p code_b ->
  80       forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
  81                                          (VMS (p+1) (push (op n1 n2) s) m) }
  82     ensures { result.pre --> ibinop_pre }
  83     ensures { result.post --> ibinop_post op }
  84     ensures { result.code.length --> code_b.length }
  85   = hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post
  86
  87   constant plus : binop = fun x y -> x + y
  88   meta rewrite_def function plus
  89
  90   constant sub : binop = fun x y -> x - y
  91   meta rewrite_def function sub
  92
  93   constant mul : binop = fun x y -> x * y
  94   meta rewrite_def function mul
  95
  96   let iaddf () : hl 'a
  97     ensures { result.pre --> ibinop_pre }
  98     ensures { result.post --> ibinop_post plus }
  99     ensures { result.code.length --> 1 }
 100   = create_binop iadd plus
 101
 102   let isubf () : hl 'a
 103     ensures { result.pre --> ibinop_pre }
 104     ensures { result.post --> ibinop_post sub }
 105     ensures { result.code.length --> 1 }
 106   = create_binop isub sub
 107
 108   let imulf () : hl 'a
 109     ensures { result.pre --> ibinop_pre }
 110     ensures { result.post --> ibinop_post mul }
 111     ensures { result.code.length --> 1 }
 112   = create_binop imul mul
 113
 114   (* Inil spec *)
 115   function inil_post : post 'a =
 116     fun _ _ ms ms' -> ms = ms'
 117   meta rewrite_def function inil_post
 118
 119   let inil () : hl 'a
 120     ensures { result.pre --> trivial_pre }
 121     ensures { result.post --> inil_post }
 122     ensures { result.code.length --> 0 }
 123   = { pre = trivial_pre; code = Nil; post = inil_post }
 124
 125   (* Ibranch specification *)
 126   function ibranch_post (ofs: ofs) : post 'a =
 127     fun _ p ms ms' -> forall s m. ms = VMS p s m -> ms' = VMS (p + 1 + ofs) s m
 128   meta rewrite_def function ibranch_post
 129
 130   function ibranch_fun (ofs:ofs) : machine_state -> machine_state =
 131     fun ms -> let (VMS p s m) = ms in VMS (p+1+ofs) s m
 132   meta rewrite_def function ibranch_fun
 133
 134   let ibranchf (ofs:ofs) : hl 'a
 135     ensures { result.pre --> trivial_pre }
 136     ensures { result.post --> ibranch_post ofs }
 137     ensures { result.code.length --> 1 }
 138   = let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in
 139     hoare trivial_pre cf (ibranch_post ofs)
 140
 141   (* Conditional jump specification via a generic builder. *)
 142   type cond = int -> int -> bool
 143
 144   function icjump_post (cond:cond) (ofs:ofs) : post 'a =
 145     fun _ p ms ms' -> forall n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m ->
 146       (cond n1 n2 -> ms' = VMS (p + ofs + 1) s m) /\
 147       (not cond n1 n2 -> ms' = VMS (p+1) s m)
 148   meta rewrite_def function icjump_post
 149
 150   function icjump_fun (cond:cond) (ofs:ofs) : machine_state -> machine_state =
 151     fun ms -> match ms with
 152       | VMS p (Cons n2 (Cons n1 s)) m ->
 153         if cond n1 n2 then VMS (p+ofs+1) s m else VMS (p+1) s m
 154       | _ -> ms
 155       end
 156   meta rewrite_def function icjump_fun
 157
 158   let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:ofs) : hl 'a
 159     requires { forall c p1 n1 n2 s m. codeseq_at c p1 code_cd ->
 160       let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in
 161       transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
 162     ensures { result.pre --> ibinop_pre }
 163     ensures { result.post --> icjump_post cond ofs }
 164     ensures { result.code.length --> code_cd.length }
 165   = let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
 166     hoare ibinop_pre c (icjump_post cond ofs)
 167
 168   (*  binary Boolean operators specification (Ibeq, Ibne, Ible, Ibgt) *)
 169   constant beq : cond = fun x y -> x = y
 170   meta rewrite_def function beq
 171
 172   constant bne : cond = fun x y -> x <> y
 173   meta rewrite_def function bne
 174
 175   constant ble : cond = fun x y -> x <= y
 176   meta rewrite_def function ble
 177
 178   constant bgt : cond = fun x y -> x > y
 179   meta rewrite_def function bgt
 180
 181   let ibeqf (ofs:ofs) : hl 'a
 182     ensures { result.pre --> ibinop_pre }
 183     ensures { result.post --> icjump_post beq ofs }
 184     ensures { result.code.length --> 1 }
 185   = create_cjump (ibeq ofs) beq ofs
 186
 187   let ibnef (ofs:ofs) : hl 'a
 188     ensures { result.pre --> ibinop_pre }
 189     ensures { result.post --> icjump_post bne ofs }
 190     ensures { result.code.length --> 1 }
 191   = create_cjump (ibne ofs) bne ofs
 192
 193   let iblef (ofs:ofs) : hl 'a
 194     ensures { result.pre --> ibinop_pre }
 195     ensures { result.post --> icjump_post ble ofs }
 196     ensures { result.code.length --> 1 }
 197   = create_cjump (ible ofs) ble ofs
 198
 199   let ibgtf (ofs:ofs) : hl 'a
 200     ensures { result.pre --> ibinop_pre }
 201     ensures { result.post --> icjump_post bgt ofs }
 202     ensures { result.code.length --> 1 }
 203   = create_cjump (ibgt ofs) bgt ofs
 204
 205   (* Isetvar specification *)
 206   constant isetvar_pre : pre 'a =
 207     fun _ p ms -> exists n s m. ms = VMS p (push n s) m
 208   meta rewrite_def function isetvar_pre
 209
 210   function isetvar_post (x:id) : post 'a =
 211     fun _ p ms ms' -> forall s n m.
 212       ms = VMS p (push n s) m -> ms' = VMS (p+1) s m[x <- n]
 213   meta rewrite_def function isetvar_post
 214
 215   function isetvar_fun (x:id) : machine_state -> machine_state =
 216     fun ms -> match ms with
 217       | VMS p (Cons n s) m -> VMS (p+1) s m[x <- n]
 218       | _ -> ms
 219       end
 220   meta rewrite_def function isetvar_fun
 221
 222   let isetvarf (x: id) : hl 'a
 223     ensures { result.pre --> isetvar_pre }
 224     ensures { result.post --> isetvar_post x }
 225     ensures { result.code.length --> 1 }
 226   = let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in
 227     hoare isetvar_pre c (isetvar_post x)
 228
 229 end