helm/software/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       elim daemon
 122     ]
 123   | cut (5 + 23 * S n = 5 + 23 * n + 23);
 124     [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
 125       letin H' ≝ (H ?); clearbody H'; clear H;
 126       [ autobatch
 127       | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
 128         clear Hcut;
 129         rewrite > xxx;
 130         clear xxx;
 131         apply (transitive_eq ? ? ? ? K);
 132         clear K;
 133         rewrite > H';
 134         clear H';
 135         cut (∃z.y-n=S z ∧ z < 255);
 136          [ elim Hcut; clear Hcut;
 137            elim H; clear H;
 138            rewrite > H2;
 139            (* instruction LDAd *)
 140            letin K ≝
 141             (breakpoint
 142               (mk_status (byte_of_nat (x*n)) 4 O
 143                (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
 144                (plusbytec (byte_of_nat (x*pred n)) x)
 145                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 146                (byte_of_nat (x*n))) O)
 147               3 20); clearbody K;
 148            normalize in K:(? ? (? ? %) ?);
 149            apply transitive_eq; [2: apply K | skip | ]; clear K;
 150            whd in ⊢ (? ? (? % ?) ?);
 151            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 152            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
 153             with (byte_of_nat (S a));
 154            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 155             (byte_of_nat (S a));
 156            (* instruction BEQ *)
 157            letin K ≝
 158             (breakpoint
 159               (mk_status (byte_of_nat (S a)) 6 O
 160                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
 161                (plusbytec (byte_of_nat (x*pred n)) x)
 162                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 163                  (byte_of_nat (x*n))) O)
 164               3 17); clearbody K;
 165            normalize in K:(? ? (? ? %) ?);
 166            apply transitive_eq; [2: apply K | skip | ]; clear K;
 167            whd in ⊢ (? ? (? % ?) ?);
 168            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
 169            rewrite > K; clear K;
 170            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 171            (* instruction LDAd *)
 172            letin K ≝
 173             (breakpoint
 174               (mk_status (byte_of_nat (S a)) 8 O
 175                (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
 176                (plusbytec (byte_of_nat (x*pred n)) x)
 177                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 178                  (byte_of_nat (x*n))) O)
 179               3 14); clearbody K;
 180            normalize in K:(? ? (? ? %) ?);
 181            apply transitive_eq; [2: apply K | skip | ]; clear K;
 182            whd in ⊢ (? ? (? % ?) ?);
 183            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
 184            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 185            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
 186            (* instruction DECd *)
 187            letin K ≝
 188             (breakpoint
 189              (mk_status (byte_of_nat (x*n)) 10 O
 190               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
 191               (plusbytec (byte_of_nat (x*pred n)) x)
 192                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
 193                 (byte_of_nat (x*n))) O)
 194              5 9); clearbody K;
 195            normalize in K:(? ? (? ? %) ?);
 196            apply transitive_eq; [2: apply K | skip | ]; clear K;
 197            whd in ⊢ (? ? (? % ?) ?);
 198            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
 199            rewrite > (eq_bpred_S_a_a ? H3);
 200            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 201            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
 202            cut (y - S n = a);
 203             [2: elim daemon | ];
 204            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
 205            (* instruction ADDd *)
 206            letin K ≝
 207             (breakpoint
 208              (mk_status (byte_of_nat (x*n)) 12
 209               O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
 210               (plusbytec (byte_of_nat (x*pred n)) x)
 211               (update
 212                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
 213                32 (byte_of_nat (x*n))) 31
 214                (byte_of_nat (y-S n))) O)
 215              3 6); clearbody K;
 216            normalize in K:(? ? (? ? %) ?);
 217            apply transitive_eq; [2: apply K | skip | ]; clear K;
 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            letin K ≝
 229             (breakpoint
 230              (mk_status (byte_of_nat (x*S n)) 14 O
 231               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
 232               (plusbytec (byte_of_nat (x*n)) x)
 233                (update
 234                 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
 235                 32 (byte_of_nat (x*n))) 31
 236                 (byte_of_nat (y-S n))) O)
 237             3 3); clearbody K;
 238            normalize in K:(? ? (? ? %) ?);
 239            apply transitive_eq; [2: apply K | skip | ]; clear K;
 240            whd in ⊢ (? ? (? % ?) ?);
 241            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 242            (* instruction BRA *)
 243            whd in ⊢ (? ? % ?);
 244            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
 245            rewrite < pred_Sn;
 246            apply status_eq;
 247             [1,2,3,4,7: normalize; reflexivity
 248             | change with (plusbytec (byte_of_nat (x*n)) x =
 249                              plusbytec (byte_of_nat (x*n)) x);
 250               reflexivity
 251             |6: intro;
 252               elim daemon
 253             ]
 254          | exists;
 255             [ apply (y - S n)
 256             | split;
 257                [ rewrite < (minus_S_S y n);
 258                  autobatch
 259                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
 260                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
 261                  autobatch
 262                ]
 263             ]
 264          ]
 265       ]
 266     | rewrite > associative_plus;
 267       autobatch paramodulation
 268     ]
 269   ]
 270 qed.
 271
 272 theorem test_x_y:
 273  ∀x,y:byte.
 274   let i ≝ 14 + 23 * y in
 275    execute (mult_status x y) i =
 276     mk_status (byte_of_nat (x*y)) 20 0
 277      (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
 278      (plusbytec (byte_of_nat (x*pred y)) x)
 279      (update
 280        (update (mult_memory x y) 31 (mk_byte x0 x0))
 281        32 (byte_of_nat (x*y)))
 282      0.
 283  intros;
 284  cut (14 + 23 * y = 5 + 23*y + 9);
 285   [2: autobatch paramodulation;
 286   | rewrite > Hcut; (* clear Hcut; *)
 287     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
 288     rewrite > loop_invariant';
 289      [2: apply le_n
 290      | rewrite < minus_n_n;
 291        apply status_eq;
 292         [1,2,3,4,5,7: normalize; reflexivity
 293         | elim daemon
 294         ]
 295      ]
 296   ].
 297 qed.