(* 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〉〉)
+ ].
(* (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 ].
(* 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
]
- ]
- ].
+ ].
(* 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〉〉)
+ ].
(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
+*)
(* 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 ≝
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.
| 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 ⊗
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
projects / helm.git / commitdiff