Changeset 1667 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jan 29, 2012, 10:25:57 PM (8 years ago)
Author:
sacerdot
Message:

Main lemma for the main_thm of AssemblyProof? re-declared as an axiom in
Assembly.ma. However, we need to understand again the role of lookup_labels.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1649 r1667  
    619619  let pc_len ≝ length ? flattened in
    620620   〈pc_len, flattened〉.
    621  
     621
    622622definition construct_costs ≝
    623623  λprogram_counter: nat.
     
    701701 cases abs /2/
    702702qed.
     703
     704(*CSC: Main axiom here, needs to be proved soon! *)
     705axiom snd_assembly_1_pseudoinstruction_ok:
     706 ∀program:pseudo_assembly_program.∀pol: policy program.
     707 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
     708  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     709  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     710  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     711   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
     712    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     713     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    703714
    704715example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
Note: See TracChangeset for help on using the changeset viewer.