Changeset 2119 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 27, 2012, 12:09:25 PM (8 years ago)
Author:
sacerdot
Message:

load_code_memory moved to Fetch.ma and proved correct w.r.t. next
(fetching) using Russell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2111 r2119  
    11041104qed.
    11051105
    1106 definition load_code_memory ≝
    1107  fold_left_i … (
    1108    λi, mem, v.
    1109      insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    1110 
    1111 definition load ≝
    1112  λl,cm.
    1113  λstatus.
    1114    set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
    1115 
    11161106definition fetch_pseudo_instruction:
    11171107 ∀code_mem:list labelled_instruction. ∀pc:Word.
Note: See TracChangeset for help on using the changeset viewer.