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/".
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 record status : Type ≝ {
109 λf: addr → byte.λa.λv.λx.
114 lemma update_update_a_a:
116 update (update s a v1) a v2 b = update s a v2 b.
124 lemma update_update_a_b:
127 update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
131 apply (bool_elim ? (eqb b a1)); intros;
132 apply (bool_elim ? (eqb b a2)); intros;
135 rewrite < (eqb_true_to_eq ? ? H1);
136 apply eqb_true_to_eq;
142 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
145 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
146 [ rewrite > (eqb_true_to_eq ? ? H);
153 ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
156 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
164 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
167 rewrite > not_eq_to_eqb_false; simplify;
174 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
177 λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
178 let opc ≝ opcode_of_byte (mem pc) in
179 let op1 ≝ mem (S pc) in
180 let clk' ≝ cycles_of_opcode opc in
181 match eqb (S clk) clk' with
185 let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
186 let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
187 let c' ≝ match res with [ couple _ c' ⇒ c'] in
188 mk_status acc' (2 + pc) spc
189 (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
194 [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *)
195 (* FIXME: can't work - address truncated to 8 bits *)
205 acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
206 (* FIXME: same as above *)
213 let x ≝ bpred (mem op1) in (* signed!!! *)
214 let mem' ≝ update mem op1 x in
215 mk_status acc (2 + pc) spc
216 (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
218 mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
221 mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
223 mk_status acc (2 + pc) spc zf cf
224 (update mem op1 acc) 0
228 acc pc spc zf cf mem (S clk)
231 let rec execute s n on n ≝
234 | S n' ⇒ execute (tick s) n'
238 ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
240 generalize in match s; clear s;
255 (∀a. mem s a = mem s' a) →