Ignore:
Timestamp:
Jun 9, 2011, 5:06:26 PM (9 years ago)
Author:
sacerdot
Message:

Main theorem false because of ticks :-(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r925 r926  
    16071607  status_of_pseudo_status ps = Some … s →
    16081608  status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' →
    1609    execute_1 s = s''.
     1609   ∃n. execute n s = s''.
    16101610 #ticks_of #ps #s #s''
    16111611 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
     
    16261626 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
    16271627 change with
    1628   (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
     1628  (∃n.
     1629    execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
    16291630   = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)
    16301631 whd in match (\snd 〈preamble,instr_list〉) in H;
     
    16351636 (* NICE STATEMENT HERE *)
    16361637 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
     1638 #K <K generalize in match K; -K;
     1639 (* STATEMENT WITH EQUALITY HERE *)
    16371640 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta;
    16381641 cases (fetch_pseudo_instruction instr_list (program_counter … ps))
    1639  #pi #newppc normalize nodelta; * #instructions *
     1642 #pi #newppc normalize nodelta; * #instructions *;
    16401643 cases pi normalize nodelta;
    16411644  [ (* Instruction *)
    1642   | (* Comment *) #comment #H1 #H2 #EQ normalize in H1 generalize in match (option_destruct_Some ??? H1) #K1
    1643     >K1 in H2 whd in ⊢ (% → ?) #H2 whd in ⊢ (??%?)
     1645  | (* Comment *) #comment #H1 #H2 #EQ %[@0] >EQ
     1646    whd in ⊢ (???(???(??%)))
     1647    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1
     1648    >K1 in H2; whd in ⊢ (% → ?) #H2 <(eq_bv_to_eq … H2)
     1649   
    16441650  | (* Cost *)
    16451651  | (* Jmp *)
Note: See TracChangeset for help on using the changeset viewer.