Changeset 1035 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 22, 2011, 11:06:43 PM (9 years ago)

Author:

sacerdot

Message:

Main theorem (broken because of dependent types) almost restored.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -1979 +1979 @@
           SFR_SP sp2)
         pbu)).
+
+theorem main_thm:
+ ∀M,M',ps,pol.
+  next_internal_pseudo_address_map M ps = Some … M' →
+   ∃n.
+      execute n (status_of_pseudo_status M ps pol)
+    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
+ [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
+ #M #M' #ps #pol #SAFE
+ cut
+  (∀ps'.
+    ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
+    ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
+ [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
+ #ps' #EQ
+ whd in ⊢ (??(λ_.??(??%)?))
+ change with
+  (∃n.
+    execute n
+     (set_low_internal_ram ?
+       (set_high_internal_ram ?
+         (set_program_counter ?
+           (set_code_memory ?? ps (load_code_memory ?))
+          (sigma ? pol (program_counter ? ps)))
+        (high_internal_ram_of_pseudo_high_internal_ram M ?))
+      (low_internal_ram_of_pseudo_low_internal_ram M ?))
+   = set_low_internal_ram ?
+      (set_high_internal_ram ?
+        (set_program_counter ?
+          (set_code_memory ?? ? (load_code_memory ?))
+         (sigma ???)) ?) ?)
+ >EQ whd in match eq_rect_Type0_r normalize nodelta
+ >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
+ generalize in match EQ -EQ;
+ generalize in match (refl … (code_memory pseudo_assembly_program ps))
+ generalize in match pol generalize in ⊢ (∀_.??%? → ?)
+ * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
+ 
+
 
 lemma main_thm0: