1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/assembly/vm/".
17 include "assembly/byte.ma".
19 definition addr ≝ nat.
21 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
23 coercion cic:/matita/assembly/vm/addr_of_byte.con.
25 inductive opcode: Type ≝
26 ADDd: opcode (* 3 clock, 171 *)
27 | BEQ: opcode (* 3, 55 *)
28 | BRA: opcode (* 3, 48 *)
29 | DECd: opcode (* 5, 58 *)
30 | LDAi: opcode (* 2, 166 *)
31 | LDAd: opcode (* 3, 182 *)
32 | STAd: opcode. (* 3, 183 *)
34 let rec cycles_of_opcode op : nat ≝
45 definition opcodemap ≝
46 [ couple ? ? ADDd (mk_byte xA xB);
47 couple ? ? BEQ (mk_byte x3 x7);
48 couple ? ? BRA (mk_byte x3 x0);
49 couple ? ? DECd (mk_byte x3 xA);
50 couple ? ? LDAi (mk_byte xA x6);
51 couple ? ? LDAd (mk_byte xB x6);
52 couple ? ? STAd (mk_byte xB x7) ].
54 definition opcode_of_byte ≝
69 definition magic_of_opcode ≝
80 definition opcodeeqb ≝
81 λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
83 definition byte_of_opcode : opcode → byte ≝
91 match opcodeeqb op op' with
98 notation "hvbox(# break a)"
99 non associative with precedence 80
100 for @{ 'byte_of_opcode $a }.
101 interpretation "byte_of_opcode" 'byte_of_opcode a =
102 (cic:/matita/assembly/vm/byte_of_opcode.con a).
104 record status : Type ≝ {
115 λf: addr → byte.λa.λv.λx.
120 lemma update_update_a_a:
122 update (update s a v1) a v2 b = update s a v2 b.
130 lemma update_update_a_b:
133 update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
137 apply (bool_elim ? (eqb b a1)); intros;
138 apply (bool_elim ? (eqb b a2)); intros;
141 rewrite < (eqb_true_to_eq ? ? H1);
142 apply eqb_true_to_eq;
148 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
151 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
152 [ rewrite > (eqb_true_to_eq ? ? H);
159 ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
162 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
170 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
173 rewrite > not_eq_to_eqb_false; simplify;
180 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
183 λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
184 let opc ≝ opcode_of_byte (mem pc) in
185 let op1 ≝ mem (S pc) in
186 let clk' ≝ cycles_of_opcode opc in
187 match eqb (S clk) clk' with
191 let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
192 let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
193 let c' ≝ match res with [ couple _ c' ⇒ c'] in
194 mk_status acc' (2 + pc) spc
195 (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
200 [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *)
201 (* FIXME: can't work - address truncated to 8 bits *)
211 acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
212 (* FIXME: same as above *)
219 let x ≝ bpred (mem op1) in (* signed!!! *)
220 let mem' ≝ update mem op1 x in
221 mk_status acc (2 + pc) spc
222 (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
224 mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
227 mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
229 mk_status acc (2 + pc) spc zf cf
230 (update mem op1 acc) 0
234 acc pc spc zf cf mem (S clk)
237 let rec execute s n on n ≝
240 | S n' ⇒ execute (tick s) n'
244 ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
246 generalize in match s; clear s;
261 (∀a. mem s a = mem s' a) →