Changeset 2132 for src/ASM

Timestamp:

Jun 28, 2012, 10:41:59 AM (8 years ago)

Author:

sacerdot

Message:

Two more daemons closed, one left.

File:

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

src/ASM/AssemblyProof.ma

@@ -180 +180 @@
     ].
 
+lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
+ ∀lookup_labels,sigma,policy,ppc,pi.
+  ∀lookup_datalabels1,lookup_datalabels2.
+   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) =
+   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
+#lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
+cases pi //
+qed.
+
+lemma fst_snd_assembly_1_pseudoinstruction:
+ ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled.
+   assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi
+   = 〈len,assembled〉 →
+    len = |assembled|.
+#lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled
+inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'
+whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
+qed.
+
 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)      
 lemma assembly_ok:
@@ -224 +243 @@
       #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
       >eq_fetch_pseudo_instruction whd in match instruction_size;
-      normalize nodelta (*CSC: TRUE, NEEDS LEMMA *)
-      cases daemon
+      normalize nodelta >create_label_cost_refl
+      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
+      [>eq_assembly_1_pseudoinstruction % | skip]
   | lapply (load_code_memory_ok assembled' ?) [ assumption ]
     #load_code_memory_ok
-    cut (len=|assembled|)
-    [1: (*CSC: provable before cleaning *)
-        cases daemon
-    ]
-    #EQlen
+    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
     (* Nice statement here *)
     cut (∀j. ∀H: j < |assembled|.