Ignore:
Timestamp:
Jun 8, 2011, 6:12:15 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r905 r906  
    828828qed.
    829829
    830 axiom  eq_bv_refl: ∀n,v. eq_bv n v v = true.
    831 
    832830axiom bitvector_3_elim_prop:
    833831 ∀P: BitVector 3 → Prop.
     
    11031101*)
    11041102
    1105 axiom assembly_ok:
    1106  ∀program,assembled,costs,labels,datalabels.
    1107   Some … 〈labels,datalabels〉 = build_maps program →
    1108   Some … 〈assembled,costs〉 = assembly program →
    1109   let code_memory ≝ load_code_memory assembled in
    1110   let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
    1111   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    1112    ∀ppc,len,assembledi.
    1113     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1114      Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
    1115       encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
    1116        sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
    1117 
     1103(*
    11181104lemma rev_preserves_length:
    11191105 ∀A.∀l. length … (rev A l) = length … l.
     
    13621348 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
    13631349 |   
    1364 
     1350*)
     1351
     1352axiom assembly_ok:
     1353 ∀program,assembled,costs,labels,datalabels.
     1354  Some … 〈labels,datalabels〉 = build_maps program →
     1355  Some … 〈assembled,costs〉 = assembly program →
     1356  let code_memory ≝ load_code_memory assembled in
     1357  let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
     1358  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
     1359   ∀ppc,len,assembledi.
     1360    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1361    (* BUG HERE: WE SHOULD PASS BOTH ppc (FOR THE POLICY) AND (sigma program ppc) FOR THE OFFSETS *)
     1362     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     1363      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
     1364       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
     1365
     1366(* OLD?
    13651367definition assembly_specification:
    13661368  ∀assembly_program: pseudo_assembly_program.
     
    14071409  | cases not_implemented
    14081410  ] *)
     1411*)
    14091412
    14101413definition status_of_pseudo_status: PseudoStatus → option Status ≝
Note: See TracChangeset for help on using the changeset viewer.