Ignore:
Timestamp:
Jun 9, 2011, 1:27:57 AM (9 years ago)
Author:
sacerdot
Message:

Back to the main theorem.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r908 r909  
    14491449    | Some p ⇒
    14501450       let cm ≝ load_code_memory (\fst p) in
    1451        let pc ≝ sigma' pap (program_counter ? ps) in
     1451       let pc ≝ sigma pap (program_counter ? ps) in
    14521452        Some …
    14531453         (mk_PreStatus (BitVectorTrie Byte 16)
     
    14631463           (clock … ps)) ].
    14641464
     1465(*
    14651466definition write_at_stack_pointer':
    14661467 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
     
    15211522 cases not_implemented
    15221523qed.
    1523 
     1524*)
    15241525(*
    15251526lemma execute_code_memory_unchanged:
     
    15611562    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
    15621563    ].
    1563  #ps #ps' #H whd in ⊢ (mat
    1564  ch % with [ _ ⇒ ? | _ ⇒ ? ])
     1564 #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    15651565 generalize in match (refl … (assembly (code_memory … ps)))
    15661566 cases (assembly ?) in ⊢ (???% → %)
    15671567  [ #K whd whd in ⊢ (??%?) <H >K %
    15681568  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
    1569 qed.*)
    1570 
    1571 let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
    1572   match encoding with
    1573   [ nil ⇒ True
    1574   | cons hd tl ⇒
    1575     let 〈new_pc, byte〉 ≝ next code_memory pc in
    1576       hd = byte ∧ encoding_check' code_memory new_pc tl
    1577   ].
    1578  
     1569qed.
     1570
    15791571lemma main_thm:
    15801572 ∀ticks_of.
Note: See TracChangeset for help on using the changeset viewer.