Changeset 1941 for src/ASM/Fetch.ma


Ignore:
Timestamp:
May 14, 2012, 4:33:20 PM (8 years ago)
Author:
mulligan
Message:

Changes to the AssemblyProof? with a few more (large) axioms closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1642 r1941  
    1010definition code_memory_size ≝ bitvector_max_nat 16.
    1111
     12definition add ≝
     13  λn: nat.
     14  λl, r: BitVector n.
     15    \snd (half_add n l r).
     16
     17axiom add_zero:
     18  ∀n: nat.
     19  ∀l: BitVector n.
     20    l = add n l (zero …).
     21
     22axiom add_associative:
     23  ∀n: nat.
     24  ∀l, c, r: BitVector n.
     25    add … l (add … c r) = add … (add … l c) r.
     26
     27include alias "ASM/BitVectorTrie.ma".
     28
    1229definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
    1330  λpmem: BitVectorTrie Byte 16.
    1431  λpc: Word.
    15     〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
     32    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    1633
    1734lemma Prod_inv_rect_Type0:
Note: See TracChangeset for help on using the changeset viewer.