matita/matita/contribs/ng_assembly2/emulator/status/status.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/status_base.ma".
  24
  25 (* *********************************** *)
  26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  27 (* *********************************** *)
  28
  29 nlemma symmetric_forallmemoryranged :
  30 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀sel.∀addrl.
  31  forall_memory_ranged t chk1 chk2 mem1 mem2 sel addrl =
  32  forall_memory_ranged t chk2 chk1 mem2 mem1 sel addrl.
  33  #t; #chk1; #chk2; #mem1; #mem2; #sel; #addrl;
  34  nelim addrl;
  35  ##[ ##1: nnormalize; napply refl_eq
  36  ##| ##2: #a; #l; #H;
  37           nchange with (
  38            ((eqc ? (mem_read t mem1 chk1 sel a)
  39                    (mem_read t mem2 chk2 sel a)) ⊗
  40            (forall_memory_ranged t chk1 chk2 mem1 mem2 sel l)) =
  41            ((eqc ? (mem_read t mem2 chk2 sel a)
  42                    (mem_read t mem1 chk1 sel a)) ⊗
  43            (forall_memory_ranged t chk2 chk1 mem2 mem1 sel l)));
  44            nrewrite > H;
  45            nrewrite > (symmetric_eqc ? … (mem_read t mem1 chk1 sel a) (mem_read t mem2 chk2 sel a));
  46            napply refl_eq
  47  ##]
  48 nqed.
  49
  50 nlemma anystatus_destruct_1 :
  51 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
  52  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
  53  x1 = y1.
  54  #m; #t;
  55  #x1; #x2; #x3; #x4;
  56  #y1; #y2; #y3; #y4; #H;
  57  nchange with (match mk_any_status m t y1 y2 y3 y4
  58                 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
  59  nrewrite < H;
  60  nnormalize;
  61  napply refl_eq.
  62 nqed.
  63
  64 nlemma anystatus_destruct_2 :
  65 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
  66  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
  67  x2 = y2.
  68  #m; #t;
  69  #x1; #x2; #x3; #x4;
  70  #y1; #y2; #y3; #y4; #H;
  71  nchange with (match mk_any_status m t y1 y2 y3 y4
  72                 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
  73  nrewrite < H;
  74  nnormalize;
  75  napply refl_eq.
  76 nqed.
  77
  78 nlemma anystatus_destruct_3 :
  79 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
  80  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
  81  x3 = y3.
  82  #m; #t;
  83  #x1; #x2; #x3; #x4;
  84  #y1; #y2; #y3; #y4; #H;
  85  nchange with (match mk_any_status m t y1 y2 y3 y4
  86                 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
  87  nrewrite < H;
  88  nnormalize;
  89  napply refl_eq.
  90 nqed.
  91
  92 nlemma anystatus_destruct_4 :
  93 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
  94  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
  95  x4 = y4.
  96  #m; #t;
  97  #x1; #x2; #x3; #x4;
  98  #y1; #y2; #y3; #y4; #H;
  99  nchange with (match mk_any_status m t y1 y2 y3 y4
 100                 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
 101  nrewrite < H;
 102  nnormalize;
 103  napply refl_eq.
 104 nqed.
 105
 106 nlemma eq_to_eqanystatus : ∀m,t.∀s1,s2:any_status m t.s1 = s2 → eq_anystatus m t s1 s2 = true.
 107  #m; #t;
 108  #s1; ncases s1; #alu1; #mem1; #chk1; #clk1;
 109  #s2; ncases s2; #alu2; #mem2; #chk2; #clk2;
 110  #H;
 111  nrewrite > (anystatus_destruct_1 … H);
 112  nrewrite > (anystatus_destruct_2 … H);
 113  nrewrite > (anystatus_destruct_3 … H);
 114  nrewrite > (anystatus_destruct_4 … H);
 115  nchange with (
 116  ((eqc ? alu2 alu2) ⊗ (eqc ? mem2 mem2) ⊗ (eqc ? chk2 chk2) ⊗ (eqc ? clk2 clk2)) = true);
 117  nrewrite > (eq_to_eqc ? alu2 alu2 (refl_eq …));
 118  nrewrite > (eq_to_eqc ? mem2 mem2 (refl_eq …));
 119  nrewrite > (eq_to_eqc ? chk2 chk2 (refl_eq …));
 120  nrewrite > (eq_to_eqc ? clk2 clk2 (refl_eq …));
 121  napply refl_eq.
 122 nqed.
 123
 124 nlemma neqanystatus_to_neq : ∀m,t.∀s1,s2:any_status m t.eq_anystatus m t s1 s2 = false → s1 ≠ s2.
 125  #m; #t; #s1; #s2; #H;
 126  napply (not_to_not (s1 = s2) (eq_anystatus m t s1 s2 = true) …);
 127  ##[ ##1: napply (eq_to_eqanystatus m t s1 s2)
 128  ##| ##2: napply (eqfalse_to_neqtrue … H)
 129  ##]
 130 nqed.
 131
 132 nlemma eqanystatus_to_eq : ∀m,t.∀s1,s2:any_status m t.eq_anystatus m t s1 s2 = true → s1 = s2.
 133  #m; #t;
 134  #s1; ncases s1; #alu1; #mem1; #chk1; #clk1;
 135  #s2; ncases s2; #alu2; #mem2; #chk2; #clk2;
 136  nchange with (
 137  ((eqc ? alu1 alu2) ⊗ (eqc ? mem1 mem2) ⊗ (eqc ? chk1 chk2) ⊗ (eqc ? clk1 clk2)) = true → ?);
 138  #H;
 139  nrewrite > (eqc_to_eq … (andb_true_true_r … H));
 140  nletin H1 ≝ (andb_true_true_l … H);
 141  nrewrite > (eqc_to_eq … (andb_true_true_r … H1));
 142  nletin H2 ≝ (andb_true_true_l … H1);
 143  nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
 144  nrewrite > (eqc_to_eq … (andb_true_true_l … H2));
 145  napply refl_eq.
 146 nqed.
 147
 148 nlemma neq_to_neqanystatus : ∀m,t.∀s1,s2:any_status m t.s1 ≠ s2 → eq_anystatus m t s1 s2 = false.
 149  #m; #t; #s1; #s2; #H;
 150  napply (neqtrue_to_eqfalse (eq_anystatus m t s1 s2));
 151  napply (not_to_not (eq_anystatus m t s1 s2 = true) (s1 = s2) ? H);
 152  napply (eqanystatus_to_eq m t s1 s2).
 153 nqed.
 154
 155 nlemma decidable_anystatus : ∀m,t.∀x,y:any_status m t.decidable (x = y).
 156  #m; #t; #x; #y; nnormalize;
 157  napply (or2_elim (eq_anystatus m t x y = true) (eq_anystatus m t x y = false) ? (decidable_bexpr ?));
 158  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqanystatus_to_eq … H))
 159  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqanystatus_to_neq … H))
 160  ##]
 161 nqed.
 162
 163 nlemma symmetric_eqanystatus : ∀m,t.symmetricT (any_status m t) bool (eq_anystatus m t).
 164  #m; #t;
 165  #s1; ncases s1; #alu1; #mem1; #chk1; #clk1;
 166  #s2; ncases s2; #alu2; #mem2; #chk2; #clk2;
 167  nchange with (
 168  ((eqc ? alu1 alu2) ⊗ (eqc ? mem1 mem2) ⊗ (eqc ? chk1 chk2) ⊗ (eqc ? clk1 clk2)) =
 169  ((eqc ? alu2 alu1) ⊗ (eqc ? mem2 mem1) ⊗ (eqc ? chk2 chk1) ⊗ (eqc ? clk2 clk1)));
 170  nrewrite > (symmetric_eqc … alu1 alu2);
 171  nrewrite > (symmetric_eqc … mem1 mem2);
 172  nrewrite > (symmetric_eqc … chk1 chk2);
 173  nrewrite > (symmetric_eqc … clk1 clk2);
 174  napply refl_eq.
 175 nqed.
 176
 177 nlemma anystatus_is_comparable : mcu_type → memory_impl → comparable.
 178  #m; #t; @ (any_status m t)
 179   ##[ napply (mk_any_status m t (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
 180   ##| napply forall_anystatus
 181   ##| napply eq_anystatus
 182   ##| napply eqanystatus_to_eq
 183   ##| napply eq_to_eqanystatus
 184   ##| napply neqanystatus_to_neq
 185   ##| napply neq_to_neqanystatus
 186   ##| napply decidable_anystatus
 187   ##| napply symmetric_eqanystatus
 188   ##]
 189 nqed.
 190
 191 unification hint 0 ≔ M:mcu_type, T:memory_impl ⊢
 192  carr (anystatus_is_comparable M T) ≡ any_status M T.