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