From 9a3b49d3584873c77a39107cb5ee4f1e6010e43c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Jul 2007 10:00:30 +0000 Subject: [PATCH] fixed includes and added notation for bytes --- helm/software/matita/library/assembly/byte.ma | 8 ++- .../matita/library/assembly/exadecimal.ma | 4 +- helm/software/matita/library/assembly/test.ma | 70 +++++++++---------- helm/software/matita/library/assembly/vm.ma | 8 ++- 4 files changed, 47 insertions(+), 43 deletions(-) diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma index 4d050e0cd..8c7be0308 100644 --- a/helm/software/matita/library/assembly/byte.ma +++ b/helm/software/matita/library/assembly/byte.ma @@ -14,13 +14,17 @@ set "baseuri" "cic:/matita/assembly/byte". -include "exadecimal.ma". +include "assembly/exadecimal.ma". record byte : Type ≝ { bh: exadecimal; bl: exadecimal }. +notation "〈 x, y 〉" non associative with precedence 80 for @{ 'mk_byte $x $y }. +interpretation "mk_byte" 'mk_byte x y = + (cic:/matita/assembly/byte/byte.ind#xpointer(1/1/1) x y). + definition eqbyte ≝ λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b'). @@ -205,7 +209,7 @@ 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. + ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b))) = false. intros; unfold byte_of_nat; cut (b < 15 ∨ b ≥ 15); diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma index 7dfd42bb1..fb1a14ede 100644 --- a/helm/software/matita/library/assembly/exadecimal.ma +++ b/helm/software/matita/library/assembly/exadecimal.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/assembly/exadecimal/". -include "extra.ma". +include "assembly/extra.ma". inductive exadecimal : Type ≝ x0: exadecimal @@ -927,4 +927,4 @@ lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b. intros; rewrite > exadecimal_of_nat_mod; rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %); -*) \ No newline at end of file +*) diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma index 1fd030efb..a917e34ff 100644 --- a/helm/software/matita/library/assembly/test.ma +++ b/helm/software/matita/library/assembly/test.ma @@ -14,30 +14,24 @@ 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). +include "assembly/vm.ma". 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) *) + [#LDAi; 〈x0, x0〉; (* A := 0 *) + #STAd; 〈x2, x0〉; (* Z := A *) + #LDAd; 〈x1, xF〉; (* (l1) A := Y *) + #BEQ; 〈x0, xA〉; (* if A == 0 then goto l2 *) + #LDAd; 〈x2, x0〉; (* A := Z *) + #DECd; 〈x1, xF〉; (* Y := Y - 1 *) + #ADDd; 〈x1, xE〉; (* A += X *) + #STAd; 〈x2, x0〉; (* Z := A *) + #BRA; 〈xF, x2〉; (* goto l1 *) + #LDAd; 〈x2, x0〉].(* (l2) *) definition mult_memory ≝ λx,y.λa:addr. match leb a 29 with - [ true ⇒ nth ? mult_source (mk_byte x0 x0) a + [ true ⇒ nth ? mult_source 〈x0, x0〉 a | false ⇒ match eqb a 30 with [ true ⇒ x @@ -47,11 +41,11 @@ definition mult_memory ≝ definition mult_status ≝ λx,y. - mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0. + mk_status 〈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 + let s ≝ execute (mult_status 〈x0, x0〉 〈x0, x0〉) i in pc s = 20 ∧ mem s 32 = byte_of_nat 0. normalize; split; @@ -59,8 +53,8 @@ lemma test_O_O: qed. lemma test_0_2: - let x ≝ mk_byte x0 x0 in - let y ≝ mk_byte x0 x2 in + let x ≝ 〈x0, x0〉 in + let y ≝ 〈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. @@ -71,14 +65,14 @@ qed. lemma test_x_1: ∀x. - let y ≝ mk_byte x0 x1 in + let y ≝ 〈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); + | change in ⊢ (? ? % ?) with (plusbytenc 〈x0, x0〉 x); rewrite > plusbytenc_O_x; reflexivity ]. @@ -86,7 +80,7 @@ qed. lemma test_x_2: ∀x. - let y ≝ mk_byte x0 x2 in + let y ≝ 〈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. @@ -94,7 +88,7 @@ lemma test_x_2: split; [ reflexivity | change in ⊢ (? ? % ?) with - (plusbytenc (plusbytenc (mk_byte x0 x0) x) x); + (plusbytenc (plusbytenc 〈x0, x0〉 x) x); rewrite > plusbytenc_O_x; reflexivity ]. @@ -104,7 +98,7 @@ 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))) + mk_status (byte_of_nat (x * j)) 4 0 (eqbyte 〈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))) @@ -121,7 +115,7 @@ lemma loop_invariant': rewrite < minus_n_O; normalize in ⊢ (? ? (? (? ? %) ?) ?); whd in ⊢ (? ? % ?); - change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 (mk_byte x0 x0) a); + change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 〈x0, x0〉 a); change in ⊢ (? ? ? %) with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat y)) 32 (byte_of_nat 0) a); change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30); @@ -154,7 +148,7 @@ lemma loop_invariant': letin K ≝ (breakpoint (mk_status (byte_of_nat (x*n)) 4 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) + (eqbyte 〈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) @@ -171,7 +165,7 @@ lemma loop_invariant': letin K ≝ (breakpoint (mk_status (byte_of_nat (S a)) 6 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) + (eqbyte 〈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) @@ -186,7 +180,7 @@ lemma loop_invariant': letin K ≝ (breakpoint (mk_status (byte_of_nat (S a)) 8 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) + (eqbyte 〈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) @@ -196,12 +190,12 @@ lemma loop_invariant': 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))); + change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈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))) + (eqbyte 〈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) @@ -222,7 +216,7 @@ lemma loop_invariant': letin K ≝ (breakpoint (mk_status (byte_of_nat (x*n)) 12 - O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n))) + O (eqbyte 〈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)))) @@ -244,7 +238,7 @@ lemma loop_invariant': letin K ≝ (breakpoint (mk_status (byte_of_nat (x*S n)) 14 O - (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n))) + (eqbyte 〈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)))) @@ -316,10 +310,10 @@ theorem test_x_y: 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))) + (eqbyte 〈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)) + (update (mult_memory x y) 31 〈x0, x0〉) 32 (byte_of_nat (x*y))) 0. intros; @@ -335,7 +329,7 @@ theorem test_x_y: | intro; change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a = - update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32 + update (update (mult_memory x y) 31 〈x0, x0〉) 32 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a); apply inj_update; intro; apply inj_update; intro; diff --git a/helm/software/matita/library/assembly/vm.ma b/helm/software/matita/library/assembly/vm.ma index 239146a07..162b5df0f 100644 --- a/helm/software/matita/library/assembly/vm.ma +++ b/helm/software/matita/library/assembly/vm.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/assembly/vm/". -include "byte.ma". +include "assembly/byte.ma". definition addr ≝ nat. @@ -95,6 +95,12 @@ definition byte_of_opcode : opcode → byte ≝ in aux opcodemap. +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). + record status : Type ≝ { acc : byte; pc : addr; -- 2.39.2