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