Changeset 2264 for src/ASM/Status.ma


Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (8 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2247 r2264  
    11011101        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    11021102
    1103 definition address_of_word_labels_code_mem ≝
    1104   λcode_mem : list labelled_instruction.
    1105   λid: Identifier.
    1106     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
    1107 
    1108 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1109  occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
    1110   address_of_word_labels_code_mem instr_list id =
    1111   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    1112  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1113  >(index_of_internal_None ?????? H) %
    1114 qed.
    1115 
    1116 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1117  eq_identifier ? id' id = false →
    1118   occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
    1119    address_of_word_labels_code_mem instr_list id =
    1120    address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    1121  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1122  >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
    1123 qed.
    1124 
    1125 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
    1126   occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
    1127    address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    1128    = bitvector_of_nat … (|instr_list|).
    1129  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
    1130  >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
    1131 qed.
    1132 
    1133 definition address_of_word_labels ≝
    1134   λpr: pseudo_assembly_program.
    1135   λid: Identifier.
    1136     address_of_word_labels_code_mem (\snd pr) id.
    1137 
    11381103definition construct_datalabels: preamble → ? ≝
    11391104  λthe_preamble: preamble.
Note: See TracChangeset for help on using the changeset viewer.