 Timestamp:
 Jun 8, 2011, 5:53:18 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r902 r903 931 931 → False. 932 932 933 933 (* 934 934 definition build_maps' ≝ 935 935 λpseudo_program. … … 986 986 qed. 987 987 988 (*989 (*990 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"991 with precedence 10992 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.993 *)994 995 988 lemma build_maps_ok: 996 989 ∀p:pseudo_assembly_program. … … 1008 1001 *) 1009 1002 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.*) 1003 axiom 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 1016 lemma 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 1018 1025 1019 1026 lemma rev_preserves_length:
Note: See TracChangeset
for help on using the changeset viewer.