Changeset 828


Ignore:
Timestamp:
May 24, 2011, 1:32:07 PM (8 years ago)
Author:
sacerdot
Message:

Proof statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r827 r828  
    5656qed.
    5757
     58axiom sigma: pseudo_assembly_program → Word → Word.
     59
    5860definition status_of_pseudo_status: PseudoStatus → option Status ≝
    5961 λps.
    60   match assembly (code_memory ? ps) with
    61    [ None ⇒ None …
    62    | Some p ⇒
    63       let cm ≝ load_code_memory (\fst p) in
    64       let pc ≝ ? in
    65        Some …
    66         (mk_PreStatus (BitVectorTrie Byte 16)
    67           cm
    68           (low_internal_ram … ps)
    69           (high_internal_ram … ps)
    70           (external_ram … ps)
    71           pc
    72           (special_function_registers_8051 … ps)
    73           (special_function_registers_8052 … ps)
    74           (p1_latch … ps)
    75           (p3_latch … ps)
    76           (clock … ps)) ].
     62  let pap ≝ code_memory … ps in
     63   match assembly pap with
     64    [ None ⇒ None …
     65    | Some p ⇒
     66       let cm ≝ load_code_memory (\fst p) in
     67       let pc ≝ sigma pap (program_counter ? ps) in
     68        Some …
     69         (mk_PreStatus (BitVectorTrie Byte 16)
     70           cm
     71           (low_internal_ram … ps)
     72           (high_internal_ram … ps)
     73           (external_ram … ps)
     74           pc
     75           (special_function_registers_8051 … ps)
     76           (special_function_registers_8052 … ps)
     77           (p1_latch … ps)
     78           (p3_latch … ps)
     79           (clock … ps)) ].
    7780
    7881lemma foo:
     
    8083 ∀ps: PseudoStatus.
    8184  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
    82   let s'' ≝ status_of_pseudo_status ps' in
    83   let s ≝ status_of_pseudo_status ps in
     85  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
     86  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
    8487  let s' ≝ execute_1 s in
    85    s = s''.
     88   s = s'']].
Note: See TracChangeset for help on using the changeset viewer.