Changeset 2156 for src/ASM

Timestamp:

Jul 6, 2012, 11:30:52 AM (7 years ago)

Author:

sacerdot

Message:

One more invariant, one less daemon.

File:

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

src/ASM/Assembly.ma

@@ -775 +775 @@
          ppc = bitvector_of_nat … (|pre|) ∧
          |code| ≤ 2^16 ∧
+         (|code| = 2^16 → |pre| = |instr_list|) ∧
          (nat_of_bitvector … (sigma ppc) = |code| ∨
           sigma ppc = zero … ∧ |code| = 2^16) ∧
@@ -798 +799 @@
   [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
     >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
-    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold3 #Hfold2 whd
+    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 #Hfold2 whd
     <eq_create_label_cost_map whd %
     [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
@@ -808 +809 @@
       | #Hfold5 %2 <Hfold1 assumption ]]
   | * #sigma_pol_ok1 #_ #instr_list_ok %
-    [ % % // >sigma_pol_ok1 % ]
+    [ % % [%] // [#abs change with (0=S ?) in abs; destruct(abs) | >sigma_pol_ok1 % ]]
     #ppc' #ppc_ok' #abs @⊥ cases abs
      [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
@@ -814 +815 @@
   | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
     #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
-    * * #IH1 #IH2 *
-    [2: #H @⊥ cases daemon (*CSC: impossible case, using Jaaps's ? *)]
+    * * * #IH1 #IH2 #IH4 *
+    [2: * #_ #H @⊥ lapply (IH4 H) >prf >length_append
+        >(plus_n_O (|prefix|)) in ⊢ (??%? → ?); #X
+        lapply (injective_plus_r … X) >length_append normalize #abs' destruct(abs')]
     #IH3 #IH5
     cut (|prefix| < |instr_list|)
@@ -835 +838 @@
     lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta
     cut (pc_delta < 2^16)
-    [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok
-    % [ % [% ] ]
+    [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok check fst_eq
+    cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
+    [ whd in match instruction_size; normalize nodelta
+      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
+    #EQpc_delta2
+    % [ % [% [% ] ] ]
     [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
     | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*)
+    | lapply (sigma_pol_ok2 … ppc_ok) * #sigma_pol_ok3
+      <eq_fetch_pseudo_instruction <eq_create_label_cost_map #sigma_pol4
+       >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta >EQpc_delta2
+       #abs >abs in sigma_pol4; *
+       [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
+       | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
+         >nat_of_bitvector_bitvector_of_nat_inverse // ]
     | cases (sigma_pol_ok2 … ppc_ok)
       whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction