helm/software/matita/library/freescale/tests.old

   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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 set "baseuri" "cic:/matita/freescale/tests/".
  28
  29 (*include "/media/VIRTUOSO/freescale/micro_tests.ma".*)
  30 include "freescale/micro_tests.ma".
  31
  32 (*
  33    RAM indirizzabile in modalita' diretta da usare per X,Y,Z
  34    A=X*Y (parte low) con [0x0020-0x004F] X ≝ [0x0020] Y ≝ [0x0021] Z ≝ [0x0022]
  35 *)
  36 definition test_mult_source_RS08 : list byte8 ≝
  37 let m ≝ RS08 in source_to_byte8 m (
  38 (* [0x3800] Z <- 0      3clk *) (compile m ? CLR (maDIR1 〈x2,x2〉) I) @
  39 (* [0x3802] (l1) A <- Y 3clk *) (compile m ? LDA (maDIR1 〈x2,x1〉) I) @
  40 (* [0x3804] A=0 goto l2 3clk *) (compile m ? BEQ (maIMM1 〈x0,xA〉) I) @
  41 (* [0x3806] A <- Z      3clk *) (compile m ? LDA (maDIR1 〈x2,x2〉) I) @
  42 (* [0x3808] Y --        5clk *) (compile m ? DEC (maDIR1 〈x2,x1〉) I) @
  43 (* [0x380A] A += X      3clk *) (compile m ? ADD (maDIR1 〈x2,x0〉) I) @
  44 (* [0x380C] Z <- A      3clk *) (compile m ? STA (maDIR1 〈x2,x2〉) I) @
  45 (* [0x380E] goto l1     3clk *) (compile m ? BRA (maIMM1 〈xF,x2〉) I) @
  46 (* [0x3810] (l2) A <- Z 3clk *) (compile m ? LDA (maDIR1 〈x2,x2〉) I)
  47  ).
  48
  49 (* ************** *)
  50 (* *****TODO***** *)
  51 (* ************** *)
  52
  53 definition mult_memory ≝
  54  λx,y.λa:addr.
  55      match leb a 29 with
  56       [ true ⇒ nth ? mult_source 〈x0, x0〉 a
  57       | false ⇒
  58          match eqb a 30 with
  59           [ true ⇒ x
  60           | false ⇒ y
  61           ]
  62       ].
  63
  64 definition mult_status ≝
  65  λx,y.
  66   mk_status 〈x0, x0〉 0 0 false false (mult_memory x y) 0.
  67
  68 notation " 'M' \sub (x y)" non associative with precedence 80 for
  69  @{ 'memory $x $y }.
  70
  71 interpretation "mult_memory" 'memory x y =
  72   (cic:/matita/freescale/test/mult_memory.con x y).
  73
  74 notation " 'M' \sub (x y) \nbsp a" non associative with precedence 80 for
  75  @{ 'memory4 $x $y $a }.
  76
  77 interpretation "mult_memory4" 'memory4 x y a =
  78   (cic:/matita/freescale/test/mult_memory.con x y a).
  79
  80 notation " \Sigma \sub (x y)" non associative with precedence 80 for
  81  @{ 'status $x $y }.
  82
  83 interpretation "mult_status" 'status x y =
  84   (cic:/matita/freescale/test/mult_status.con x y).
  85
  86 lemma test_O_O:
  87   let i ≝ 14 in
  88   let s ≝ execute (mult_status 〈x0, x0〉 〈x0, x0〉) i in
  89    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
  90  split;
  91  reflexivity.
  92 qed.
  93
  94 lemma test_0_2:
  95   let x ≝ 〈x0, x0〉 in
  96   let y ≝ 〈x0, x2〉 in
  97   let i ≝ 14 + 23 * nat_of_byte y in
  98   let s ≝ execute (mult_status x y) i in
  99    pc s = 20 ∧ mem s 32 = plusbytenc x x.
 100  intros;
 101  split;
 102  reflexivity.
 103 qed.
 104
 105 lemma test_x_1:
 106  ∀x.
 107   let y ≝ 〈x0, x1〉 in
 108   let i ≝ 14 + 23 * nat_of_byte y in
 109   let s ≝ execute (mult_status x y) i in
 110    pc s = 20 ∧ mem s 32 = x.
 111  intros;
 112  split;
 113   [ reflexivity
 114   | change in ⊢ (? ? % ?) with (plusbytenc 〈x0, x0〉 x);
 115     rewrite > plusbytenc_O_x;
 116     reflexivity
 117   ].
 118 qed.
 119
 120 lemma test_x_2:
 121  ∀x.
 122   let y ≝ 〈x0, x2〉 in
 123   let i ≝ 14 + 23 * nat_of_byte y in
 124   let s ≝ execute (mult_status x y) i in
 125    pc s = 20 ∧ mem s 32 = plusbytenc x x.
 126  intros;
 127  split;
 128   [ reflexivity
 129   | change in ⊢ (? ? % ?) with
 130      (plusbytenc (plusbytenc 〈x0, x0〉 x) x);
 131     rewrite > plusbytenc_O_x;
 132     reflexivity
 133   ].
 134 qed.
 135
 136 lemma loop_invariant':
 137  ∀x,y:byte.∀j:nat. j ≤ y →
 138   execute (mult_status x y) (5 + 23*j)
 139    =
 140     mk_status (byte_of_nat (x * j)) 4 0 (eqbyte 〈x0, x0〉 (byte_of_nat (x*j)))
 141      (plusbytec (byte_of_nat (x*pred j)) x)
 142      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
 143       (byte_of_nat (x * j)))
 144      0.
 145  intros 3;
 146  elim j;
 147   [ do 2 (rewrite < times_n_O);
 148     apply status_eq;
 149     [1,2,3,4,7: normalize; reflexivity
 150     | rewrite > eq_plusbytec_x0_x0_x_false;
 151       normalize;
 152       reflexivity
 153     | intro;
 154       rewrite < minus_n_O;
 155       normalize in ⊢ (? ? (? (? ? %) ?) ?);
 156       change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 〈x0, x0〉 a);
 157       simplify in ⊢ (? ? ? %);
 158       change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
 159       rewrite > byte_of_nat_nat_of_byte;
 160       change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
 161       apply inj_update;
 162       intro;
 163       rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
 164        31 a);
 165       rewrite > eq_update_s_a_sa;
 166       reflexivity
 167     ]
 168   | cut (5 + 23 * S n = 5 + 23 * n + 23);
 169     [ rewrite > Hcut; clear Hcut;
 170       rewrite > breakpoint;
 171       rewrite > H; clear H;
 172       [2: apply le_S_S_to_le;
 173         apply le_S;
 174         apply H1
 175       | cut (∃z.y-n=S z ∧ z < 255);
 176          [ elim Hcut; clear Hcut;
 177            elim H; clear H;
 178            rewrite > H2;
 179            (* instruction LDAd *)
 180            change in ⊢ (? ? (? ? %) ?) with (3+20);
 181            rewrite > breakpoint in ⊢ (? ? % ?);
 182            whd in ⊢ (? ? (? % ?) ?);
 183            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 184            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
 185             with (byte_of_nat (S a));
 186            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 187             (byte_of_nat (S a));
 188            (* instruction BEQ *)
 189            change in ⊢ (? ? (? ? %) ?) with (3+17);
 190            rewrite > breakpoint in ⊢ (? ? % ?);
 191            whd in ⊢ (? ? (? % ?) ?);
 192            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
 193            rewrite > K; clear K;
 194            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 195            (* instruction LDAd *)
 196            change in ⊢ (? ? (? ? %) ?) with (3+14);
 197            rewrite > breakpoint in ⊢ (? ? % ?);
 198            whd in ⊢ (? ? (? % ?) ?);
 199            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
 200            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 201            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
 202            (* instruction DECd *)
 203            change in ⊢ (? ? (? ? %) ?) with (5+9);
 204            rewrite > breakpoint in ⊢ (? ? % ?);
 205            whd in ⊢ (? ? (? % ?) ?);
 206            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
 207            rewrite > (eq_bpred_S_a_a ? H3);
 208            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 209            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
 210            cut (y - S n = a);
 211             [2: rewrite > eq_minus_S_pred;
 212                 rewrite > H2;
 213                 reflexivity | ];
 214            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
 215            (* instruction ADDd *)
 216            change in ⊢ (? ? (? ? %) ?) with (3+6);
 217            rewrite > breakpoint in ⊢ (? ? % ?);
 218            whd in ⊢ (? ? (? % ?) ?);
 219            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
 220             (plusbytenc (byte_of_nat (x*n)) x);
 221            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 222             (plusbytenc (byte_of_nat (x*n)) x);
 223            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 224            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
 225             with (plusbytec (byte_of_nat (x*n)) x);
 226            rewrite > plusbytenc_S;
 227            (* instruction STAd *)
 228            rewrite > (breakpoint ? 3 3);
 229            whd in ⊢ (? ? (? % ?) ?);
 230            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 231            (* instruction BRA *)
 232            whd in ⊢ (? ? % ?);
 233            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
 234            rewrite < pred_Sn;
 235            apply status_eq;
 236             [1,2,3,4,7: normalize; reflexivity
 237             | change with (plusbytec #(x*n) x = plusbytec #(x*n) x);
 238               reflexivity
 239             |6: intro;
 240               simplify in ⊢ (? ? ? %);
 241               normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? (? %) ?) ?) ?) ?);
 242               change in ⊢ (? ? % ?) with
 243                ((mult_memory x y){30↦x}{31↦#(S (y-S n))}{32↦#(x*n)}{31↦#(y-S n)}
 244                 {〈x2,x0〉↦ #(x*S n)} a);
 245               apply inj_update;
 246               intro;
 247               apply inj_update;
 248               intro;
 249               rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
 250               rewrite > not_eq_a_b_to_eq_update_a_b;
 251                [ reflexivity
 252                | assumption
 253                ]
 254             ]
 255          | exists;
 256             [ apply (y - S n)
 257             | split;
 258                [ rewrite < (minus_S_S y n);
 259                  apply (minus_Sn_m (nat_of_byte y) (S n) H1)
 260                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
 261                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
 262                  [ apply (lt_to_le_to_lt O (S n) (nat_of_byte y) ? ?);
 263                    autobatch
 264                  | autobatch
 265                  | autobatch
 266                  ]
 267                ]
 268             ]
 269          ]
 270       ]
 271     | rewrite > associative_plus;
 272       rewrite < times_n_Sm;
 273       rewrite > sym_plus in ⊢ (? ? ? (? ? %));
 274       reflexivity
 275     ]
 276   ]
 277 qed.
 278
 279
 280 theorem test_x_y:
 281  ∀x,y:byte.
 282   let i ≝ 14 + 23 * y in
 283    execute (mult_status x y) i =
 284     mk_status (#(x*y)) 20 0
 285      (eqbyte 〈x0, x0〉 (#(x*y)))
 286      (plusbytec (byte_of_nat (x*pred y)) x)
 287      (update
 288        (update (mult_memory x y) 31 〈x0, x0〉)
 289        32 (byte_of_nat (x*y)))
 290      0.
 291  intros;
 292  cut (14 + 23 * y = 5 + 23*y + 9);
 293   [2: autobatch paramodulation;
 294   | rewrite > Hcut; (* clear Hcut; *)
 295     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
 296     rewrite > loop_invariant';
 297      [2: apply le_n
 298      | rewrite < minus_n_n;
 299        apply status_eq;
 300         [1,2,3,4,5,7: normalize; reflexivity
 301         | intro;
 302           simplify in ⊢ (? ? ? %);
 303           change in ⊢ (? ? % ?) with
 304            (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
 305 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
 306           repeat (apply inj_update; intro);
 307           apply (eq_update_s_a_sa ? 30)
 308         ]
 309      ]
 310   ].
 311 qed.