Changeset 2157 for src/ASM

Timestamp:

Jul 6, 2012, 11:34:09 AM (8 years ago)

Author:

sacerdot

Message:

Anticipating a proof needed before.

Location:

src/ASM

Files:

• Assembly.ma (modified) (1 diff)
• AssemblyProof.ma (modified) (1 diff)

src/ASM/Assembly.ma

@@ -731 +731 @@
 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
 qed.
+
+(* XXX: easy but tedious *)
+lemma assembly1_lt_128:
+  ∀i: instruction.
+    |(assembly1 i)| < 128.
+  cases daemon
+(* XXX: commented out as takes ages to type check 
+  #i cases i
+  try (#assm1 #assm2) try #assm1
+  [8:
+    cases assm1
+    try (#assm1 #assm2) try #assm1
+    whd in match assembly1; normalize nodelta
+    whd in match assembly_preinstruction; normalize nodelta
+    try @(subaddressing_mode_elim … assm2)
+    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
+    [32:
+      cases assm1 -assm1 #assm1 normalize nodelta
+      cases assm1 #addr1 #addr2 normalize nodelta
+      [1:
+        @(subaddressing_mode_elim … addr2)
+      |2:
+        @(subaddressing_mode_elim … addr1)
+      ]
+      #w
+    |35,36,37:
+      cases assm1 -assm1 #assm1 normalize nodelta
+      [1,3:
+        cases assm1 -assm1 #assm1 normalize nodelta
+      ]
+      cases assm1 #addr1 #addr2 normalize nodelta
+      @(subaddressing_mode_elim … addr2) try #w
+    |49:
+      cases assm1 -assm1 #assm1 normalize nodelta
+      [1:
+        cases assm1 -assm1 #assm1 normalize nodelta
+        [1:
+          cases assm1 -assm1 #assm1 normalize nodelta
+          [1:
+            cases assm1 -assm1 #assm1 normalize nodelta
+            [1:
+              cases assm1 -assm1 #assm1 normalize nodelta
+            ]
+          ]
+        ]
+      ]
+      cases assm1 #addr1 #addr2 normalize nodelta
+      [1,3,4,5:
+        @(subaddressing_mode_elim … addr2) try #w
+      |*:
+        @(subaddressing_mode_elim … addr1) try #w
+        normalize nodelta
+        [1,2:
+          @(subaddressing_mode_elim … addr2) try #w
+        ]
+      ]
+    |50:
+      cases assm1 -assm1 #assm1 normalize nodelta
+      cases assm1 #addr1 #addr2 normalize nodelta
+      [1:
+        @(subaddressing_mode_elim … addr2) try #w
+      |2:
+        @(subaddressing_mode_elim … addr1) try #w
+      ]
+    ]
+    normalize repeat @le_S_S @le_O_n
+  ]
+  whd in match assembly1; normalize nodelta
+  [6:
+    normalize repeat @le_S_S @le_O_n
+  |7:
+    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
+  |*:
+    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
+  ]
+  *)
+qed.
+
+lemma assembly1_pseudoinstruction_lt_2_to_16:
+  ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
+  |\snd (assembly_1_pseudoinstruction
+    lookup_labels sigma policy ppc lookup_datalabels pi)|
+   < 2^16.
+ #lookup_labels #sigma #policy #ppc #lookup_datalabels *
+[ cut (128 < 2^16) [@leb_true_to_le %] #LT
+  * whd in match (assembly_1_pseudoinstruction ??????);
+  whd in match (expand_pseudo_instruction ??????);
+  whd in match assembly_1_pseudoinstruction; normalize nodelta
+  try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1
+  whd in match (expand_pseudo_instruction ??????);
+  try
+   (change with (|flatten ? [assembly1 ?]| < ?)
+    >flatten_singleton
+    @(transitive_lt … (assembly1_lt_128 ?))
+    @LT)
+  @pair_elim #x #y #_ cases x normalize nodelta
+  try
+   (change with (|flatten ? [assembly1 ?]| < ?)
+    >flatten_singleton
+    @(transitive_lt … (assembly1_lt_128 ?))
+    @LT)
+  change with (|flatten ? [assembly1 ?; assembly1 ?; assembly1 ?]| < ?)
+  >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O
+  <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))
+  try @assembly1_lt_128 @leb_true_to_le %
+|2,3: #msg normalize in ⊢ (?%?); //
+| #label whd in match (assembly_1_pseudoinstruction ??????);
+  whd in match (expand_pseudo_instruction ??????);
+  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
+  [2: @pair_elim #x #y #_ cases (?∧?)]
+  normalize in ⊢ (?%?); //
+| #label whd in match (assembly_1_pseudoinstruction ??????);
+  whd in match (expand_pseudo_instruction ??????);
+  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
+  normalize in ⊢ (?%?); //
+| #dptr #id normalize in ⊢ (?%?); //
+]
+qed.
+
+
 
 definition assembly:

src/ASM/AssemblyProof.ma

@@ -179 +179 @@
     | _ ⇒ True
     ].
