Changeset 971 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 16, 2011, 12:07:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r959 r971 924 924 program counters. It is at the heart of the proof. *) 925 925 (*CSC: code taken from build_maps *) 926 definition sigma0 : pseudo_assembly_program→ option (nat × (nat × (BitVectorTrie Word 16))) ≝927 λinstr_list. 926 definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 927 λinstr_list.λl:list labelled_instruction. 928 928 foldl ?? 929 (λt. λi.929 (λt,i. 930 930 match t with 931 931 [ None ⇒ None ? … … 939 939 let 〈pc,ignore〉 ≝ pc_ignore in 940 940 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ] 941 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list). 942 943 definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝ 944 λinstr_list. 945 match sigma0 instr_list with 941 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l. 942 943 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) 944 ≝ λprog.sigma00 prog (\snd prog). 945 946 definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝ 947 λprogram,instr_list. 948 match sigma00 program instr_list with 946 949 [ None ⇒ None … 947 950  Some result ⇒ 948 951 let 〈ppc,pc_sigma_map〉 ≝ result in 949 Some … pc_sigma_map ]. 952 let 〈pc,map〉 ≝ pc_sigma_map in 953 Some … 〈ppc,pc〉 ]. 950 954 951 955 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝ … … 992 996 qed. 993 997 998 lemma does_not_occur_Some: 999 ∀id,id',i,list_instr. 1000 eq_bv ? id' id = false → 1001 does_not_occur id (list_instr@[〈Some ? id',i〉]) = 1002 does_not_occur id list_instr. 1003 #id #id' #i #list_instr elim list_instr 1004 [ #H normalize in H ⊢ %; >H % 1005  * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %] 1006 qed. 1007 994 1008 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝ 995 1009 match l with … … 1030 1044 qed. 1031 1045 1032 axiom tech_pc_sigma0_append: 1033 ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'. 1034 Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 → 1035 construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 1036 tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉. 1037 1038 axiom tech_pc_sigma0_append_None: 1039 ∀preamble,instr_list,prefix,i,ppc,pc,costs. 1040 Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 → 1041 construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 1046 lemma occurs_exactly_once_Some: 1047 ∀id,id',i,prefix. 1048 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix. 1049 #id #id' #i #prefix elim prefix 1050 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 1051 change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/ 1052  *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 1053 cases he; normalize nodelta 1054 [ #H @ (IH H) 1055  #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??) 1056 change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv 16 x id) normalize nodelta; 1057 [ #H  #H @IH @H] 1058 qed. 1059 1060 axiom tech_pc_sigma00_append_Some: 1061 ∀program,prefix,costs,label,i,pc',code,ppc,pc. 1062 tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 → 1063 construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 1064 tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉. 1065 1066 axiom tech_pc_sigma00_append_None: 1067 ∀program,prefix,i,ppc,pc,costs. 1068 tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 → 1069 construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 1042 1070 → False. 1043 1071 1044 (*1045 1072 definition build_maps' ≝ 1046 1073 λpseudo_program. 1047 let 〈preamble,instr_list〉 ≝ pseudo_program in1048 1074 let result ≝ 1049 1075 foldl_strong 1050 1076 (option Identifier × pseudo_instruction) 1051 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 1052 let pre' ≝ 〈preamble,pre〉 in 1053 let 〈labels,pc_costs〉 ≝ res in 1054 tech_pc_sigma0 pre' = Some … pc_costs ∧ 1077 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))). 1078 let 〈labels,ppc_pc_costs〉 ≝ res in 1079 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 1080 let 〈pc',costs〉 ≝ pc_costs in 1081 tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧ 1055 1082 ∀id. occurs_exactly_once id pre → 1056 lookup ?? id labels (zero …) = sigma p re'(address_of_word_labels_code_mem pre id))1057 instr_list1083 lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id)) 1084 (\snd pseudo_program) 1058 1085 (λprefix,i,tl,prf,t. 1059 let 〈labels, pc_costs〉 ≝ t in 1060 let 〈program_counter, costs〉 ≝ pc_costs in 1086 let 〈labels, ppc_pc_costs〉 ≝ t in 1087 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in 1088 let 〈pc,costs〉 ≝ pc_costs in 1061 1089 let 〈label, i'〉 ≝ i in 1062 1090 let labels ≝ … … 1064 1092 [ None ⇒ labels 1065 1093  Some label ⇒ 1066 let program_counter_bv ≝ bitvector_of_nat ? p rogram_counterin1094 let program_counter_bv ≝ bitvector_of_nat ? pc in 1067 1095 insert ? ? label program_counter_bv labels 1068 1096 ] 1069 1097 in 1070 match construct_costs 〈preamble,instr_list〉 program_counter(λx. zero ?) (λx. zero ?) costs i' with1098 match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with 1071 1099 [ None ⇒ 1072 let dummy ≝ 〈labels,p c_costs〉 in1100 let dummy ≝ 〈labels,ppc_pc_costs〉 in 1073 1101 dummy 1074  Some construct ⇒ 〈labels, construct〉1102  Some construct ⇒ 〈labels, 〈S ppc,construct〉〉 1075 1103 ] 1076 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉1104 ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉 1077 1105 in 1078 let 〈labels, pc_costs〉 ≝ result in 1106 let 〈labels, ppc_pc_costs〉 ≝ result in 1107 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in 1079 1108 let 〈pc, costs〉 ≝ pc_costs in 1080 1109 〈labels, costs〉. 1081 1110 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ // 1082  whd cases construct in p3 #PC #CODE #JMEQ % 1083 [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ))  #id #Hid ] 1084  (* dummy case *) @⊥ 1085 @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ] 1086 [*: generalize in match (sig2 … t) whd in ⊢ (% → ?) 1087 >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ] 1088 whd in ⊢ (??(????%?)?) labels1; 1089 cases label in Hid 1090 [ #Hid whd in ⊢ (??(????%?)?) >IH1 IH1 1091 [ >(address_of_word_labels_code_mem_None … Hid) 1092 (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *) 1093  whd in Hid >occurs_exactly_once_None in Hid // ] 1094  label #label #Hid whd in ⊢ (??(????%?)?) 1095 1096 ] 1111  whd generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 1112 cases construct in p4 #PC #CODE #JMEQ % 1113 [ @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ)) 1114  #id normalize nodelta; labels1; cases label; normalize nodelta 1115 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 // 1116  #l 1117 ]] 1118  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 1119 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ] 1097 1120 qed. 1098 1121
Note: See TracChangeset
for help on using the changeset viewer.