From bf0cc84dcef9ae3d2145e79754bb39feb3985574 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Wed, 14 Oct 2009 20:52:07 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 .../ng_assembly/freescale/memory_bits.ma      | 16 ++---
 .../ng_assembly/freescale/memory_func.ma      | 24 +++-----
 .../ng_assembly/freescale/memory_trees.ma     | 18 +++---
 .../freescale_tests/micro_tests4.ma           | 61 +++++++++++++++----
 .../matita/contribs/ng_assembly/num/byte8.ma  | 27 +++++---
 .../contribs/ng_assembly/num/exadecim.ma      |  4 ++
 .../matita/contribs/ng_assembly/num/word16.ma | 25 +++++---
 .../matita/contribs/ng_assembly/num/word32.ma | 25 +++++---
 8 files changed, 126 insertions(+), 74 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
index 93dcfa53f..c49be931a 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
@@ -215,13 +215,9 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
 
 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 nlet rec mb_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))))
-                               (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
-  (* non supera 0xFFFF, ricorsione *)
-  [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
-  (* supera 0xFFFF, niente ricorsione *)
-  | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)
-  ]].
+                                (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
+  ].
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
index 723ec0b84..831c75a1a 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
@@ -31,8 +31,8 @@ include "common/list.ma".
 
 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
 ndefinition mf_check_update_ranged ≝
-λf:word16 → memory_type.λi.λs.λv.
- λx.match inrange_w16 x i s with
+λf:word16 → memory_type.λinf.λsup.λv.
+ λx.match inrange_w16 x inf sup with
   [ true ⇒ v
   | false ⇒ f x ].
 
@@ -73,19 +73,15 @@ ndefinition mf_mem_read ≝
 (* CARICAMENTO PROGRAMMA/DATI *)
 (* ************************** *)
 
-(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
-nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
-  (* e' prima di source: carica da old_mem *)
-  [ true ⇒ old_mem x
-  | false ⇒ match eq_w16 x addr with
+(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
+nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ λx:word16.match eq_w16 addr x with
    (* la locazione corrisponde al punto corrente di source *)
    [ true ⇒ hd
-   (* la locazione e' piu' avanti: ricorsione *)
+   (* la locazione e' piu' avanti? ricorsione *)
    | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)) x
    ]
-  ]
- ].
+  ].
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma
index b9d67c554..e1e338b81 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma
@@ -217,15 +217,11 @@ ndefinition mt_mem_read ≝
 (* CARICAMENTO PROGRAMMA/DATI *)
 (* ************************** *)
 
-(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
+(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
 nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8))))
-                               (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
-  (* non supera 0xFFFF, ricorsione *)
-  [ true ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
-  (* supera 0xFFFF, niente ricorsione *)
-  | false ⇒ mt_update ? old_mem addr hd
-  ]].
+                                (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
+  ].
diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma
index 7f182852b..c2f055c70 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma
@@ -101,17 +101,52 @@ nlemma ok_mTest_HCS08_CBEQ_DBNZ_full :
     (mk_word16 〈x1,x8〉 〈x8,xE〉))
    (mk_byte8 xF xF))
   [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true.
- #t; 
- napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t
-        (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat68
-         with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
-        (set_acc_8_low_reg HCS08 t (* nuovo A *)
-         (set_pc_reg HCS08 t (* nuovo PC *)
-          (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
-           (mk_word16 〈x0,x0〉 〈x7,x0〉))
-          (mk_word16 〈x1,x8〉 〈x8,xE〉))
-         (mk_byte8 xF xF)));
- nelim t;
- nnormalize in ⊢ (? ? ? %);
- napply refl_eq.
+ #t;
+
+ (* nelim t; napply refl_eq; *)
+ (* cosi' in 7sec fa tutto *)
+
+ napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t …);
+ ##[ ##3: (* ram *) 
+          nelim t;
+          nnormalize in ⊢ (? ? % ?);
+          napply refl_eq;
+          (* 10sec con normalize, leggermente di piu' senza *)
+ ##| ##2: (* descrittore *)
+          nelim t;
+          nnormalize in ⊢ (? ? ? %);
+          nnormalize in ⊢ (? ? % ?);
+          napply refl_eq;
+          (* 7sec con normalize, leggermente di piu' senza il secondo normalize,
+             non termina senza il primo *)
+ ##| ##1: (* alu *)
+          nelim t;
+          (* senza questo normalize non va nulla *)
+          ##[ ##2,3: nnormalize in ⊢ (? ? ? %);
+                     napply refl_eq;
+          ##| ##1: (* in questo punto si vede benissimo come stato1 = stato2 esplode
+                      mentre la trasformazione eq_stato s1 s2 = true computa benissimo *)
+                   (* un napply refl_eq diretto non ci riesce proprio... *)
+                   napply (eqaluHC08_to_eq
+                    (alu HCS08 MEM_FUNC (match execute HCS08 MEM_FUNC (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status MEM_FUNC 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat68 with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]))
+                    (alu HCS08 MEM_FUNC (set_acc_8_low_reg HCS08 MEM_FUNC (* nuovo A *)
+                     (set_pc_reg HCS08 MEM_FUNC (* nuovo PC *)
+                      (setweak_indX_16_reg HCS08 MEM_FUNC (mTest_HCS08_CBEQ_DBNZ_status MEM_FUNC 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
+                       (mk_word16 〈x0,x0〉 〈x7,x0〉)) (mk_word16 〈x1,x8〉 〈x8,xE〉)) (mk_byte8 xF xF)))
+                    ?);
+                   nnormalize in ⊢ (? ? % ?);
+                   napply refl_eq;
+          ##]
+ ##]
+(* pero' ora si e' inceppato nqed... *)
 nqed.
+
+(* IMPRESSIONI
+   sembra confermato ora che un confronto diretto "oggettoGrosso1 = oggettoGrosso2" fallisca
+   mentre "funzione_eq oggettoGrosso1 oggettoGrosso2 = const." riesce
+
+   lo si vede in "forall_memory_ranged mem1 mem2 [addr] = true"
+   lo si vede in "get_clk (...) = const." NB: senza il normalize dx. infatti fallisce...
+   lo si vede in "alu1 = alu2" che fallisce stranamente solo nel caso MEM_FUNC
+    riportare "alu1 = alu2" a "eq alu1 alu2 = true" col teorema lo aggira, ma non chiude nqed
+*)
diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index 698736af6..4d621bb29 100755
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -43,20 +43,27 @@ ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1
 
 (* operatore < *)
 ndefinition lt_b8 ≝
-λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
- [ true ⇒ true
- | false ⇒ match gt_ex (b8h b1) (b8h b2) with
-  [ true ⇒ false
-  | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
+λb1,b2:byte8.
+ (lt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (lt_ex (b8l b1) (b8l b2))).
 
 (* operatore ≤ *)
-ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2). 
+ndefinition le_b8 ≝
+λb1,b2:byte8.
+ (lt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (le_ex (b8l b1) (b8l b2))).
 
 (* operatore > *)
-ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
+ndefinition gt_b8 ≝
+λb1,b2:byte8.
+ (gt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (gt_ex (b8l b1) (b8l b2))).
 
 (* operatore ≥ *)
-ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
+ndefinition ge_b8 ≝
+λb1,b2:byte8.
+ (gt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (ge_ex (b8l b1) (b8l b2))).
 
 (* operatore and *)
 ndefinition and_b8 ≝
@@ -299,6 +306,10 @@ ndefinition daa_b8 ≝
    pair … X'' true
   ].
 
+(* operatore x in [inf,sup] *)
+ndefinition inrange_b8 ≝
+λx,inf,sup:byte8.(le_b8 inf x) ⊗ (le_b8 x sup).
+
 (* iteratore sui byte *)
 ndefinition forall_b8 ≝
  λP.
diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index 797ac1948..eb92c8f2d 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -1378,6 +1378,10 @@ ndefinition compl_ex ≝
  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
 
+(* operatore x in [inf,sup] *)
+ndefinition inrange_ex ≝
+λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup).
+
 (* iteratore sugli esadecimali *)
 ndefinition forall_ex ≝ λP.
  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 6c1b21865..51fb30644 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -42,20 +42,27 @@ ndefinition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1)
 
 (* operatore < *)
 ndefinition lt_w16 ≝
-λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with
- [ true ⇒ true
- | false ⇒ match gt_b8 (w16h w1) (w16h w2) with
-  [ true ⇒ false
-  | false ⇒ lt_b8 (w16l w1) (w16l w2) ]].
+λw1,w2:word16.
+ (lt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (lt_b8 (w16l w1) (w16l w2))).
 
 (* operatore ≤ *)
-ndefinition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2).
+ndefinition le_w16 ≝
+λw1,w2:word16.
+ (lt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (le_b8 (w16l w1) (w16l w2))).
 
 (* operatore > *)
-ndefinition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2).
+ndefinition gt_w16 ≝
+λw1,w2:word16.
+ (gt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (gt_b8 (w16l w1) (w16l w2))).
 
 (* operatore ≥ *)
-ndefinition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2).
+ndefinition ge_w16 ≝
+λw1,w2:word16.
+ (gt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (ge_b8 (w16l w1) (w16l w2))).
 
 (* operatore and *)
 ndefinition and_w16 ≝
@@ -228,7 +235,7 @@ ndefinition div_b8 ≝
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w16 ≝
-λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
+λx,inf,sup:word16.(le_w16 inf x) ⊗ (le_w16 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w16 ≝
diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index 51bbf1ced..a5a74faa8 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -42,20 +42,27 @@ ndefinition eq_w32 ≝ λdw1,dw2.(eq_w16 (w32h dw1) (w32h dw2)) ⊗ (eq_w16 (w32
 
 (* operatore < *)
 ndefinition lt_w32 ≝
-λdw1,dw2:word32.match lt_w16 (w32h dw1) (w32h dw2) with
- [ true ⇒ true
- | false ⇒ match gt_w16 (w32h dw1) (w32h dw2) with
-  [ true ⇒ false
-  | false ⇒ lt_w16 (w32l dw1) (w32l dw2) ]].
+λdw1,dw2:word32.
+ (lt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (lt_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore ≤ *)
-ndefinition le_w32 ≝ λdw1,dw2:word32.(eq_w32 dw1 dw2) ⊕ (lt_w32 dw1 dw2).
+ndefinition le_w32 ≝
+λdw1,dw2:word32.
+ (lt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (le_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore > *)
-ndefinition gt_w32 ≝ λdw1,dw2:word32.⊖ (le_w32 dw1 dw2).
+ndefinition gt_w32 ≝
+λdw1,dw2:word32.
+ (gt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (gt_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore ≥ *)
-ndefinition ge_w32 ≝ λdw1,dw2:word32.⊖ (lt_w32 dw1 dw2).
+ndefinition ge_w32 ≝
+λdw1,dw2:word32.
+ (gt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (ge_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore and *)
 ndefinition and_w32 ≝
@@ -228,7 +235,7 @@ ndefinition div_w16 ≝
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w32 ≝
-λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup).
+λx,inf,sup:word32.(le_w32 inf x) ⊗ (le_w32 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w32 ≝
-- 
2.39.2