Changeset 921
 Timestamp:
 Jun 9, 2011, 3:21:27 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r919 r921 892 892 ∀pi,code_memory,len,assembled,instructions,pc. 893 893 let expansion ≝ jump_expansion ppc program in 894 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppcexpansion pi →895 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →894 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi → 895 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi → 896 896 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 897 897 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. 898 898 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc 899 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2; #EQ2a #EQ2b 899 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 900 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2; #EQ2a #EQ2b 900 901 >EQ2a >EQ2b EQ2a EQ2b; 901 902 generalize in match (pc + flatten … (map … assembly1 instructions)); #final_pc … … 908 909 >(eq_bv_to_eq … K2) @IH @H2 ] 909 910 qed. 910 911 911 912 912 (* This establishes the correspondence between pseudo program counters and … … 923 923 let 〈program_counter, sigma_map〉 ≝ pc_map in 924 924 let 〈label, i〉 ≝ i in 925 match construct_costs instr_list p rogram_counter (λx. zero ?) (λx. zero ?) (Stub …) i with925 match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with 926 926 [ None ⇒ None ? 927 927  Some pc_ignore ⇒ … … 1020 1020 1021 1021 axiom tech_pc_sigma0_append: 1022 ∀preamble,instr_list,prefix,label,i,pc',code,p c,costs,costs'.1022 ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'. 1023 1023 Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 → 1024 construct_costs 〈preamble,instr_list〉 … p c (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →1024 construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 1025 1025 tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉. 1026 1026 1027 1027 axiom tech_pc_sigma0_append_None: 1028 ∀preamble,instr_list,prefix,i,p c,costs.1028 ∀preamble,instr_list,prefix,i,ppc,pc,costs. 1029 1029 Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 → 1030 construct_costs 〈preamble,instr_list〉 … p c (λx.zero 16) (λx. zero 16) costs i = None …1030 construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 1031 1031 → False. 1032 1032 … … 1361 1361 ∀ppc,len,assembledi. 1362 1362 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1363 (* BUG HERE: WE SHOULD PASS BOTH ppc (FOR THE POLICY) AND (sigma program ppc) FOR THE OFFSETS *) 1364 Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → 1363 Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi → 1365 1364 encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧ 1366 1365 sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len). … … 1382 1381 let expansion ≝ jump_expansion ppc program in 1383 1382 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1384 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppcexpansion pi →1383 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi → 1385 1384 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 1386 1385 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions … … 1398 1397 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?) 1399 1398 #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?); 1400 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?) 1399 normalize nodelta in EXPAND; (* HERE *) 1400 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) H1; #H1 1401 >bitvector_of_nat_nat_of_bitvector in H1; #H1 1402 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?) 1401 1403 #H1 #H2 1402 1404 cases (H2 ?? (refl …)) H2; #K1 #K2 >K2 1403 generalize in match (H1 ??? (nat_of_bitvector … (sigma program ppc)) (refl …) (refl …) ?) H1; 1404 [ #K3 >bitvector_of_nat_nat_of_bitvector in K3; #R @R 1405  >bitvector_of_nat_nat_of_bitvector @K1 ] 1405 generalize in match (H1 ?? (refl …) (refl …) ?) H1; 1406 [ #K3 @K3  @K1 ] 1406 1407 qed. 1407 1408
Note: See TracChangeset
for help on using the changeset viewer.