Changeset 826


Ignore:
Timestamp:
May 23, 2011, 6:39:41 PM (8 years ago)
Author:
mulligan
Message:

start of proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r825 r826  
    1111  ].
    1212
    13 definition invariant:
     13definition assembly_specification:
    1414  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
    1515  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
     
    2727      cases not_implemented
    2828qed.
     29
     30theorem assembly_meets_specification:
     31  ∀pseudo_assembly_program.
     32    match assembly pseudo_assembly_program with
     33    [ None ⇒ True
     34    | Some code_mem_cost ⇒
     35      let 〈code_mem, cost〉 ≝ code_mem_cost in
     36        assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
     37    ].
     38  # PROGRAM
     39  [ cases PROGRAM
     40    # PREAMBLE
     41    # INSTR_LIST
     42    elim INSTR_LIST
     43    [ whd
     44      whd in ⊢ (∀_. %)
     45      # PC
     46      whd
     47    | # INSTR
     48      # INSTR_LIST_TL
     49      # H
     50      whd
     51      normalize
     52    ]
     53  | cases not_implemented
     54  ]
Note: See TracChangeset for help on using the changeset viewer.