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            letin K ≝
 167             (breakpoint
 168               (mk_status (byte_of_nat (x*n)) 4 O
 169                (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)))
 170                (plusbytec (byte_of_nat (x*pred n)) x)
 171                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 172                (byte_of_nat (x*n))) O)
 173               3 20); clearbody K;
 174            normalize in K:(? ? (? ? %) ?);
 175            rewrite > K; clear K;
 176            whd in ⊢ (? ? (? % ?) ?);
 177            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 178            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
 179             with (byte_of_nat (S a));
 180            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 181             (byte_of_nat (S a));
 182            (* instruction BEQ *)
 183            letin K ≝
 184             (breakpoint
 185               (mk_status (byte_of_nat (S a)) 6 O
 186                (eqbyte 〈x0, x0〉 (byte_of_nat (S a)))
 187                (plusbytec (byte_of_nat (x*pred n)) x)
 188                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 189                  (byte_of_nat (x*n))) O)
 190               3 17); clearbody K;
 191            normalize in K:(? ? (? ? %) ?);
 192            rewrite > K; clear K;
 193            whd in ⊢ (? ? (? % ?) ?);
 194            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
 195            rewrite > K; clear K;
 196            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 197            (* instruction LDAd *)
 198            rewrite > (breakpoint ? 3 14);
 199            whd in ⊢ (? ? (? % ?) ?);
 200            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
 201            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 202            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
 203            (* instruction DECd *)
 204            rewrite > (breakpoint ? 5 9);
 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            rewrite > (breakpoint ? 3 6);
 217            whd in ⊢ (? ? (? % ?) ?);
 218            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
 219             (plusbytenc (byte_of_nat (x*n)) x);
 220            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 221             (plusbytenc (byte_of_nat (x*n)) x);
 222            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 223            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
 224             with (plusbytec (byte_of_nat (x*n)) x);
 225            rewrite > plusbytenc_S;
 226            (* instruction STAd *)
 227            rewrite > (breakpoint ? 3 3);
 228            whd in ⊢ (? ? (? % ?) ?);
 229            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 230            (* instruction BRA *)
 231            whd in ⊢ (? ? % ?);
 232            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
 233            rewrite < pred_Sn;
 234            apply status_eq;
 235             [1,2,3,4,7: normalize; reflexivity
 236             | change with (plusbytec (byte_of_nat (x*n)) x =
 237                              plusbytec (byte_of_nat (x*n)) x);
 238               reflexivity
 239             |6: intro;
 240               simplify in ⊢ (? ? ? %);
 241               change in ⊢ (? ? % ?) with
 242                (update
 243                 (update
 244                  (update
 245                   (update (update (mult_memory x y) 30 x) 31
 246                    (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
 247                     (byte_of_nat (nat_of_byte y-S n)))
 248                    (nat_of_byte
 249                     (update
 250                      (update
 251                       (update (update (mult_memory x y) 30 x) 31
 252                        (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
 253                       (byte_of_nat (nat_of_byte y-S n)) 15))
 254                      (byte_of_nat (nat_of_byte x*S n)) a);
 255               normalize in ⊢ (? ? (? ? % ? ?) ?);
 256               apply inj_update;
 257               intro;
 258               apply inj_update;
 259               intro;
 260               rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
 261               rewrite > not_eq_a_b_to_eq_update_a_b;
 262                [ reflexivity
 263                | assumption
 264                ]
 265             ]
 266          | exists;
 267             [ apply (y - S n)
 268             | split;
 269                [ rewrite < (minus_S_S y n);
 270                  apply (minus_Sn_m (nat_of_byte y) (S n) H1)
 271                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
 272                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
 273                  autobatch
 274                ]
 275             ]
 276          ]
 277       ]
 278     | rewrite > associative_plus;
 279       rewrite < times_n_Sm;
 280       rewrite > sym_plus in ⊢ (? ? ? (? ? %));
 281       reflexivity
 282     ]
 283   ]
 284 qed.
 285
 286
 287 theorem test_x_y:
 288  ∀x,y:byte.
 289   let i ≝ 14 + 23 * y in
 290    execute (mult_status x y) i =
 291     mk_status (#(x*y)) 20 0
 292      (eqbyte 〈x0, x0〉 (#(x*y)))
 293      (plusbytec (byte_of_nat (x*pred y)) x)
 294      (update
 295        (update (mult_memory x y) 31 〈x0, x0〉)
 296        32 (byte_of_nat (x*y)))
 297      0.
 298  intros;
 299  cut (14 + 23 * y = 5 + 23*y + 9);
 300   [2: autobatch paramodulation;
 301   | rewrite > Hcut; (* clear Hcut; *)
 302     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
 303     rewrite > loop_invariant';
 304      [2: apply le_n
 305      | rewrite < minus_n_n;
 306        apply status_eq;
 307         [1,2,3,4,5,7: normalize; reflexivity
 308         | intro;
 309         letin xxx \def ((mult_memory x y) { a ↦ x }).
 310           change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
 311 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
 312            update (update (mult_memory x y) 31 〈x0, x0〉) 32
 313 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
 314           apply inj_update; intro;
 315           apply inj_update; intro;
 316           change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
 317           apply eq_update_s_a_sa
 318         ]
 319      ]
 320   ].
 321 qed.