Changeset 829


Ignore:
Timestamp:
May 24, 2011, 2:06:01 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r828 r829  
    7979           (clock … ps)) ].
    8080
     81
     82lemma execute_code_memory_unchanged:
     83 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
     84 #ticks #ps whd in ⊢ (??? (??%))
     85 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
     86  (program_counter pseudo_assembly_program ps)) #instr #pc
     87 whd in ⊢ (??? (??%)) cases instr
     88  [ #pre cases pre
     89     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
     90       cases (split ????) #z1 #z2 %
     91     | *: cases not_implemented
     92     ]
     93  | #comment %
     94  | #cost %
     95  | #label %
     96  | #label (* CSC: ??? *)
     97  | #dptr #label (* CSC: ??? *)
     98  ]
     99  cases not_implemented
     100qed.
     101
    81102lemma foo:
    82103 ∀ticks_of.
    83104 ∀ps: PseudoStatus.
     105  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
    84106  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
    85107  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
    86   match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
    87108  let s' ≝ execute_1 s in
    88109   s = s'']].
     110 #ticks_of #ps
     111 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     112 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
     113 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     114 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracChangeset for help on using the changeset viewer.