Ignore:
Timestamp:
May 23, 2011, 6:12:51 PM (10 years ago)
Author:
mulligan
Message:

lots of refactoring, finally got something to prove

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r823 r825  
    22include "ASM/Interpret.ma".
    33
     4let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
     5                       (encoding: list Byte) on encoding: Prop ≝
     6  match encoding with
     7  [ nil ⇒ final_pc = pc
     8  | cons hd tl ⇒
     9    let 〈new_pc, byte〉 ≝ next code_memory pc in
     10      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
     11  ].
     12
     13definition invariant:
     14  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
     15  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
     16  λsigma.
     17  λpseudo_assembly_program.
     18  λcode_mem.
     19    ∀pc: Word.
     20      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
     21      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
     22      let address_of ≝ ? in
     23      let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
     24      let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
     25      let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
     26        encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
     27      cases not_implemented
     28qed.
Note: See TracChangeset for help on using the changeset viewer.