Changeset 2757 for src/ASM/Status.ma


Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2754 r2757  
    10281028qed.
    10291029
    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.
     1030definition construct_datalabels: list (Identifier × Word) → ? ≝
     1031  λthe_preamble.
    10851032    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
    10861033    λt. λpreamble.
     
    10891036      let 〈carry, sum〉 ≝ half_add … addr size in
    10901037        〈add ? ? datalabels name addr, sum〉)
    1091           〈empty_map …, zero 16〉 (\fst the_preamble)).
     1038          〈empty_map …, zero 16〉 (the_preamble)).
Note: See TracChangeset for help on using the changeset viewer.