Changeset 1955


Ignore:
Timestamp:
May 16, 2012, 3:03:52 PM (7 years ago)
Author:
mulligan
Message:

Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some small changes to the statement

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1946 r1955  
    545545
    546546example add_SO:
    547  ∀pc.
    548  add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1) = bitvector_of_nat … (S pc).
     547  ∀n: nat.
     548  ∀m: nat.
     549    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
    549550 cases daemon.
    550551qed.
  • src/ASM/AssemblyProof.ma

    r1953 r1955  
    1717      bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
    1818  ].
    19   [1:
    20     applyS prefix
    21   |2:
    22     letin res ≝ (bit ::: prefix)
    23     <minus_S_S >minus_Sn_m
    24     try assumption @res
    25   |3:
    26     @le_S_to_le
    27     assumption
    28   ]
     19  try applyS prefix
     20  try (@le_S_to_le assumption)
     21  letin res ≝ (bit ::: prefix)
     22  <minus_S_S >minus_Sn_m
     23  assumption
    2924qed.
    3025
     
    3328  λP: BitVector n → Prop.
    3429    bitvector_elim_prop_internal n P n ? ?.
    35   [ @(le_n ?)
    36   | <(minus_n_n ?)
    37     @[[ ]]
    38   ]
     30  try @le_n
     31  <minus_n_n @[[ ]]
    3932qed.
    4033
     
    6053  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
    6154  ].
    62   [1:
    63     applyS prefix
    64   |2:
    65     letin res ≝ (bit ::: prefix)
    66     <(minus_S_S ? ?) >(minus_Sn_m ? ?)
    67     try @prf2 @res
    68   |3:
    69     /2/
    70   ].
     55  /2/
    7156qed.
    7257
     
    12841269  ].
    12851270
     1271axiom add_commutative:
     1272  ∀n: nat.
     1273  ∀l, r: BitVector n.
     1274    add n l r = add n r l.
     1275
    12861276axiom add_bitvector_of_nat_Sm:
    12871277  ∀n, m: nat.
     
    13211311qed.
    13221312
    1323 axiom bitvector_3_cases:
     1313lemma destruct_bug_fix:
     1314  3 = 0 → False.
     1315  #absurd destruct(absurd)
     1316qed.
     1317
     1318definition bitvector_3_cases:
    13241319  ∀b: BitVector 3.
    1325   ∃l, c, r: bool.
    1326     b = [[l; c; r]].
     1320    ∃l, c, r: bool.
     1321      b ≃ [[l; c; r]] ≝ ?.
     1322  #b
     1323  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
     1324  [1:
     1325    #absurd @⊥ @destruct_bug_fix
     1326    >absurd %
     1327  |2:
     1328    #n #hd #tl #_ #_ #_ %{hd}
     1329    cases daemon
     1330  ]
     1331qed.
    13271332
    13281333lemma bitvector_3_elim_prop:
     
    21872192qed.
    21882193
     2194definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
     2195  λpseudo_instruction.
     2196    match pseudo_instruction with
     2197    [ Comment c ⇒ False
     2198    | Cost c ⇒ False
     2199    | _ ⇒ True
     2200    ].
     2201   
    21892202(*CSC: ???*)
    21902203lemma snd_assembly_1_pseudoinstruction_ok:
     
    21942207  ∀ppc: Word.
    21952208  ∀pi.
     2209  ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi.
    21962210  ∀lookup_labels.
    21972211  ∀lookup_datalabels.
     
    21992213    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    22002214    \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    2201     let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels  pi) in
     2215    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels  pi) in
    22022216      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    2203   #program #sigma #policy #ppc #pi #lookup_labels #lookup_datalabels
    2204   #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
    2205   normalize nodelta cases daemon (* XXX: !!! *)
     2217  #program #sigma #policy #ppc #pi #is_present_in_machine_code_image_witness
     2218  #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl
     2219  #fetch_pseudo_refl
     2220  normalize nodelta
     2221  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
     2222  generalize in match is_present_in_machine_code_image_witness; -is_present_in_machine_code_image_witness
     2223  cases pi
     2224  [1:
     2225    #preinstruction #_
     2226  |2,3:
     2227    (* XXX: bug in original statement here, to prove: sigma (ppc + 1) = sigma ppc *)
     2228    #cost_or_comment normalize in ⊢ (% → ?); #absurd cases absurd
     2229  |4,5:
     2230    #identifier #_
     2231  |6:
     2232    #dptr #identifier #_
     2233  ]
     2234  #fetch_pseudo_refl
     2235  letin assembled ≝ (\fst (assembly program sigma policy))
     2236  letin costs ≝ (\snd (assembly program sigma policy))
     2237  lapply (assembly_ok program sigma policy assembled costs)
     2238  @pair_elim #labels #costs' #create_label_cost_map_refl
     2239  <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H
     2240  lapply (H ppc) -H
     2241  @pair_elim #pi' #newppc #fetch_pseudo_refl'
     2242  @pair_elim #len #assembled #assembly1_refl #H cases H
     2243  #encoding_check_assm #sigma_newppc_refl
     2244  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
     2245  >pi_refl' in assembly1_refl; #assembly1_refl
     2246  >lookup_labels_refl >lookup_datalabels_refl >assembly1_refl
     2247  <sigma_newppc_refl
     2248  generalize in match fetch_pseudo_refl';
     2249  whd in match (fetch_pseudo_instruction ??);
     2250  @pair_elim #lbl #instr #nth_refl normalize nodelta
     2251  #G destruct %
    22062252qed.
    22072253
Note: See TracChangeset for help on using the changeset viewer.