Changeset 2072 for src/ASM

Timestamp:

Jun 14, 2012, 4:03:19 AM (8 years ago)

Author:

sacerdot

Message:

We need to import Jaap's invariants now.

File:

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

src/ASM/Assembly.ma

@@ -804 +804 @@
         let 〈ppc,code〉 ≝ ppc_code in
          ppc = bitvector_of_nat … (|pre|) ∧
+         nat_of_bitvector … (sigma ppc) = |code| ∧
          ∀ppc'.∀ppc_ok'.
           nat_of_bitvector … ppc' < nat_of_bitvector … ppc →
@@ -823 +824 @@
       fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
   [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
-    >EQignore_revcode in Hfold; * #Hfold1 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
+    >EQignore_revcode in Hfold; * * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
     >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     (* CSC: FALSE, NEEDS ADDITIONAL ASSUMPTION *) cases daemon
-  | % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
+  | %
+    [ % // (*CSC: NEW INVARIANT FOR JAAP!*) cases daemon ]
+    #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
   | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
-    * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
+    * * #IH1 #IH3 #IH2 whd % [%
+    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
+    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
     #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
     cases (le_to_or_lt_eq … LTppc_ppc)
@@ -873 +878 @@
       >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
       >IH
-      [2: (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon
+      [2: >length_reverse <IH3 (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon
       | @shift_nth_prefix
       |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add