-
-(* XXX: easy but tedious *)
-lemma assembly1_lt_128:
-  ∀i: instruction.
-    |(assembly1 i)| < 128.
-  cases daemon
-(* XXX: commented out as takes ages to type check 
-  #i cases i
-  try (#assm1 #assm2) try #assm1
-  [8:
-    cases assm1
-    try (#assm1 #assm2) try #assm1
-    whd in match assembly1; normalize nodelta
-    whd in match assembly_preinstruction; normalize nodelta
-    try @(subaddressing_mode_elim … assm2)
-    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
-    [32:
-      cases assm1 -assm1 #assm1 normalize nodelta
-      cases assm1 #addr1 #addr2 normalize nodelta
-      [1:
-        @(subaddressing_mode_elim … addr2)
-      |2:
-        @(subaddressing_mode_elim … addr1)
-      ]
-      #w
-    |35,36,37:
-      cases assm1 -assm1 #assm1 normalize nodelta
-      [1,3:
-        cases assm1 -assm1 #assm1 normalize nodelta
-      ]
-      cases assm1 #addr1 #addr2 normalize nodelta
-      @(subaddressing_mode_elim … addr2) try #w
-    |49:
-      cases assm1 -assm1 #assm1 normalize nodelta
-      [1:
-        cases assm1 -assm1 #assm1 normalize nodelta
-        [1:
-          cases assm1 -assm1 #assm1 normalize nodelta
-          [1:
-            cases assm1 -assm1 #assm1 normalize nodelta
-            [1:
-              cases assm1 -assm1 #assm1 normalize nodelta
-            ]
-          ]
-        ]
-      ]
-      cases assm1 #addr1 #addr2 normalize nodelta
-      [1,3,4,5:
-        @(subaddressing_mode_elim … addr2) try #w
-      |*:
-        @(subaddressing_mode_elim … addr1) try #w
-        normalize nodelta
-        [1,2:
-          @(subaddressing_mode_elim … addr2) try #w
-        ]
-      ]
-    |50:
-      cases assm1 -assm1 #assm1 normalize nodelta
-      cases assm1 #addr1 #addr2 normalize nodelta
-      [1:
-        @(subaddressing_mode_elim … addr2) try #w
-      |2:
-        @(subaddressing_mode_elim … addr1) try #w
-      ]
-    ]
-    normalize repeat @le_S_S @le_O_n
-  ]
-  whd in match assembly1; normalize nodelta
-  [6:
-    normalize repeat @le_S_S @le_O_n
-  |7:
-    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
-  |*:
-    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
-  ]
-  *)
-qed.
-
-lemma assembly1_pseudoinstruction_lt_2_to_16:
-  ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
-  |\snd (assembly_1_pseudoinstruction
-    lookup_labels sigma policy ppc lookup_datalabels pi)|
-   < 2^16.
- #lookup_labels #sigma #policy #ppc #lookup_datalabels *
-[ cut (128 < 2^16) [@leb_true_to_le %] #LT
-  * whd in match (assembly_1_pseudoinstruction ??????);
-  whd in match (expand_pseudo_instruction ??????);
-  whd in match assembly_1_pseudoinstruction; normalize nodelta
-  try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1
-  whd in match (expand_pseudo_instruction ??????);
-  try
-   (change with (|flatten ? [assembly1 ?]| < ?)
-    >flatten_singleton
-    @(transitive_lt … (assembly1_lt_128 ?))
-    @LT)
-  @pair_elim #x #y #_ cases x normalize nodelta
-  try
-   (change with (|flatten ? [assembly1 ?]| < ?)
-    >flatten_singleton
-    @(transitive_lt … (assembly1_lt_128 ?))
-    @LT)
-  change with (|flatten ? [assembly1 ?; assembly1 ?; assembly1 ?]| < ?)
-  >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O
-  <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))
-  try @assembly1_lt_128 @leb_true_to_le %
-|2,3: #msg normalize in ⊢ (?%?); //
-| #label whd in match (assembly_1_pseudoinstruction ??????);
-  whd in match (expand_pseudo_instruction ??????);
-  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
-  [2: @pair_elim #x #y #_ cases (?∧?)]
-  normalize in ⊢ (?%?); //
-| #label whd in match (assembly_1_pseudoinstruction ??????);
-  whd in match (expand_pseudo_instruction ??????);
-  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
-  normalize in ⊢ (?%?); //
-| #dptr #id normalize in ⊢ (?%?); //
-]
-qed.
 
 lemma monotone_sigma: