Changeset 2757 for src/ASM/Status.ma
 Timestamp:
 Mar 1, 2013, 7:13:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r2754 r2757 1028 1028 qed. 1029 1029 1030 definition fetch_pseudo_instruction: 1031 ∀code_mem:list labelled_instruction. ∀pc:Word. 1032 nat_of_bitvector … pc < code_mem → (pseudo_instruction × Word) ≝ 1033 λcode_mem. 1034 λpc: Word. 1035 λpc_ok. 1036 let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in 1037 let new_pc ≝ add ? pc (bitvector_of_nat … 1) in 1038 〈instr, new_pc〉. 1039 1040 lemma snd_fetch_pseudo_instruction: 1041 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1). 1042 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim 1043 #lft #rgt #_ % 1044 qed. 1045 1046 lemma fetch_pseudo_instruction_vsplit: 1047 ∀instr_list,ppc,ppc_ok. 1048 ∃pre,suff,lbl. 1049 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list. 1050 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???); 1051 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff} 1052 lapply EQ EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta 1053 #EQ %{lbl0} @EQ 1054 qed. 1055 1056 lemma fetch_pseudo_instruction_append: 1057 ∀l1,l2. l1@l2 ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'. 1058 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in 1059 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) ppc_ok' = 1060 〈\fst code_newppc, add … (bitvector_of_nat … (l1)) (\snd code_newppc)〉. 1061 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 1062 cut (l1 + nat_of_bitvector … ppc < 2^16) 1063 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ] 1064 l1l2_ok #l1ppc_ok >nat_of_bitvector_add 1065 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 1066 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 1067 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???) 1068 #lbl #instr normalize nodelta >add_associative % 1069 qed. 1070 1071 definition is_well_labelled_p ≝ 1072 λinstr_list. 1073 ∀id: Identifier. 1074 ∀ppc. 1075 ∀ppc_ok. 1076 ∀i. 1077 \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i → 1078 (instruction_has_label id i → 1079 occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧ 1080 (is_jump_to i id → 1081 occurs_exactly_once ASMTag pseudo_instruction id instr_list). 1082 1083 definition construct_datalabels: preamble → ? ≝ 1084 λthe_preamble: preamble. 1030 definition construct_datalabels: list (Identifier × Word) → ? ≝ 1031 λthe_preamble. 1085 1032 \fst (foldl ((identifier_map ASMTag Word) × Word) ? ( 1086 1033 λt. λpreamble. … … 1089 1036 let 〈carry, sum〉 ≝ half_add … addr size in 1090 1037 〈add ? ? datalabels name addr, sum〉) 1091 〈empty_map …, zero 16〉 ( \fstthe_preamble)).1038 〈empty_map …, zero 16〉 (the_preamble)).
Note: See TracChangeset
for help on using the changeset viewer.