matita/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/status/HC05_status_lemmas.ma".
  24 include "emulator/status/HC08_status_lemmas.ma".
  25 include "emulator/status/RS08_status_lemmas.ma".
  26 include "emulator/status/IP2022_status_lemmas.ma".
  27 include "emulator/status/status.ma".
  28 include "common/option_lemmas.ma".
  29 include "common/prod_lemmas.ma".
  30 include "emulator/opcodes/pseudo_lemmas.ma".
  31
  32 (* *********************************** *)
  33 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  34 (* *********************************** *)
  35
  36 nlemma symmetric_eqclk : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = eq_clk m clk2 clk1.
  37  #m;
  38  napply (symmetric_eqoption ? (eq_quintuple …) (symmetric_eqquintuple …));
  39  ##[ ##1: napply symmetric_eqw16
  40  ##| ##2: napply symmetric_eqb8
  41  ##| ##3: napply (symmetric_eqim m)
  42  ##| ##4: napply (symmetric_eqpseudo m)
  43  ##| ##5: napply symmetric_eqb8
  44  ##]
  45 nqed.
  46
  47 nlemma eqclk_to_eq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = true → clk1 = clk2.
  48  #m;
  49  napply (eqoption_to_eq ? (eq_quintuple …) (eqquintuple_to_eq …));
  50  ##[ ##1: napply eqw16_to_eq
  51  ##| ##2: napply eqb8_to_eq
  52  ##| ##3: napply (eqim_to_eq m)
  53  ##| ##4: napply (eqpseudo_to_eq m)
  54  ##| ##5: napply eqb8_to_eq
  55  ##]
  56 nqed.
  57
  58 nlemma eq_to_eqclk : ∀m.∀clk1,clk2.(clk1 = clk2) → (eq_clk m clk1 clk2 = true).
  59  #m;
  60  napply (eq_to_eqoption ? (eq_quintuple …) (eq_to_eqquintuple …));
  61  ##[ ##1: napply eq_to_eqw16
  62  ##| ##2: napply eq_to_eqb8
  63  ##| ##3: napply (eq_to_eqim m)
  64  ##| ##4: napply (eq_to_eqpseudo m)
  65  ##| ##5: napply eq_to_eqb8
  66  ##]
  67 nqed.
  68
  69 nlemma neqclk_to_neq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = false → clk1 ≠ clk2.
  70  #m;
  71  napply (neqoption_to_neq ? (eq_quintuple …) (neqquintuple_to_neq …));
  72  ##[ ##1: napply neqw16_to_neq
  73  ##| ##2: napply neqb8_to_neq
  74  ##| ##3: napply (neqim_to_neq m)
  75  ##| ##4: napply (neqpseudo_to_neq m)
  76  ##| ##5: napply neqb8_to_neq
  77  ##]
  78 nqed.
  79
  80 nlemma neq_to_neqclk : ∀m.∀clk1,clk2.(clk1 ≠ clk2) → (eq_clk m clk1 clk2 = false).
  81  #m;
  82  napply (neq_to_neqoption ? (eq_quintuple …) (neq_to_neqquintuple …));
  83  ##[ ##1: napply neq_to_neqw16
  84  ##| ##2: napply neq_to_neqb8
  85  ##| ##3: napply (neq_to_neqim m)
  86  ##| ##4: napply (neq_to_neqpseudo m)
  87  ##| ##5: napply neq_to_neqb8
  88  ##| ##6: napply decidable_w16
  89  ##| ##7: napply decidable_b8
  90  ##| ##8: napply (decidable_im m)
  91  ##| ##9: napply (decidable_pseudo m)
  92  ##| ##10: napply decidable_b8
  93  ##]
  94 nqed.
  95
  96 nlemma decidable_clk : ∀m.∀clk1,clk2:option (aux_clk_type m).decidable (clk1 = clk2).
  97  #m;
  98  napply (decidable_option ? (decidable_quintuple …));
  99  ##[ ##1: napply decidable_w16
 100  ##| ##2: napply decidable_b8
 101  ##| ##3: napply (decidable_im m)
 102  ##| ##4: napply (decidable_pseudo m)
 103  ##| ##5: napply decidable_b8
 104  ##]
 105 nqed.
 106
 107 nlemma symmetric_forallmemoryranged :
 108 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
 109  forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
 110  forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
 111  #t; #chk1; #chk2; #mem1; #mem2; #addrl;
 112  nelim addrl;
 113  ##[ ##1: nnormalize; napply refl_eq
 114  ##| ##2: #a; #l; #H;
 115           nchange with (
 116            ((eq_option byte8 eq_b8 (mem_read t mem1 chk1 a)
 117                                    (mem_read t mem2 chk2 a)) ⊗
 118            (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
 119            ((eq_option byte8 eq_b8 (mem_read t mem2 chk2 a)
 120                                    (mem_read t mem1 chk1 a)) ⊗
 121            (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
 122            nrewrite > H;
 123            nrewrite > (symmetric_eqoption ? eq_b8 symmetric_eqb8 (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a));
 124            napply refl_eq
 125  ##]
 126 nqed.
 127
 128 nlemma anystatus_destruct_1 :
 129 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 130  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 131  x1 = y1.
 132  #m; #t;
 133  #x1; #x2; #x3; #x4;
 134  #y1; #y2; #y3; #y4; #H;
 135  nchange with (match mk_any_status m t y1 y2 y3 y4
 136                 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
 137  nrewrite < H;
 138  nnormalize;
 139  napply refl_eq.
 140 nqed.
 141
 142 nlemma anystatus_destruct_2 :
 143 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 144  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 145  x2 = y2.
 146  #m; #t;
 147  #x1; #x2; #x3; #x4;
 148  #y1; #y2; #y3; #y4; #H;
 149  nchange with (match mk_any_status m t y1 y2 y3 y4
 150                 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
 151  nrewrite < H;
 152  nnormalize;
 153  napply refl_eq.
 154 nqed.
 155
 156 nlemma anystatus_destruct_3 :
 157 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 158  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 159  x3 = y3.
 160  #m; #t;
 161  #x1; #x2; #x3; #x4;
 162  #y1; #y2; #y3; #y4; #H;
 163  nchange with (match mk_any_status m t y1 y2 y3 y4
 164                 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
 165  nrewrite < H;
 166  nnormalize;
 167  napply refl_eq.
 168 nqed.
 169
 170 nlemma anystatus_destruct_4 :
 171 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 172  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 173  x4 = y4.
 174  #m; #t;
 175  #x1; #x2; #x3; #x4;
 176  #y1; #y2; #y3; #y4; #H;
 177  nchange with (match mk_any_status m t y1 y2 y3 y4
 178                 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
 179  nrewrite < H;
 180  nnormalize;
 181  napply refl_eq.
 182 nqed.
 183
 184 naxiom symmetric_eqanystatus :
 185 ∀addrl:list word32.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 186  eq_anystatus m t s1 s2 addrl = eq_anystatus m t s2 s1 addrl.
 187 (* !!! si blocca su symmetric_eqalu_HC05 *)
 188 (* #addrl; #m; ncases m; #t; #s1;
 189  ##[ ##1: nelim s1; #x1; #x2; #x3; #x4;
 190           #s2; nelim s2; #y1; #y2; #y3; #y4;
 191           nchange with (
 192            ((eq_HC05_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
 193            ((eq_HC05_alu y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
 194            nrewrite > (symmetric_eqaluHC05 x1 y1)
 195  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
 196           #s2; ncases s2; #y1; #y2; #y3; #y4;
 197           nchange with (
 198            ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
 199            ((eq_aluHC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
 200            nrewrite > (symmetric_eqaluHC08 x1 y1)
 201  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
 202           #s2; ncases s2; #y1; #y2; #y3; #y4;
 203           nchange with (
 204            ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
 205            ((eq_aluRS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
 206            nrewrite > (symmetric_eqaluRS08 x1 y1)
 207  ##| ##5: ...
 208  ##]
 209  nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
 210  nrewrite > (symmetric_eqclk ? x4 y4);
 211  napply refl_eq.
 212 nqed.*)
 213
 214 nlemma eqanystatus_to_eq :
 215 ∀addrl:list word32.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 216  (eq_anystatus m t s1 s2 addrl = true) →
 217   And3 (alu m t s1 = alu m t s2)
 218        (clk_desc m t s1 = clk_desc m t s2)
 219        ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
 220                                 (mem_desc m t s1) (mem_desc m t s2) addrl) = true).
 221  #addrl; #m; #t;
 222  ncases m; #s1;
 223  ncases s1; #x1; #x2; #x3; #x4;
 224           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 225  ##[ ##1: nchange in H:(%) with (
 226            ((eq_HC05_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 227            nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
 228  ##| ##2,3: nchange in H:(%) with (
 229             ((eq_HC08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 230             nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
 231  ##| ##4: nchange in H:(%) with (
 232            ((eq_RS08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 233           nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
 234  ##| ##5: nchange in H:(%) with (
 235            ((eq_IP2022_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 236           nrewrite > (eqaluIP2022_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
 237  ##]
 238  nchange with (And3 (y1 = y1) (x4 = y4) (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
 239  nrewrite > (andb_true_true_r … (andb_true_true_l … H));
 240  nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
 241  napply (conj3 … (refl_eq ? y1) (refl_eq ? y4) (refl_eq ? true)).
 242 nqed.
 243
 244 naxiom eq_to_eqanystatus :
 245 ∀addrl:list word32.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 246  (alu m t s1 = alu m t s2) →
 247  (clk_desc m t s1 = clk_desc m t s2) →
 248  ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
 249                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
 250  (eq_anystatus m t s1 s2 addrl = true).
 251 (* !!! si blocca su symmetric_eqalu_HC05 *)
 252 (* #addrl; #m; #t;
 253  ncases m; #s1; ncases s1; #x1; #x2; #x3; #x4;
 254  #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
 255  ##[ ##1: nchange with (((eq_HC05_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 256           nchange in H:(%) with (x1 = y1);
 257           nrewrite > H;
 258           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
 259  ##| ##2,3: nchange with (((eq_HC08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 260             nchange in H:(%) with (x1 = y1);
 261             nrewrite > H;
 262             nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
 263  ##| ##4: nchange with (((eq_RS08_alu x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 264           nchange in H:(%) with (x1 = y1);
 265           nrewrite > H;
 266           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
 267  ##| ##5: ...
 268  ##]
 269  nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
 270  nrewrite > H2;
 271  nchange in H1:(%) with (x4 = y4);
 272  nrewrite > H1;
 273  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
 274  nnormalize;
 275  napply refl_eq.
 276 nqed.*)