From 8451a479e2cdaddd1da2daee8c8074412ff4d43d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 16 Jul 2007 14:51:18 +0000 Subject: [PATCH] assembly.ma splitted into many files --- helm/software/matita/library/assembly/byte.ma | 261 ++++++ .../assembly/{assembly.ma => exadecimal.ma} | 832 +----------------- .../software/matita/library/assembly/extra.ma | 81 ++ helm/software/matita/library/assembly/test.ma | 297 +++++++ helm/software/matita/library/assembly/vm.ma | 225 +++++ 5 files changed, 871 insertions(+), 825 deletions(-) create mode 100644 helm/software/matita/library/assembly/byte.ma rename helm/software/matita/library/assembly/{assembly.ma => exadecimal.ma} (62%) create mode 100644 helm/software/matita/library/assembly/extra.ma create mode 100644 helm/software/matita/library/assembly/test.ma create mode 100644 helm/software/matita/library/assembly/vm.ma diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma new file mode 100644 index 000000000..f18effeab --- /dev/null +++ b/helm/software/matita/library/assembly/byte.ma @@ -0,0 +1,261 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/assembly/byte". + +include "exadecimal.ma". + +record byte : Type ≝ { + bh: exadecimal; + bl: exadecimal +}. + +definition eqbyte ≝ + λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b'). + +definition plusbyte ≝ + λb1,b2,c. + match plusex (bl b1) (bl b2) c with + [ couple l c' ⇒ + match plusex (bh b1) (bh b2) c' with + [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]]. + +definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b). + +coercion cic:/matita/assembly/byte/nat_of_byte.con. + +definition byte_of_nat ≝ + λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n). + +lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b. + intros; + elim b; + elim e; + elim e1; + reflexivity. +qed. + +lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256. + intro; + unfold nat_of_byte; + letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H; + letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K; + unfold lt in H K ⊢ %; + letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H; + letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K; + apply le_S_S; + cut (16*bh b ≤ 16*15); + [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf; + simplify in Hf:(? ? %); + assumption + | autobatch + ] +qed. + +lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256. + intro; + letin H ≝ (lt_nat_of_byte_256 (byte_of_nat n)); clearbody H; + rewrite < (lt_to_eq_mod ? ? H); clear H; + unfold byte_of_nat; + unfold nat_of_byte; + change with ((16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n) \mod 256 = n \mod 256); + letin H ≝ (div_mod n 16 ?); clearbody H; [ autobatch | ]; + rewrite > symmetric_times in H; + rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? % ?) ?) ?); + rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?); + rewrite > H in ⊢ (? ? ? (? % ?)); clear H; + rewrite > mod_plus in ⊢ (? ? % ?); + rewrite > mod_plus in ⊢ (? ? ? %); + apply eq_mod_to_eq_plus_mod; + rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch]; + rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch]; + rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ]; + rewrite < mod_mod in ⊢ (? ? % ?); + [ reflexivity + | autobatch + ]. +qed. + +axiom eq_nat_of_byte_n_nat_of_byte_mod_n_256: + ∀n. byte_of_nat n = byte_of_nat (n \mod 256). + +lemma plusbyte_ok: + ∀b1,b2,c. + match plusbyte b1 b2 c with + [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256 + ]. + intros; + unfold plusbyte; + generalize in match (plusex_ok (bl b1) (bl b2) c); + elim (plusex (bl b1) (bl b2) c); + simplify in H ⊢ %; + generalize in match (plusex_ok (bh b1) (bh b2) t1); + elim (plusex (bh b1) (bh b2) t1); + simplify in H1 ⊢ %; + change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2); + unfold nat_of_byte; + letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1; + rewrite > distr_times_plus in K:(? ? ? %); + rewrite > symmetric_times in K:(? ? ? (? ? (? ? %))); + rewrite < associative_times in K:(? ? ? (? ? %)); + normalize in K:(? ? ? (? ? (? % ?))); + rewrite > symmetric_times in K:(? ? ? (? ? %)); + rewrite > sym_plus in ⊢ (? ? ? (? % ?)); + rewrite > associative_plus in ⊢ (? ? ? %); + letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K; + apply transitive_eq; [3: apply K' | skip | ]; + clear K'; + rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?); + rewrite > associative_plus in ⊢ (? ? (? % ?) ?); + rewrite > associative_plus in ⊢ (? ? % ?); + rewrite > associative_plus in ⊢ (? ? (? ? %) ?); + rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?); + rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?); + rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?); + rewrite < associative_plus in ⊢ (? ? (? ? %) ?); + rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?); + rewrite > H; clear H; + autobatch paramodulation. +qed. + +definition bpred ≝ + λb. + match eqex (bl b) x0 with + [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b)) + | false ⇒ mk_byte (bh b) (xpred (bl b)) + ]. + +lemma plusbyte_O_x: + ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false. + intros; + elim b; + elim e; + elim e1; + reflexivity. +qed. + +definition plusbytenc ≝ + λx,y. + match plusbyte x y false with + [couple res _ ⇒ res]. + +definition plusbytec ≝ + λx,y. + match plusbyte x y false with + [couple _ c ⇒ c]. + +lemma plusbytenc_O_x: + ∀x. plusbytenc (mk_byte x0 x0) x = x. + intros; + unfold plusbytenc; + rewrite > plusbyte_O_x; + reflexivity. +qed. + +axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256. + +theorem plusbytenc_ok: + ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256. + intros; + unfold plusbytenc; + generalize in match (plusbyte_ok b1 b2 false); + elim (plusbyte b1 b2 false); + simplify in H ⊢ %; + change with (nat_of_byte t = (b1 + b2) \mod 256); + rewrite < plus_n_O in H; + rewrite > H; clear H; + rewrite > mod_plus; + letin K ≝ (eq_nat_of_byte_mod t); clearbody K; + letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K'; + [ autobatch | ]; + autobatch paramodulation. +qed. + +lemma eq_eqbyte_x0_x0_byte_of_nat_S_false: + ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false. + intros; + unfold byte_of_nat; + cut (b < 15 ∨ b ≥ 15); + [ elim Hcut; + [ unfold eqbyte; + change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); + rewrite > eq_eqex_S_x0_false; + [ elim (eqex (bh (mk_byte x0 x0)) +(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify; +(* + alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con". + rewrite > andb_sym; +*) + reflexivity + | assumption + ] + | unfold eqbyte; + change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16))); + letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?); + [ autobatch + | unfold in H1; + apply le_S_S; + assumption + | clearbody K; + elim K; clear K; + rewrite > H2; + rewrite > eq_eqex_S_x0_false; + [ reflexivity + | unfold lt; + unfold lt in H; + rewrite < H2; + clear H2; clear a; clear H1; clear Hcut; + elim daemon (* trivial arithmetic property over <= and div *) + ] + ] + ] + | elim daemon + ]. +qed. + +lemma eq_bpred_S_a_a: + ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a. +elim daemon. (* + intros; + unfold byte_of_nat; + cut (a \mod 16 = 15 ∨ a \mod 16 < 15); + [ elim Hcut; + [ + | + ] + | autobatch + ].*) +qed. + +lemma plusbytenc_S: + ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n). + intros; + rewrite < byte_of_nat_nat_of_byte; + rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x); + rewrite < times_n_Sm; + rewrite > mod_plus; + rewrite < eq_nat_of_byte_mod in ⊢ (? ? (? (? (? ? %) ?)) ?); + rewrite > nat_of_byte_byte_of_nat; + rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); +elim daemon. +qed. + +lemma eq_plusbytec_x0_x0_x_false: + ∀x.plusbytec (mk_byte x0 x0) x = false. + intro; + elim x; + elim e; + elim e1; + reflexivity. +qed. diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/exadecimal.ma similarity index 62% rename from helm/software/matita/library/assembly/assembly.ma rename to helm/software/matita/library/assembly/exadecimal.ma index 4e2326de0..bf689de00 100644 --- a/helm/software/matita/library/assembly/assembly.ma +++ b/helm/software/matita/library/assembly/exadecimal.ma @@ -12,10 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/assembly/". +set "baseuri" "cic:/matita/assembly/exadecimal/". -include "nat/div_and_mod.ma". -include "list/list.ma". +include "extra.ma". inductive exadecimal : Type ≝ x0: exadecimal @@ -34,11 +33,6 @@ inductive exadecimal : Type ≝ | xD: exadecimal | xE: exadecimal | xF: exadecimal. - -record byte : Type ≝ { - bh: exadecimal; - bl: exadecimal -}. definition eqex ≝ λb1,b2. @@ -140,13 +134,6 @@ definition eqex ≝ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]]. - -definition eqbyte ≝ - λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b'). - -inductive cartesian_product (A,B: Type) : Type ≝ - couple: ∀a:A.∀b:B. cartesian_product A B. - definition plusex ≝ λb1,b2,c. match c with @@ -735,14 +722,6 @@ definition plusex ≝ ] . -definition plusbyte ≝ - λb1,b2,c. - match plusex (bl b1) (bl b2) c with - [ couple l c' ⇒ - match plusex (bh b1) (bh b2) c' with - [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]]. - -alias num (instance 0) = "natural number". definition nat_of_exadecimal ≝ λb. match b with @@ -764,11 +743,7 @@ definition nat_of_exadecimal ≝ | xF ⇒ 15 ]. -coercion cic:/matita/assembly/nat_of_exadecimal.con. - -definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b). - -coercion cic:/matita/assembly/nat_of_byte.con. +coercion cic:/matita/assembly/exadecimal/nat_of_exadecimal.con. let rec exadecimal_of_nat b ≝ match b with [ O ⇒ x0 | S b ⇒ @@ -788,48 +763,17 @@ let rec exadecimal_of_nat b ≝ match b with [ O ⇒ xE | S b ⇒ match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]]. -definition byte_of_nat ≝ - λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n). - -lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b. - intros; - elim b; - elim e; - elim e1; - reflexivity. -qed. - lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16. intro; elim b; simplify; + [ + |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con". + repeat (apply lt_S_S) + ]; autobatch. qed. -lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256. - intro; - unfold nat_of_byte; - letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H; - letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K; - unfold lt in H K ⊢ %; - letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H; - letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K; - apply le_S_S; - cut (16*bh b ≤ 16*15); - [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf; - simplify in Hf:(? ? %); - assumption - | autobatch - ] -qed. - -lemma le_to_lt: ∀n,m. n ≤ m → n < S m. - intros; - autobatch. -qed. - -axiom daemon: False. - lemma exadecimal_of_nat_mod: ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16). elim daemon. @@ -877,32 +821,6 @@ lemma exadecimal_of_nat_mod: ]*) qed. -(*lemma exadecimal_of_nat_elim: - ∀P:exadecimal → Prop. - (∀m. m < 16 → P (exadecimal_of_nat m)) → - ∀n. P (exadecimal_of_nat n). - intros; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - cases n; [ apply H; autobatch | ]; clear n; - cases n1; [ apply H; autobatch | ]; clear n1; - simplify; - elim daemon. -qed. -*) - axiom nat_of_exadecimal_exadecimal_of_nat: ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16. (* @@ -934,19 +852,6 @@ axiom nat_of_exadecimal_exadecimal_of_nat: qed. *) -lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256. - intro; - unfold byte_of_nat; - unfold nat_of_byte; - change with (16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n = n \mod 256); - rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?); - rewrite > nat_of_exadecimal_exadecimal_of_nat; - elim daemon. -qed. - -definition nat_of_bool ≝ - λb. match b with [ true ⇒ 1 | false ⇒ 0 ]. - lemma plusex_ok: ∀b1,b2,c. match plusex b1 b2 c with @@ -959,53 +864,6 @@ lemma plusex_ok: reflexivity. qed. -lemma plusbyte_ok: - ∀b1,b2,c. - match plusbyte b1 b2 c with - [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256 - ]. - intros; - unfold plusbyte; - generalize in match (plusex_ok (bl b1) (bl b2) c); - elim (plusex (bl b1) (bl b2) c); - simplify in H ⊢ %; - generalize in match (plusex_ok (bh b1) (bh b2) t1); - elim (plusex (bh b1) (bh b2) t1); - simplify in H1 ⊢ %; - change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2); - unfold nat_of_byte; - letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1; - rewrite > distr_times_plus in K:(? ? ? %); - rewrite > symmetric_times in K:(? ? ? (? ? (? ? %))); - rewrite < associative_times in K:(? ? ? (? ? %)); - normalize in K:(? ? ? (? ? (? % ?))); - rewrite > symmetric_times in K:(? ? ? (? ? %)); - rewrite > sym_plus in ⊢ (? ? ? (? % ?)); - rewrite > associative_plus in ⊢ (? ? ? %); - letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K; - apply transitive_eq; [3: apply K' | skip | ]; - clear K'; - rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?); - rewrite > associative_plus in ⊢ (? ? (? % ?) ?); - rewrite > associative_plus in ⊢ (? ? % ?); - rewrite > associative_plus in ⊢ (? ? (? ? %) ?); - rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?); - rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?); - rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?); - rewrite < associative_plus in ⊢ (? ? (? ? %) ?); - rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?); - rewrite > H; clear H; - autobatch paramodulation. -qed. - -(* -lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256. - intros; elim n; [ reflexivity | unfold byte_of_nat. -qed. -*) - -definition addr ≝ nat. - definition xpred ≝ λb. match b with @@ -1026,13 +884,6 @@ definition xpred ≝ | xE ⇒ xD | xF ⇒ xE ]. -definition bpred ≝ - λb. - match eqex (bl b) x0 with - [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b)) - | false ⇒ mk_byte (bh b) (xpred (bl b)) - ]. - (* Way too slow and subsumed by previous theorem lemma bpred_pred: ∀b. @@ -1047,362 +898,6 @@ lemma bpred_pred: qed. *) -definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b. - -coercion cic:/matita/assembly/addr_of_byte.con. - -inductive opcode: Type ≝ - ADDd: opcode (* 3 clock, 171 *) - | BEQ: opcode (* 3, 55 *) - | BRA: opcode (* 3, 48 *) - | DECd: opcode (* 5, 58 *) - | LDAi: opcode (* 2, 166 *) - | LDAd: opcode (* 3, 182 *) - | STAd: opcode. (* 3, 183 *) - -let rec cycles_of_opcode op : nat ≝ - match op with - [ ADDd ⇒ 3 - | BEQ ⇒ 3 - | BRA ⇒ 3 - | DECd ⇒ 5 - | LDAi ⇒ 2 - | LDAd ⇒ 3 - | STAd ⇒ 3 - ]. - -definition opcodemap ≝ - [ couple ? ? ADDd (mk_byte xA xB); - couple ? ? BEQ (mk_byte x3 x7); - couple ? ? BRA (mk_byte x3 x0); - couple ? ? DECd (mk_byte x3 xA); - couple ? ? LDAi (mk_byte xA x6); - couple ? ? LDAd (mk_byte xB x6); - couple ? ? STAd (mk_byte xB x7) ]. - -definition opcode_of_byte ≝ - λb. - let rec aux l ≝ - match l with - [ nil ⇒ ADDd - | cons c tl ⇒ - match c with - [ couple op n ⇒ - match eqbyte n b with - [ true ⇒ op - | false ⇒ aux tl - ]]] - in - aux opcodemap. - -definition magic_of_opcode ≝ - λop1. - match op1 with - [ ADDd ⇒ 0 - | BEQ ⇒ 1 - | BRA ⇒ 2 - | DECd ⇒ 3 - | LDAi ⇒ 4 - | LDAd ⇒ 5 - | STAd ⇒ 6 ]. - -definition opcodeeqb ≝ - λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2). - -definition byte_of_opcode : opcode → byte ≝ - λop. - let rec aux l ≝ - match l with - [ nil ⇒ mk_byte x0 x0 - | cons c tl ⇒ - match c with - [ couple op' n ⇒ - match opcodeeqb op op' with - [ true ⇒ n - | false ⇒ aux tl - ]]] - in - aux opcodemap. - -record status : Type ≝ { - acc : byte; - pc : addr; - spc : addr; - zf : bool; - cf : bool; - mem : addr → byte; - clk : nat -}. - -definition update ≝ - λf: addr → byte.λa.λv.λx. - match eqb x a with - [ true ⇒ v - | false ⇒ f x ]. - -lemma update_update_a_a: - ∀s,a,v1,v2,b. - update (update s a v1) a v2 b = update s a v2 b. - intros; - unfold update; - unfold update; - elim (eqb b a); - reflexivity. -qed. - -lemma update_update_a_b: - ∀s,a1,v1,a2,v2,b. - a1 ≠ a2 → - update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b. - intros; - unfold update; - unfold update; - apply (bool_elim ? (eqb b a1)); intros; - apply (bool_elim ? (eqb b a2)); intros; - simplify; - [ elim H; - rewrite < (eqb_true_to_eq ? ? H1); - apply eqb_true_to_eq; - assumption - |*: reflexivity - ]. -qed. - -definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n). - -definition tick ≝ - λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒ - let opc ≝ opcode_of_byte (mem pc) in - let op1 ≝ mem (S pc) in - let clk' ≝ cycles_of_opcode opc in - match eqb (S clk) clk' with - [ true ⇒ - match opc with - [ ADDd ⇒ - let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *) - let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in - let c' ≝ match res with [ couple _ c' ⇒ c'] in - mk_status acc' (2 + pc) spc - (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *) - | BEQ ⇒ - mk_status - acc - (match zf with - [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *) - (* FIXME: can't work - address truncated to 8 bits *) - | false ⇒ 2 + pc - ]) - spc - zf - cf - mem - 0 - | BRA ⇒ - mk_status - acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *) - (* FIXME: same as above *) - spc - zf - cf - mem - 0 - | DECd ⇒ - let x ≝ bpred (mem op1) in (* signed!!! *) - let mem' ≝ update mem op1 x in - mk_status acc (2 + pc) spc - (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *) - | LDAi ⇒ - mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0 - | LDAd ⇒ - let x ≝ mem op1 in - mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0 - | STAd ⇒ - mk_status acc (2 + pc) spc zf cf - (update mem op1 acc) 0 - ] - | false ⇒ - mk_status - acc pc spc zf cf mem (S clk) - ]]. - -let rec execute s n on n ≝ - match n with - [ O ⇒ s - | S n' ⇒ execute (tick s) n' - ]. - -lemma breakpoint: - ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2. - intros; - generalize in match s; clear s; - elim n1; - [ reflexivity - | simplify; - apply H; - ] -qed. - -notation "hvbox(# break a)" - non associative with precedence 80 -for @{ 'byte_of_opcode $a }. -interpretation "byte_of_opcode" 'byte_of_opcode a = - (cic:/matita/assembly/byte_of_opcode.con a). - -definition mult_source : list byte ≝ - [#LDAi; mk_byte x0 x0; (* A := 0 *) - #STAd; mk_byte x2 x0; (* Z := A *) - #LDAd; mk_byte x1 xF; (* (l1) A := Y *) - #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *) - #LDAd; mk_byte x2 x0; (* A := Z *) - #DECd; mk_byte x1 xF; (* Y := Y - 1 *) - #ADDd; mk_byte x1 xE; (* A += X *) - #STAd; mk_byte x2 x0; (* Z := A *) - #BRA; mk_byte xF x2; (* goto l1 *) - #LDAd; mk_byte x2 x0].(* (l2) *) - -definition mult_memory ≝ - λx,y.λa:addr. - match leb a 29 with - [ true ⇒ nth ? mult_source (mk_byte x0 x0) a - | false ⇒ - match eqb a 30 with - [ true ⇒ x - | false ⇒ y - ] - ]. - -definition mult_status ≝ - λx,y. - mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0. - -lemma plusbyte_O_x: - ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false. - intros; - elim b; - elim e; - elim e1; - reflexivity. -qed. - -definition plusbytenc ≝ - λx,y. - match plusbyte x y false with - [couple res _ ⇒ res]. - -definition plusbytec ≝ - λx,y. - match plusbyte x y false with - [couple _ c ⇒ c]. - -lemma plusbytenc_O_x: - ∀x. plusbytenc (mk_byte x0 x0) x = x. - intros; - unfold plusbytenc; - rewrite > plusbyte_O_x; - reflexivity. -qed. - -(*axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.*) -axiom mod_plus: \forall a1,a2,b1,b2,m. - a1 \mod m = b1 \mod m \to - a2 \mod m = b2 \mod m \to - (a1 + a2) \mod m = (b1 + b2) \mod m. - -axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O. - -axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256. - -theorem plusbytenc_ok: - ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256. - intros; - unfold plusbytenc; - generalize in match (plusbyte_ok b1 b2 false); - elim (plusbyte b1 b2 false); - simplify in H ⊢ %; - change with (nat_of_byte t = (b1 + b2) \mod 256); - rewrite < plus_n_O in H; - rewrite > H; clear H; - letin K ≝ (eq_nat_of_byte_mod t); clearbody K; - rewrite > K in ⊢ (? ? % ?); - letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K'; - [ autobatch - | cut (O = O \mod 256); - [ rewrite > Hcut in K':(? ? ? %); - rewrite > K in K:(? ? % ?); - rewrite > (mod_plus ? ? ? ? ? K K') in ⊢ (? ? ? %); - rewrite < plus_n_O;reflexivity - |simplify;reflexivity]] -qed. - -lemma test_O_O: - let i ≝ 14 in - let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in - pc s = 20 ∧ mem s 32 = byte_of_nat 0. - normalize; - split; - reflexivity. -qed. - - -lemma test_0_2: - let x ≝ mk_byte x0 x0 in - let y ≝ mk_byte x0 x2 in - let i ≝ 14 + 23 * nat_of_byte y in - let s ≝ execute (mult_status x y) i in - pc s = 20 ∧ mem s 32 = plusbytenc x x. - intros; - split; - reflexivity. -qed. - -lemma test_x_1: - ∀x. - let y ≝ mk_byte x0 x1 in - let i ≝ 14 + 23 * nat_of_byte y in - let s ≝ execute (mult_status x y) i in - pc s = 20 ∧ mem s 32 = x. - intros; - split; - [ reflexivity - | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x); - rewrite > plusbytenc_O_x; - reflexivity - ]. -qed. - -lemma test_x_2: - ∀x. - let y ≝ mk_byte x0 x2 in - let i ≝ 14 + 23 * nat_of_byte y in - let s ≝ execute (mult_status x y) i in - pc s = 20 ∧ mem s 32 = plusbytenc x x. - intros; - split; - [ reflexivity - | change in ⊢ (? ? % ?) with - (plusbytenc (plusbytenc (mk_byte x0 x0) x) x); - rewrite > plusbytenc_O_x; - reflexivity - ]. -qed. - -theorem lt_trans: ∀x,y,z. x < y → y < z → x < z. - unfold lt; - intros; - autobatch. -qed. - -axiom status_eq: - ∀s,s'. - acc s = acc s' → - pc s = pc s' → - spc s = spc s' → - zf s = zf s' → - cf s = cf s' → - (∀a. mem s a = mem s' a) → - clk s = clk s' → - s=s'. - lemma eq_eqex_S_x0_false: ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false. intro; @@ -1429,316 +924,3 @@ lemma eq_eqex_S_x0_false: assumption ] qed. - -lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z. - intros; - unfold div; - apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m))); - cut (∃w.m = S w); - [ elim Hcut; - rewrite > H2; - rewrite > H2 in H1; - clear Hcut; clear H2; clear H; (*clear m;*) - simplify; - unfold in ⊢ (? ? % ?); - cut (∃z.n = S z); - [ elim Hcut; clear Hcut; - rewrite > H in H1; - rewrite > H; clear m; - change in ⊢ (? ? % ?) with - (match leb (S a1) a with - [ true ⇒ O - | false ⇒ S (div_aux a1 ((S a1) - S a) a)]); - cut (S a1 ≰ a); - [ apply (leb_elim (S a1) a); - [ intro; - elim (Hcut H2) - | intro; - simplify; - reflexivity - ] - | intro; - autobatch - ] - | elim H1; autobatch - ] - | autobatch - ]. -qed. - -lemma eq_eqbyte_x0_x0_byte_of_nat_S_false: - ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false. - intros; - unfold byte_of_nat; - cut (b < 15 ∨ b ≥ 15); - [ elim Hcut; - [ unfold eqbyte; - change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); - rewrite > eq_eqex_S_x0_false; - [ elim (eqex (bh (mk_byte x0 x0)) -(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify; -(* - alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con". - rewrite > andb_sym; -*) - reflexivity - | assumption - ] - | unfold eqbyte; - change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16))); - letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?); - [ autobatch - | unfold in H1; - apply le_S_S; - assumption - | clearbody K; - elim K; clear K; - rewrite > H2; - rewrite > eq_eqex_S_x0_false; - [ reflexivity - | unfold lt; - unfold lt in H; - rewrite < H2; - clear H2; clear a; clear H1; clear Hcut; - elim daemon (* trivial arithmetic property over <= and div *) - ] - ] - ] - | elim daemon - ]. -qed. - -lemma eq_bpred_S_a_a: - ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a. -elim daemon. (* - intros; - unfold byte_of_nat; - cut (a \mod 16 = 15 ∨ a \mod 16 < 15); - [ elim Hcut; - [ - | - ] - | autobatch - ].*) -qed. - -lemma plusbyteenc_S: - ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n). - intros; - rewrite < byte_of_nat_nat_of_byte; - rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x); - rewrite > na - -(*CSC*) - intros; - unfold byte_of_nat; - unfold plusbytenc; - unfold plusbyte; - - elim daemon. -qed. - -lemma eq_plusbytec_x0_x0_x_false: - ∀x.plusbytec (mk_byte x0 x0) x = false. - intro; - elim x; - elim e; - elim e1; - reflexivity. -qed. - -lemma loop_invariant': - ∀x,y:byte.∀j:nat. j ≤ y → - execute (mult_status x y) (5 + 23*j) - = - mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j))) - (plusbytec (byte_of_nat (x*pred j)) x) - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32 - (byte_of_nat (x * j))) - 0. - intros 3; - elim j; - [ do 2 (rewrite < times_n_O); - apply status_eq; - [1,2,3,4,7: normalize; reflexivity - | rewrite > eq_plusbytec_x0_x0_x_false; - normalize; - reflexivity - | intro; - elim daemon - ] - | cut (5 + 23 * S n = 5 + 23 * n + 23); - [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K; - letin H' ≝ (H ?); clearbody H'; clear H; - [ autobatch - | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx; - clear Hcut; - rewrite > xxx; - clear xxx; - apply (transitive_eq ? ? ? ? K); - clear K; - rewrite > H'; - clear H'; - cut (∃z.y-n=S z ∧ z < 255); - [ elim Hcut; clear Hcut; - elim H; clear H; - rewrite > H2; - (* instruction LDAd *) - letin K ≝ - (breakpoint - (mk_status (byte_of_nat (x*n)) 4 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) - (plusbytec (byte_of_nat (x*pred n)) x) - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 - (byte_of_nat (x*n))) O) - 3 20); clearbody K; - normalize in K:(? ? (? ? %) ?); - apply transitive_eq; [2: apply K | skip | ]; clear K; - whd in ⊢ (? ? (? % ?) ?); - normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); - change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) - with (byte_of_nat (S a)); - change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with - (byte_of_nat (S a)); - (* instruction BEQ *) - letin K ≝ - (breakpoint - (mk_status (byte_of_nat (S a)) 6 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) - (plusbytec (byte_of_nat (x*pred n)) x) - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 - (byte_of_nat (x*n))) O) - 3 17); clearbody K; - normalize in K:(? ? (? ? %) ?); - apply transitive_eq; [2: apply K | skip | ]; clear K; - whd in ⊢ (? ? (? % ?) ?); - letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K; - rewrite > K; clear K; - simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); - (* instruction LDAd *) - letin K ≝ - (breakpoint - (mk_status (byte_of_nat (S a)) 8 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) - (plusbytec (byte_of_nat (x*pred n)) x) - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 - (byte_of_nat (x*n))) O) - 3 14); clearbody K; - normalize in K:(? ? (? ? %) ?); - apply transitive_eq; [2: apply K | skip | ]; clear K; - whd in ⊢ (? ? (? % ?) ?); - change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n)); - normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); - change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))); - (* instruction DECd *) - letin K ≝ - (breakpoint - (mk_status (byte_of_nat (x*n)) 10 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) - (plusbytec (byte_of_nat (x*pred n)) x) - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 - (byte_of_nat (x*n))) O) - 5 9); clearbody K; - normalize in K:(? ? (? ? %) ?); - apply transitive_eq; [2: apply K | skip | ]; clear K; - whd in ⊢ (? ? (? % ?) ?); - change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a))); - rewrite > (eq_bpred_S_a_a ? H3); - normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); - normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?); - cut (y - S n = a); - [2: elim daemon | ]; - rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a; - (* instruction ADDd *) - letin K ≝ - (breakpoint - (mk_status (byte_of_nat (x*n)) 12 - O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n))) - (plusbytec (byte_of_nat (x*pred n)) x) - (update - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n)))) - 32 (byte_of_nat (x*n))) 31 - (byte_of_nat (y-S n))) O) - 3 6); clearbody K; - normalize in K:(? ? (? ? %) ?); - apply transitive_eq; [2: apply K | skip | ]; clear K; - whd in ⊢ (? ? (? % ?) ?); - change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with - (plusbytenc (byte_of_nat (x*n)) x); - change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with - (plusbytenc (byte_of_nat (x*n)) x); - normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); - change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?) - with (plusbytec (byte_of_nat (x*n)) x); - rewrite > plusbyteenc_S; - (* instruction STAd *) - letin K ≝ - (breakpoint - (mk_status (byte_of_nat (x*S n)) 14 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n))) - (plusbytec (byte_of_nat (x*n)) x) - (update - (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n)))) - 32 (byte_of_nat (x*n))) 31 - (byte_of_nat (y-S n))) O) - 3 3); clearbody K; - normalize in K:(? ? (? ? %) ?); - apply transitive_eq; [2: apply K | skip | ]; clear K; - whd in ⊢ (? ? (? % ?) ?); - normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); - (* instruction BRA *) - whd in ⊢ (? ? % ?); - normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?); - rewrite < pred_Sn; - apply status_eq; - [1,2,3,4,7: normalize; reflexivity - | change with (plusbytec (byte_of_nat (x*n)) x = - plusbytec (byte_of_nat (x*n)) x); - reflexivity - |6: intro; - elim daemon - ] - | exists; - [ apply (y - S n) - | split; - [ rewrite < (minus_S_S y n); - autobatch - | letin K ≝ (lt_nat_of_byte_256 y); clearbody K; - letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K'; - autobatch - ] - ] - ] - ] - | rewrite > associative_plus; - autobatch paramodulation - ] - ] -qed. - -theorem test_x_y: - ∀x,y:byte. - let i ≝ 14 + 23 * y in - execute (mult_status x y) i = - mk_status (byte_of_nat (x*y)) 20 0 - (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y))) - (plusbytec (byte_of_nat (x*pred y)) x) - (update - (update (mult_memory x y) 31 (mk_byte x0 x0)) - 32 (byte_of_nat (x*y))) - 0. - intros; - cut (14 + 23 * y = 5 + 23*y + 9); - [2: autobatch paramodulation; - | rewrite > Hcut; (* clear Hcut; *) - rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9); - rewrite > loop_invariant'; - [2: apply le_n - | rewrite < minus_n_n; - apply status_eq; - [1,2,3,4,5,7: normalize; reflexivity - | elim daemon - ] - ] - ]. -qed. diff --git a/helm/software/matita/library/assembly/extra.ma b/helm/software/matita/library/assembly/extra.ma new file mode 100644 index 000000000..70b43bb1e --- /dev/null +++ b/helm/software/matita/library/assembly/extra.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/assembly/extra". + +include "nat/div_and_mod.ma". +include "nat/primes.ma". +include "list/list.ma". + +axiom mod_plus: ∀a,b,m. (a + b) \mod m = (a \mod m + b \mod m) \mod m. +axiom mod_mod: ∀a,n,m. n∣m → a \mod n = a \mod n \mod m. +axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O. +axiom eq_mod_to_eq_plus_mod: ∀a,b,c,m. a \mod m = b \mod m → (a+c) \mod m = (b+c) \mod m. +axiom eq_mod_times_times_mod: ∀a,b,n,m. m = a*n → (a*b) \mod m = a * (b \mod n). + +inductive cartesian_product (A,B: Type) : Type ≝ + couple: ∀a:A.∀b:B. cartesian_product A B. + +lemma le_to_lt: ∀n,m. n ≤ m → n < S m. + intros; + autobatch. +qed. + +alias num (instance 0) = "natural number". +definition nat_of_bool ≝ + λb. match b with [ true ⇒ 1 | false ⇒ 0 ]. + +theorem lt_trans: ∀x,y,z. x < y → y < z → x < z. + unfold lt; + intros; + autobatch. +qed. + +lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z. + intros; + unfold div; + apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m))); + cut (∃w.m = S w); + [ elim Hcut; + rewrite > H2; + rewrite > H2 in H1; + clear Hcut; clear H2; clear H; (*clear m;*) + simplify; + unfold in ⊢ (? ? % ?); + cut (∃z.n = S z); + [ elim Hcut; clear Hcut; + rewrite > H in H1; + rewrite > H; clear m; + change in ⊢ (? ? % ?) with + (match leb (S a1) a with + [ true ⇒ O + | false ⇒ S (div_aux a1 ((S a1) - S a) a)]); + cut (S a1 ≰ a); + [ apply (leb_elim (S a1) a); + [ intro; + elim (Hcut H2) + | intro; + simplify; + reflexivity + ] + | intro; + autobatch + ] + | elim H1; autobatch + ] + | autobatch + ]. +qed. + +axiom daemon: False. diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma new file mode 100644 index 000000000..98eb48d91 --- /dev/null +++ b/helm/software/matita/library/assembly/test.ma @@ -0,0 +1,297 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/assembly/test/". + +include "vm.ma". + +notation "hvbox(# break a)" + non associative with precedence 80 +for @{ 'byte_of_opcode $a }. +interpretation "byte_of_opcode" 'byte_of_opcode a = + (cic:/matita/assembly/vm/byte_of_opcode.con a). + +definition mult_source : list byte ≝ + [#LDAi; mk_byte x0 x0; (* A := 0 *) + #STAd; mk_byte x2 x0; (* Z := A *) + #LDAd; mk_byte x1 xF; (* (l1) A := Y *) + #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *) + #LDAd; mk_byte x2 x0; (* A := Z *) + #DECd; mk_byte x1 xF; (* Y := Y - 1 *) + #ADDd; mk_byte x1 xE; (* A += X *) + #STAd; mk_byte x2 x0; (* Z := A *) + #BRA; mk_byte xF x2; (* goto l1 *) + #LDAd; mk_byte x2 x0].(* (l2) *) + +definition mult_memory ≝ + λx,y.λa:addr. + match leb a 29 with + [ true ⇒ nth ? mult_source (mk_byte x0 x0) a + | false ⇒ + match eqb a 30 with + [ true ⇒ x + | false ⇒ y + ] + ]. + +definition mult_status ≝ + λx,y. + mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0. + +lemma test_O_O: + let i ≝ 14 in + let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in + pc s = 20 ∧ mem s 32 = byte_of_nat 0. + normalize; + split; + reflexivity. +qed. + +lemma test_0_2: + let x ≝ mk_byte x0 x0 in + let y ≝ mk_byte x0 x2 in + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 20 ∧ mem s 32 = plusbytenc x x. + intros; + split; + reflexivity. +qed. + +lemma test_x_1: + ∀x. + let y ≝ mk_byte x0 x1 in + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 20 ∧ mem s 32 = x. + intros; + split; + [ reflexivity + | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x); + rewrite > plusbytenc_O_x; + reflexivity + ]. +qed. + +lemma test_x_2: + ∀x. + let y ≝ mk_byte x0 x2 in + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 20 ∧ mem s 32 = plusbytenc x x. + intros; + split; + [ reflexivity + | change in ⊢ (? ? % ?) with + (plusbytenc (plusbytenc (mk_byte x0 x0) x) x); + rewrite > plusbytenc_O_x; + reflexivity + ]. +qed. + +lemma loop_invariant': + ∀x,y:byte.∀j:nat. j ≤ y → + execute (mult_status x y) (5 + 23*j) + = + mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j))) + (plusbytec (byte_of_nat (x*pred j)) x) + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32 + (byte_of_nat (x * j))) + 0. + intros 3; + elim j; + [ do 2 (rewrite < times_n_O); + apply status_eq; + [1,2,3,4,7: normalize; reflexivity + | rewrite > eq_plusbytec_x0_x0_x_false; + normalize; + reflexivity + | intro; + elim daemon + ] + | cut (5 + 23 * S n = 5 + 23 * n + 23); + [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K; + letin H' ≝ (H ?); clearbody H'; clear H; + [ autobatch + | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx; + clear Hcut; + rewrite > xxx; + clear xxx; + apply (transitive_eq ? ? ? ? K); + clear K; + rewrite > H'; + clear H'; + cut (∃z.y-n=S z ∧ z < 255); + [ elim Hcut; clear Hcut; + elim H; clear H; + rewrite > H2; + (* instruction LDAd *) + letin K ≝ + (breakpoint + (mk_status (byte_of_nat (x*n)) 4 O + (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) + (plusbytec (byte_of_nat (x*pred n)) x) + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 + (byte_of_nat (x*n))) O) + 3 20); clearbody K; + normalize in K:(? ? (? ? %) ?); + apply transitive_eq; [2: apply K | skip | ]; clear K; + whd in ⊢ (? ? (? % ?) ?); + normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); + change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) + with (byte_of_nat (S a)); + change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with + (byte_of_nat (S a)); + (* instruction BEQ *) + letin K ≝ + (breakpoint + (mk_status (byte_of_nat (S a)) 6 O + (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) + (plusbytec (byte_of_nat (x*pred n)) x) + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 + (byte_of_nat (x*n))) O) + 3 17); clearbody K; + normalize in K:(? ? (? ? %) ?); + apply transitive_eq; [2: apply K | skip | ]; clear K; + whd in ⊢ (? ? (? % ?) ?); + letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K; + rewrite > K; clear K; + simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); + (* instruction LDAd *) + letin K ≝ + (breakpoint + (mk_status (byte_of_nat (S a)) 8 O + (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) + (plusbytec (byte_of_nat (x*pred n)) x) + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 + (byte_of_nat (x*n))) O) + 3 14); clearbody K; + normalize in K:(? ? (? ? %) ?); + apply transitive_eq; [2: apply K | skip | ]; clear K; + whd in ⊢ (? ? (? % ?) ?); + change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n)); + normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); + change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))); + (* instruction DECd *) + letin K ≝ + (breakpoint + (mk_status (byte_of_nat (x*n)) 10 O + (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) + (plusbytec (byte_of_nat (x*pred n)) x) + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32 + (byte_of_nat (x*n))) O) + 5 9); clearbody K; + normalize in K:(? ? (? ? %) ?); + apply transitive_eq; [2: apply K | skip | ]; clear K; + whd in ⊢ (? ? (? % ?) ?); + change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a))); + rewrite > (eq_bpred_S_a_a ? H3); + normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); + normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?); + cut (y - S n = a); + [2: elim daemon | ]; + rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a; + (* instruction ADDd *) + letin K ≝ + (breakpoint + (mk_status (byte_of_nat (x*n)) 12 + O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n))) + (plusbytec (byte_of_nat (x*pred n)) x) + (update + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n)))) + 32 (byte_of_nat (x*n))) 31 + (byte_of_nat (y-S n))) O) + 3 6); clearbody K; + normalize in K:(? ? (? ? %) ?); + apply transitive_eq; [2: apply K | skip | ]; clear K; + whd in ⊢ (? ? (? % ?) ?); + change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with + (plusbytenc (byte_of_nat (x*n)) x); + change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with + (plusbytenc (byte_of_nat (x*n)) x); + normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); + change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?) + with (plusbytec (byte_of_nat (x*n)) x); + rewrite > plusbytenc_S; + (* instruction STAd *) + letin K ≝ + (breakpoint + (mk_status (byte_of_nat (x*S n)) 14 O + (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n))) + (plusbytec (byte_of_nat (x*n)) x) + (update + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n)))) + 32 (byte_of_nat (x*n))) 31 + (byte_of_nat (y-S n))) O) + 3 3); clearbody K; + normalize in K:(? ? (? ? %) ?); + apply transitive_eq; [2: apply K | skip | ]; clear K; + whd in ⊢ (? ? (? % ?) ?); + normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?); + (* instruction BRA *) + whd in ⊢ (? ? % ?); + normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?); + rewrite < pred_Sn; + apply status_eq; + [1,2,3,4,7: normalize; reflexivity + | change with (plusbytec (byte_of_nat (x*n)) x = + plusbytec (byte_of_nat (x*n)) x); + reflexivity + |6: intro; + elim daemon + ] + | exists; + [ apply (y - S n) + | split; + [ rewrite < (minus_S_S y n); + autobatch + | letin K ≝ (lt_nat_of_byte_256 y); clearbody K; + letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K'; + autobatch + ] + ] + ] + ] + | rewrite > associative_plus; + autobatch paramodulation + ] + ] +qed. + +theorem test_x_y: + ∀x,y:byte. + let i ≝ 14 + 23 * y in + execute (mult_status x y) i = + mk_status (byte_of_nat (x*y)) 20 0 + (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y))) + (plusbytec (byte_of_nat (x*pred y)) x) + (update + (update (mult_memory x y) 31 (mk_byte x0 x0)) + 32 (byte_of_nat (x*y))) + 0. + intros; + cut (14 + 23 * y = 5 + 23*y + 9); + [2: autobatch paramodulation; + | rewrite > Hcut; (* clear Hcut; *) + rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9); + rewrite > loop_invariant'; + [2: apply le_n + | rewrite < minus_n_n; + apply status_eq; + [1,2,3,4,5,7: normalize; reflexivity + | elim daemon + ] + ] + ]. +qed. diff --git a/helm/software/matita/library/assembly/vm.ma b/helm/software/matita/library/assembly/vm.ma new file mode 100644 index 000000000..dac755c82 --- /dev/null +++ b/helm/software/matita/library/assembly/vm.ma @@ -0,0 +1,225 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/assembly/vm/". + +include "byte.ma". + +definition addr ≝ nat. + +definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b. + +coercion cic:/matita/assembly/vm/addr_of_byte.con. + +inductive opcode: Type ≝ + ADDd: opcode (* 3 clock, 171 *) + | BEQ: opcode (* 3, 55 *) + | BRA: opcode (* 3, 48 *) + | DECd: opcode (* 5, 58 *) + | LDAi: opcode (* 2, 166 *) + | LDAd: opcode (* 3, 182 *) + | STAd: opcode. (* 3, 183 *) + +let rec cycles_of_opcode op : nat ≝ + match op with + [ ADDd ⇒ 3 + | BEQ ⇒ 3 + | BRA ⇒ 3 + | DECd ⇒ 5 + | LDAi ⇒ 2 + | LDAd ⇒ 3 + | STAd ⇒ 3 + ]. + +definition opcodemap ≝ + [ couple ? ? ADDd (mk_byte xA xB); + couple ? ? BEQ (mk_byte x3 x7); + couple ? ? BRA (mk_byte x3 x0); + couple ? ? DECd (mk_byte x3 xA); + couple ? ? LDAi (mk_byte xA x6); + couple ? ? LDAd (mk_byte xB x6); + couple ? ? STAd (mk_byte xB x7) ]. + +definition opcode_of_byte ≝ + λb. + let rec aux l ≝ + match l with + [ nil ⇒ ADDd + | cons c tl ⇒ + match c with + [ couple op n ⇒ + match eqbyte n b with + [ true ⇒ op + | false ⇒ aux tl + ]]] + in + aux opcodemap. + +definition magic_of_opcode ≝ + λop1. + match op1 with + [ ADDd ⇒ 0 + | BEQ ⇒ 1 + | BRA ⇒ 2 + | DECd ⇒ 3 + | LDAi ⇒ 4 + | LDAd ⇒ 5 + | STAd ⇒ 6 ]. + +definition opcodeeqb ≝ + λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2). + +definition byte_of_opcode : opcode → byte ≝ + λop. + let rec aux l ≝ + match l with + [ nil ⇒ mk_byte x0 x0 + | cons c tl ⇒ + match c with + [ couple op' n ⇒ + match opcodeeqb op op' with + [ true ⇒ n + | false ⇒ aux tl + ]]] + in + aux opcodemap. + +record status : Type ≝ { + acc : byte; + pc : addr; + spc : addr; + zf : bool; + cf : bool; + mem : addr → byte; + clk : nat +}. + +definition update ≝ + λf: addr → byte.λa.λv.λx. + match eqb x a with + [ true ⇒ v + | false ⇒ f x ]. + +lemma update_update_a_a: + ∀s,a,v1,v2,b. + update (update s a v1) a v2 b = update s a v2 b. + intros; + unfold update; + unfold update; + elim (eqb b a); + reflexivity. +qed. + +lemma update_update_a_b: + ∀s,a1,v1,a2,v2,b. + a1 ≠ a2 → + update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b. + intros; + unfold update; + unfold update; + apply (bool_elim ? (eqb b a1)); intros; + apply (bool_elim ? (eqb b a2)); intros; + simplify; + [ elim H; + rewrite < (eqb_true_to_eq ? ? H1); + apply eqb_true_to_eq; + assumption + |*: reflexivity + ]. +qed. + +definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n). + +definition tick ≝ + λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒ + let opc ≝ opcode_of_byte (mem pc) in + let op1 ≝ mem (S pc) in + let clk' ≝ cycles_of_opcode opc in + match eqb (S clk) clk' with + [ true ⇒ + match opc with + [ ADDd ⇒ + let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *) + let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in + let c' ≝ match res with [ couple _ c' ⇒ c'] in + mk_status acc' (2 + pc) spc + (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *) + | BEQ ⇒ + mk_status + acc + (match zf with + [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *) + (* FIXME: can't work - address truncated to 8 bits *) + | false ⇒ 2 + pc + ]) + spc + zf + cf + mem + 0 + | BRA ⇒ + mk_status + acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *) + (* FIXME: same as above *) + spc + zf + cf + mem + 0 + | DECd ⇒ + let x ≝ bpred (mem op1) in (* signed!!! *) + let mem' ≝ update mem op1 x in + mk_status acc (2 + pc) spc + (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *) + | LDAi ⇒ + mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0 + | LDAd ⇒ + let x ≝ mem op1 in + mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0 + | STAd ⇒ + mk_status acc (2 + pc) spc zf cf + (update mem op1 acc) 0 + ] + | false ⇒ + mk_status + acc pc spc zf cf mem (S clk) + ]]. + +let rec execute s n on n ≝ + match n with + [ O ⇒ s + | S n' ⇒ execute (tick s) n' + ]. + +lemma breakpoint: + ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2. + intros; + generalize in match s; clear s; + elim n1; + [ reflexivity + | simplify; + apply H; + ] +qed. + +axiom status_eq: + ∀s,s'. + acc s = acc s' → + pc s = pc s' → + spc s = spc s' → + zf s = zf s' → + cf s = cf s' → + (∀a. mem s a = mem s' a) → + clk s = clk s' → + s=s'. -- 2.39.2