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