Changeset 926 for src

Timestamp:

Jun 9, 2011, 5:06:26 PM (10 years ago)

Author:

sacerdot

Message:

Main theorem false because of ticks :-(

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -1607 +1607 @@
   status_of_pseudo_status ps = Some … s →
   status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' →
-   execute_1 s = s''.
+   ∃n. execute n s = s''.
  #ticks_of #ps #s #s''
  generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
@@ -1626 +1626 @@
  #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
  change with
-  (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
+  (∃n.
+    execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
    = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)
  whd in match (\snd 〈preamble,instr_list〉) in H;
@@ -1635 +1636 @@
  (* NICE STATEMENT HERE *)
  generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
+ #K <K generalize in match K; -K;
+ (* STATEMENT WITH EQUALITY HERE *)
  whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta;
  cases (fetch_pseudo_instruction instr_list (program_counter … ps))
- #pi #newppc normalize nodelta; * #instructions *
+ #pi #newppc normalize nodelta; * #instructions *;
  cases pi normalize nodelta;
   [ (* Instruction *)
-  | (* Comment *) #comment #H1 #H2 #EQ normalize in H1 generalize in match (option_destruct_Some ??? H1) #K1
-    >K1 in H2 whd in ⊢ (% → ?) #H2 whd in ⊢ (??%?)
+  | (* Comment *) #comment #H1 #H2 #EQ %[@0] >EQ
+    whd in ⊢ (???(???(??%)))
+    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1
+    >K1 in H2; whd in ⊢ (% → ?) #H2 <(eq_bv_to_eq … H2)
+    
   | (* Cost *)
   | (* Jmp *)