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
  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       simplify in ⊢ (? ? ? %);
 136       change in ⊢ (? ? ? (? (? (? ? ? %) ? ?) ? ? ?)) with (mult_memory x y 30);
 137       rewrite > byte_of_nat_nat_of_byte;
 138       change in ⊢ (? ? ? (? (? ? ? %) ? ? ?)) with (mult_memory x y 31);
 139       apply inj_update;
 140       intro;
 141       rewrite > (eq_update_s_a_sa (update (mult_memory x y) 30 (mult_memory x y 30))
 142        31 a);
 143       rewrite > eq_update_s_a_sa;
 144       reflexivity
 145     ]
 146   | cut (5 + 23 * S n = 5 + 23 * n + 23);
 147     [ rewrite > Hcut; clear Hcut;
 148       rewrite > breakpoint;
 149       rewrite > H; clear H;
 150       [2: apply le_S_S_to_le;
 151         apply le_S;
 152         apply H1
 153       | cut (∃z.y-n=S z ∧ z < 255);
 154          [ elim Hcut; clear Hcut;
 155            elim H; clear H;
 156            rewrite > H2;
 157            (* instruction LDAd *)
 158            change in ⊢ (? ? (? ? %) ?) with (3+20);
 159            rewrite > breakpoint in ⊢ (? ? % ?);
 160            whd in ⊢ (? ? (? % ?) ?);
 161            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 162            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
 163             with (byte_of_nat (S a));
 164            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 165             (byte_of_nat (S a));
 166            (* instruction BEQ *)
 167            change in ⊢ (? ? (? ? %) ?) with (3+17);
 168            rewrite > breakpoint in ⊢ (? ? % ?);
 169            whd in ⊢ (? ? (? % ?) ?);
 170            letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
 171            rewrite > K; clear K;
 172            simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 173            (* instruction LDAd *)
 174            change in ⊢ (? ? (? ? %) ?) with (3+14);
 175            rewrite > breakpoint in ⊢ (? ? % ?);
 176            whd in ⊢ (? ? (? % ?) ?);
 177            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
 178            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 179            change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte 〈x0, x0〉 (byte_of_nat (x*n)));
 180            (* instruction DECd *)
 181            change in ⊢ (? ? (? ? %) ?) with (5+9);
 182            rewrite > breakpoint in ⊢ (? ? % ?);
 183            whd in ⊢ (? ? (? % ?) ?);
 184            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
 185            rewrite > (eq_bpred_S_a_a ? H3);
 186            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 187            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
 188            cut (y - S n = a);
 189             [2: rewrite > eq_minus_S_pred;
 190                 rewrite > H2;
 191                 reflexivity | ];
 192            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
 193            (* instruction ADDd *)
 194            change in ⊢ (? ? (? ? %) ?) with (3+6);
 195            rewrite > breakpoint in ⊢ (? ? % ?);
 196            whd in ⊢ (? ? (? % ?) ?);
 197            change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
 198             (plusbytenc (byte_of_nat (x*n)) x);
 199            change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
 200             (plusbytenc (byte_of_nat (x*n)) x);
 201            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 202            change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
 203             with (plusbytec (byte_of_nat (x*n)) x);
 204            rewrite > plusbytenc_S;
 205            (* instruction STAd *)
 206            rewrite > (breakpoint ? 3 3);
 207            whd in ⊢ (? ? (? % ?) ?);
 208            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
 209            (* instruction BRA *)
 210            whd in ⊢ (? ? % ?);
 211            normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
 212            rewrite < pred_Sn;
 213            apply status_eq;
 214             [1,2,3,4,7: normalize; reflexivity
 215             | change with (plusbytec #(x*n) x = plusbytec #(x*n) x);
 216               reflexivity
 217             |6: intro;
 218               simplify in ⊢ (? ? ? %);
 219               normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? (? %) ?) ?) ?) ?);
 220               change in ⊢ (? ? % ?) with
 221                ((mult_memory x y){30↦x}{31↦#(S (y-S n))}{32↦#(x*n)}{31↦#(y-S n)}
 222                 {〈x2,x0〉↦ #(x*S n)} a);
 223               apply inj_update;
 224               intro;
 225               apply inj_update;
 226               intro;
 227               rewrite > not_eq_a_b_to_eq_update_a_b; [2: apply H | ];
 228               rewrite > not_eq_a_b_to_eq_update_a_b;
 229                [ reflexivity
 230                | assumption
 231                ]
 232             ]
 233          | exists;
 234             [ apply (y - S n)
 235             | split;
 236                [ rewrite < (minus_S_S y n);
 237                  apply (minus_Sn_m (nat_of_byte y) (S n) H1)
 238                | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
 239                  letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
 240                  [ apply (lt_to_le_to_lt O (S n) (nat_of_byte y) ? ?);
 241                    autobatch
 242                  | autobatch
 243                  | autobatch
 244                  ]
 245                ]
 246             ]
 247          ]
 248       ]
 249     | rewrite > associative_plus;
 250       rewrite < times_n_Sm;
 251       rewrite > sym_plus in ⊢ (? ? ? (? ? %));
 252       reflexivity
 253     ]
 254   ]
 255 qed.
 256
 257
 258 theorem test_x_y:
 259  ∀x,y:byte.
 260   let i ≝ 14 + 23 * y in
 261    execute (mult_status x y) i =
 262     mk_status (#(x*y)) 20 0
 263      (eqbyte 〈x0, x0〉 (#(x*y)))
 264      (plusbytec (byte_of_nat (x*pred y)) x)
 265      (update
 266        (update (mult_memory x y) 31 〈x0, x0〉)
 267        32 (byte_of_nat (x*y)))
 268      0.
 269  intros;
 270  cut (14 + 23 * y = 5 + 23*y + 9);
 271   [2: autobatch paramodulation;
 272   | rewrite > Hcut; (* clear Hcut; *)
 273     rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
 274     rewrite > loop_invariant';
 275      [2: apply le_n
 276      | rewrite < minus_n_n;
 277        apply status_eq;
 278         [1,2,3,4,5,7: normalize; reflexivity
 279         | intro;
 280           simplify in ⊢ (? ? ? %);
 281           change in ⊢ (? ? % ?) with
 282            (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
 283 (byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
 284           repeat (apply inj_update; intro);
 285           apply (eq_update_s_a_sa ? 30)
 286         ]
 287      ]
 288   ].
 289 qed.