Changeset 985 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (8 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r936 r985  
    11include "ASM/Status.ma".
    22include "ASM/Fetch.ma".
    3 include "ASM/Assembly.ma".
    43
    54definition sign_extension: Byte → Word ≝
     
    1211qed.
    1312   
    14 lemma inclusive_disjunction_true:
    15   ∀b, c: bool.
    16     (orb b c) = true → b = true ∨ c = true.
    17   # b
    18   # c
    19   elim b
    20   [ normalize
    21     # H
    22     @ or_introl
    23     %
    24   | normalize
    25     /2/
    26   ]
    27 qed.
    28 
    29 lemma conjunction_true:
    30   ∀b, c: bool.
    31     andb b c = true → b = true ∧ c = true.
    32   # b
    33   # c
    34   elim b
    35   normalize
    36   [ /2/
    37   | # K
    38     destruct
    39   ]
    40 qed.
    41 
    42 lemma eq_true_false: false=true → False.
    43  # K
    44  destruct
    45 qed.
    46 
    4713lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
    4814 # a
     
    5420 # K
    5521 cases (eq_true_false K)
    56 qed.
    57 
    58 lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
    59  # b
    60  cases b
    61  %
    6222qed.
    6323
     
    691651     execute_1_0 s instr_pc_ticks.
    692652
    693 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    694   match l with
    695   [ nil ⇒ ?
    696   | cons hd tl ⇒
    697     if pred hd then
    698       acc
    699     else
    700       index_of_internal A pred tl (S acc)
    701   ].
    702   cases not_implemented.
    703 qed.
    704 
    705 definition index_of ≝
    706   λA.
    707   λeq.
    708   λl.
    709     index_of_internal A eq l 0.
    710 
    711 definition instruction_matches_identifier ≝
    712   λy: Identifier.
    713   λx: labelled_instruction.
    714     match \fst x with
    715     [ None ⇒ false
    716     | Some x ⇒ eq_bv ? x y
    717     ].
    718 
    719 definition address_of_word_labels_code_mem ≝
    720   λcode_mem.
    721   λid: Identifier.
    722     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
    723 
    724 definition address_of_word_labels ≝
    725   λps: PseudoStatus.
    726   λid: Identifier.
    727     address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    728 
    729653definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
    730654  λticks_of.
Note: See TracChangeset for help on using the changeset viewer.