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  normalize;
  69  split;
  70  reflexivity.
  71 qed.
  72
  73 (*
  74 lemma test_0_2:
  75   let x ≝ 〈x0, x0〉 in
  76   let y ≝ 〈x0, x2〉 in
  77   let i ≝ 14 + 23 * nat_of_byte y in
  78   let s ≝ execute (mult_status x y) i in
  79    pc s = 20 ∧ mem s 32 = plusbytenc x x.
  80  intros;
  81  split;
  82  reflexivity.
  83 qed.
  84 *)
  85
  86 lemma test_x_1:
  87  ∀x.
  88   let y ≝ 〈x0, x1〉 in
  89   let i ≝ 14 + 23 * nat_of_byte y in
  90   let s ≝ execute (mult_status x y) i in
  91    pc s = 20 ∧ mem s 32 = x.
  92  intros;
  93  split;
  94   [ reflexivity
  95   | change in ⊢ (? ? % ?) with (plusbytenc 〈x0, x0〉 x);
  96     rewrite > plusbytenc_O_x;
  97     reflexivity
  98   ].
  99 qed.
 100
 101 (*
 102 lemma test_x_2:
 103  ∀x.
 104   let y ≝ 〈x0, x2〉 in
 105   let i ≝ 14 + 23 * nat_of_byte y in
 106   let s ≝ execute (mult_status x y) i in
 107    pc s = 20 ∧ mem s 32 = plusbytenc x x.
 108  intros;
 109  split;
 110   [ reflexivity
 111   | change in ⊢ (? ? % ?) with
 112      (plusbytenc (plusbytenc 〈x0, x0〉 x) x);
 113     rewrite > plusbytenc_O_x;
 114     reflexivity
 115   ].
 116 qed.
 117 *)
 118
 119 lemma loop_invariant':
 120  ∀x,y:byte.∀j:nat. j ≤ y →
 121   execute (mult_status x y) (5 + 23*j)
 122    =
 123     mk_status (byte_of_nat (x * j)) 4 0 (eqbyte 〈x0, x0〉 (byte_of_nat (x*j)))
 124      (plusbytec (byte_of_nat (x*pred j)) x)
 125      (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
 126       (byte_of_nat (x * j)))
 127      0.
 128  intros 3;
 129  elim j;
 130   [ do 2 (rewrite < times_n_O);
 131     apply status_eq;
 132     [1,2,3,4,7: normalize; reflexivity
 133     | rewrite > eq_plusbytec_x0_x0_x_false;
 134       normalize;
 135       reflexivity
 136     | intro;
 137       rewrite < minus_n_O;
 138       normalize in ⊢ (? ? (? (? ? %) ?) ?);
 139       change in ⊢ (? ? % ?) with (update (mult_memory x y) 32 〈x0, x0〉 a);
 140       change in ⊢ (? ? ? %) with (update (update (update (mult_memory x y) 30 x) 31
 141         (byte_of_nat y)) 32 (byte_of_nat 0) a);
 142       change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
 143       rewrite > byte_of_nat_nat_of_byte;
 144       change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
 145       apply inj_update;
 146       intro;
 147       rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
 148        31 a) in ⊢ (? ? ? %);
 149       rewrite > eq_update_s_a_sa;
 150       reflexivity
 151     ]
 152   | cut (5 + 23 * S n = 5 + 23 * n + 23);
 153     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
 154       letin H' ≝ (H ?); clearbody H'; clear H;
 155       [ autobatch
 156       | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
 157         clear Hcut;
 158         rewrite > xxx;
 159         clear xxx;
 160         apply (transitive_eq ? ? ? ? K);
 161         clear K;
 162         rewrite > H';
 163         clear H';
 164         cut (∃z.y-n=S z ∧ z < 255);
 165          [ elim Hcut; clear Hcut;
 166            elim H; clear H;
 167            rewrite > H2;
 168            (* instruction LDAd *)
 169            letin K ≝
 170             (breakpoint
 171               (mk_status (byte_of_nat (x*n)) 4 O
 172                (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)))
 173                (plusbytec (byte_of_nat (x*pred n)) x)
 174                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 175                (byte_of_nat (x*n))) O)
 176               3 20); clearbody K;
 177            normalize in K:(? ? (? ? %) ?);
 178            apply transitive_eq; [2: apply K | skip | ]; clear K;
 179            whd in ⊢ (? ? (? % ?) ?);
 180            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 181            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
 182             with (byte_of_nat (S a));
 183            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 184             (byte_of_nat (S a));
 185            (* instruction BEQ *)
 186            letin K ≝
 187             (breakpoint
 188               (mk_status (byte_of_nat (S a)) 6 O
 189                (eqbyte 〈x0, x0〉 (byte_of_nat (S a)))
 190                (plusbytec (byte_of_nat (x*pred n)) x)
 191                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 192                  (byte_of_nat (x*n))) O)
 193               3 17); clearbody K;
 194            normalize in K:(? ? (? ? %) ?);
 195            apply transitive_eq; [2: apply K | skip | ]; clear K;
 196            whd in ⊢ (? ? (? % ?) ?);
 197            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
 198            rewrite > K; clear K;
 199            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 200            (* instruction LDAd *)
 201            letin K ≝
 202             (breakpoint
 203               (mk_status (byte_of_nat (S a)) 8 O
 204                (eqbyte 〈x0, x0〉 (byte_of_nat (S a)))
 205                (plusbytec (byte_of_nat (x*pred n)) x)
 206                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 207                  (byte_of_nat (x*n))) O)
 208               3 14); clearbody K;
 209            normalize in K:(? ? (? ? %) ?);
 210            apply transitive_eq; [2: apply K | skip | ]; clear K;
 211            whd in ⊢ (? ? (? % ?) ?);
 212            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
 213            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 214            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
 215            (* instruction DECd *)
 216            letin K ≝
 217             (breakpoint
 218              (mk_status (byte_of_nat (x*n)) 10 O
 219               (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)))
 220               (plusbytec (byte_of_nat (x*pred n)) x)
 221                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 222                 (byte_of_nat (x*n))) O)
 223              5 9); clearbody K;
 224            normalize in K:(? ? (? ? %) ?);
 225            apply transitive_eq; [2: apply K | skip | ]; clear K;
 226            whd in ⊢ (? ? (? % ?) ?);
 227            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
 228            rewrite > (eq_bpred_S_a_a ? H3);
 229            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 230            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
 231            cut (y - S n = a);
 232             [2: rewrite > eq_minus_S_pred;
 233                 rewrite > H2;
 234                 reflexivity | ];
 235            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
 236            (* instruction ADDd *)
 237            letin K ≝
 238             (breakpoint
 239              (mk_status (byte_of_nat (x*n)) 12
 240               O (eqbyte 〈x0, x0〉 (byte_of_nat (y-S n)))
 241               (plusbytec (byte_of_nat (x*pred n)) x)
 242               (update
 243                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
 244                32 (byte_of_nat (x*n))) 31
 245                (byte_of_nat (y-S n))) O)
 246              3 6); clearbody K;
 247            normalize in K:(? ? (? ? %) ?);
 248            apply transitive_eq; [2: apply K | skip | ]; clear K;
 249            whd in ⊢ (? ? (? % ?) ?);
 250            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
 251             (plusbytenc (byte_of_nat (x*n)) x);
 252            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 253             (plusbytenc (byte_of_nat (x*n)) x);
 254            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 255            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
 256             with (plusbytec (byte_of_nat (x*n)) x);
 257            rewrite > plusbytenc_S;
 258            (* instruction STAd *)
 259            letin K ≝
 260             (breakpoint
 261              (mk_status (byte_of_nat (x*S n)) 14 O
 262               (eqbyte 〈x0, x0〉 (byte_of_nat (x*S n)))
 263               (plusbytec (byte_of_nat (x*n)) x)
 264                (update
 265                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
 266                 32 (byte_of_nat (x*n))) 31
 267                 (byte_of_nat (y-S n))) O)
 268             3 3); clearbody K;
 269            normalize in K:(? ? (? ? %) ?);
 270            apply transitive_eq; [2: apply K | skip | ]; clear K;
 271            whd in ⊢ (? ? (? % ?) ?);
 272            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 273            (* instruction BRA *)
 274            whd in ⊢ (? ? % ?);
 275            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
 276            rewrite < pred_Sn;
 277            apply status_eq;
 278             [1,2,3,4,7: normalize; reflexivity
 279             | change with (plusbytec (byte_of_nat (x*n)) x =
 280                              plusbytec (byte_of_nat (x*n)) x);
 281               reflexivity
 282             |6: intro;
 283               simplify in ⊢ (? ? ? %);
 284               change in ⊢ (? ? % ?) with
 285                (update
 286                 (update
 287                  (update
 288                   (update (update (mult_memory x y) 30 x) 31
 289                    (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
 290                     (byte_of_nat (nat_of_byte y-S n)))
 291                    (nat_of_byte
 292                     (update
 293                      (update
 294                       (update (update (mult_memory x y) 30 x) 31
 295                        (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
 296                       (byte_of_nat (nat_of_byte y-S n)) 15))
 297                      (byte_of_nat (nat_of_byte x*S n)) a);
 298               normalize in ⊢ (? ? (? ? % ? ?) ?);
 299               apply inj_update;
 300               intro;
 301               apply inj_update;
 302               intro;
 303               rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?); [2: apply H | ];
 304               rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?);
 305                [ reflexivity
 306                | assumption
 307                ]
 308             ]
 309          | exists;
 310             [ apply (y - S n)
 311             | split;
 312                [ rewrite < (minus_S_S y n);
 313                  apply (minus_Sn_m (nat_of_byte y) (S n) H1)
 314                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
 315                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
 316                  autobatch
 317                ]
 318             ]
 319          ]
 320       ]
 321     | rewrite > associative_plus;
 322       rewrite < times_n_Sm;
 323       rewrite > sym_plus in ⊢ (? ? ? (? ? %));
 324       reflexivity
 325     ]
 326   ]
 327 qed.
 328
 329
 330 theorem test_x_y:
 331  ∀x,y:byte.
 332   let i ≝ 14 + 23 * y in
 333    execute (mult_status x y) i =
 334     mk_status (#(x*y)) 20 0
 335      (eqbyte 〈x0, x0〉 (#(x*y)))
 336      (plusbytec (byte_of_nat (x*pred y)) x)
 337      (update
 338        (update (mult_memory x y) 31 〈x0, x0〉)
 339        32 (byte_of_nat (x*y)))
 340      0.
 341  intros;
 342  cut (14 + 23 * y = 5 + 23*y + 9);
 343   [2: autobatch paramodulation;
 344   | rewrite > Hcut; (* clear Hcut; *)
 345     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
 346     rewrite > loop_invariant';
 347      [2: apply le_n
 348      | rewrite < minus_n_n;
 349        apply status_eq;
 350         [1,2,3,4,5,7: normalize; reflexivity
 351         | intro;
 352         letin xxx \def ((mult_memory x y) { a ↦ x }).
 353           change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
 354 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
 355            update (update (mult_memory x y) 31 〈x0, x0〉) 32
 356 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
 357           apply inj_update; intro;
 358           apply inj_update; intro;
 359           change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
 360           apply eq_update_s_a_sa
 361         ]
 362      ]
 363   ].
 364 qed.