Ignore:
Timestamp:
Jun 8, 2011, 5:53:18 PM (9 years ago)
Author:
sacerdot
Message:

Statement of new main lemma (as axiom).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r902 r903  
    931931    → False.
    932932
    933 
     933(*
    934934definition build_maps' ≝
    935935  λpseudo_program.
     
    986986qed.
    987987
    988 (*
    989 (*
    990 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    991  with precedence 10
    992 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    993 *)
    994 
    995988lemma build_maps_ok:
    996989 ∀p:pseudo_assembly_program.
     
    10081001*)
    10091002
    1010 (*
    1011 lemma list_elim_rev:
    1012  ∀A:Type[0].∀P:list A → Prop.
    1013   P [ ] → (∀n,l. length l = n → P l → 
    1014   P [ ] → (∀l,a. P l → P (l@[a])) →
    1015    ∀l. P l.
    1016  #A #P
    1017 qed.*)
     1003axiom assembly_ok:
     1004 ∀program,assembled,costs,labels,datalabels.
     1005  Some … 〈labels,datalabels〉 = build_maps program →
     1006  Some … 〈assembled,costs〉 = assembly program →
     1007  let code_memory ≝ load_code_memory assembled in
     1008  let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
     1009  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
     1010   ∀ppc,len,assembledi.
     1011    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1012     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     1013      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
     1014       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
     1015
     1016lemma fetch_assembly_pseudo:
     1017 ∀program,ppc,lookup_labels,lookup_datalabels.
     1018  ∀pi,code_memory,len,assembled,instructions,pc.
     1019   let expansion ≝ jump_expansion_policy program ppc in
     1020   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
     1021    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     1022     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
     1023      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
     1024
    10181025
    10191026lemma rev_preserves_length:
Note: See TracChangeset for help on using the changeset viewer.