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 ≝ {
114 notation "{hvbox('Acc' ≝ acc ; break 'Pc' ≝ pc ; break 'Spc' ≝ spc ; break 'Fz' ≝ fz ; break 'Fc' ≝ fc ; break 'M' ≝ m ; break 'Clk' ≝ clk)}"
115 non associative with precedence 80 for
116 @{ 'mkstatus $acc $pc $spc $fz $fc $m $clk }.
118 interpretation "mk_status" 'mkstatus acc pc spc fz fc m clk =
119 (cic:/matita/assembly/vm/status.ind#xpointer(1/1/1) acc pc spc fz fc m clk).
122 λf: addr → byte.λa.λv.λx.
127 notation "hvbox(m break {a ↦ break v})" non associative with precedence 80 for
128 @{ 'update $m $a $v }.
130 notation "hvbox(m break {a ↦ break v} \nbsp x)" non associative with precedence 80 for
131 @{ 'update4 $m $a $v $x }.
133 interpretation "update" 'update m a v =
134 (cic:/matita/assembly/vm/update.con m a v).
136 interpretation "update4" 'update4 m a v x =
137 (cic:/matita/assembly/vm/update.con m a v x).
139 lemma update_update_a_a:
141 update (update s a v1) a v2 b = update s a v2 b.
149 lemma update_update_a_b:
152 update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
156 apply (bool_elim ? (eqb b a1)); intros;
157 apply (bool_elim ? (eqb b a2)); intros;
160 rewrite < (eqb_true_to_eq ? ? H1);
161 apply eqb_true_to_eq;
167 lemma eq_update_s_a_sa: ∀s,a,b. update s a (s a) b = s b.
170 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
171 [ rewrite > (eqb_true_to_eq ? ? H);
178 ∀s,s',a,v,b. (a ≠ b → s b = s' b) → update s a v b = update s' a v b.
181 apply (bool_elim ? (eqb b a) ? ?); simplify; intros;
189 lemma not_eq_a_b_to_eq_update_a_b: ∀s,a,b,v. a ≠ b → update s a v b = s b.
192 rewrite > not_eq_to_eqb_false; simplify;
199 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
202 λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
203 let opc ≝ opcode_of_byte (mem pc) in
204 let op1 ≝ mem (S pc) in
205 let clk' ≝ cycles_of_opcode opc in
206 match eqb (S clk) clk' with
210 let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
211 let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
212 let c' ≝ match res with [ couple _ c' ⇒ c'] in
213 mk_status acc' (2 + pc) spc
214 (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
219 [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *)
220 (* FIXME: can't work - address truncated to 8 bits *)
230 acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
231 (* FIXME: same as above *)
238 let x ≝ bpred (mem op1) in (* signed!!! *)
239 let mem' ≝ update mem op1 x in
240 mk_status acc (2 + pc) spc
241 (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
243 mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
246 mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
248 mk_status acc (2 + pc) spc zf cf
249 (update mem op1 acc) 0
253 acc pc spc zf cf mem (S clk)
256 let rec execute s n on n ≝
259 | S n' ⇒ execute (tick s) n'
263 ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
265 generalize in match s; clear s;
280 (∀a. mem s a = mem s' a) →