Changeset 2055 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 13, 2012, 12:11:21 PM (8 years ago)
Author:
sacerdot
Message:

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2032 r2055  
    11141114   set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
    11151115
    1116 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
     1116definition fetch_pseudo_instruction:
     1117 ∀code_mem:list labelled_instruction. ∀pc:Word.
     1118  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
    11171119  λcode_mem.
    11181120  λpc: Word.
    1119     let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    1120     let new_pc ≝ add ? pc (bitvector_of_nat ? 1) in
     1121  λpc_ok.
     1122    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
     1123    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
    11211124      〈instr, new_pc〉.
    1122     cases not_implemented.
    1123 qed.
    11241125
    11251126lemma snd_fetch_pseudo_instruction:
    1126  ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = add ? ppc (bitvector_of_nat ? 1).
    1127  #l #ppc whd in ⊢ (??(???%)?); @pair_elim
     1127 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
     1128 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
    11281129 #lft #rgt #_ %
    11291130qed.
Note: See TracChangeset for help on using the changeset viewer.