Changeset 2110 for src/ASM/Assembly.ma

Timestamp:

Jun 26, 2012, 4:05:15 PM (7 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/Assembly.ma

@@ -801 +801 @@
 (*CSC: move elsewhere *)
 lemma fetch_pseudo_instruction_append:
- ∀l1,l2. |l1@l2| < 2^16 → ∀ppc,ppc_ok,ppc_ok'.
+ ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
   let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
   fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
@@ -807 +807 @@
  #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
  cut (|l1| + nat_of_bitvector … ppc < 2^16)
- [ @(transitive_lt … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/ ]
+ [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
  -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
  >nat_of_bitvector_bitvector_of_nat_inverse try assumption
@@ -833 +833 @@
        ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
 
+(*CSC: Move elsewhere *)
+axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
+
 definition assembly:
     ∀p: pseudo_assembly_program.
@@ -840 +843 @@
        sigma_policy_specification p sigma policy →
        let 〈preamble,instr_list〉 ≝ p in
-       |instr_list| < 2^16 →
+       |instr_list| ≤ 2^16 →
        let 〈assembled,costs〉 ≝ res in
+       |assembled| ≤ 2^16 ∧
        let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
        let datalabels ≝ construct_datalabels preamble in
-       let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
+       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
        let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
        ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
@@ -861 +865 @@
   let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
   let datalabels ≝ construct_datalabels preamble in
-  let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
+  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
   let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
   let 〈ignore,revcode〉 ≝ pi1 … (
@@ -868 +872 @@
       (λpre. Σppc_code:(Word × (list Byte)).
        sigma_policy_specification 〈preamble,instr_list〉 sigma policy →
-        |instr_list| < 2^16 →
+        |instr_list| ≤ 2^16 →
         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 →
+          (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) →
            let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in
            let 〈len,assembledi〉 ≝
@@ -892 +896 @@
   [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #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 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
-    >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
+    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd %
+    [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
+      [ #limit %2 @limit
+      | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
+        @not_eq_to_le_to_lt assumption ]
+    | >length_reverse <Hfold3
+      @(transitive_le … (S (nat_of_bitvector … (sigma ignore))))
+      [ // | change with (? < ?); @lt_nat_of_bitvector ]]
   | * #sigma_pol_ok1 #_ #instr_list_ok %
     [ % // >sigma_pol_ok1 % ]
-    #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
+    #ppc' #ppc_ok' #abs @⊥ cases abs
+     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
+     |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ]
   | * #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 ] * #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)
-    [2: #S_S_eq normalize nodelta in S_S_eq;
-        (*CSC: TRUE, NEEDS SOME WORK *)
-        cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
-        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
-        >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
-        >fetch_pseudo_instruction_append
-        [3: @le_S_S @le_O_n
-        |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
-        |4: <prf <p_refl in instr_list_ok; #H @H ]
-        #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
-        #j #LTj >nat_of_bitvector_add
-        >nat_of_bitvector_bitvector_of_nat_inverse
-        [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
-        |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
-        >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
-        @nth_safe_prepend
-    | #LTppc''
-      cut (nat_of_bitvector … ppc' < |instr_list|)
-      [ normalize nodelta in LTppc'';
-        @(transitive_le … (nat_of_bitvector … ppc))
-        [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
-           [ //
-           | <p_refl in instr_list_ok; #instr_list_ok
-             @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
-        | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
-          [ >commutative_plus #H @H 
-          | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
-            @(transitive_le … (S (|instr_list|)))
-            [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
-            | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
-              >length_append >nat_of_bitvector_bitvector_of_nat_inverse
-              [2: <p_refl in instr_list_ok; >prf >length_append #H
-                  @(transitive_le … H) //
-              | @le_S_S // ]]]]]
+    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 *
+    cases daemon (*
+    ?????????????? PRIMA NON C'ERA L'OR :-(
+    MANTENERE LO SCHEMA DI PRIMA CON DUE CASI, MA IN UN CASO ppc=0 OVERFLOWED
+    [2: #eq_S_prefix_bound -IH @(IH2 ? LTppc')
+      @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
+      @pair_elim 
+    | #LTppc_ppc
+      cases (le_to_or_lt_eq … LTppc_ppc)
+      [2: #S_S_eq normalize nodelta in S_S_eq;
+          (*CSC: TRUE, NEEDS SOME WORK *)
+          cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
+          >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
+          >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
+          >fetch_pseudo_instruction_append
+          [3: @le_S_S @le_O_n
+          |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
+          |4: <prf <p_refl in instr_list_ok; #H @H ]
+          #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
+          #j #LTj >nat_of_bitvector_add
+          >nat_of_bitvector_bitvector_of_nat_inverse
+          [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
+          |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
+          >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
+          @nth_safe_prepend
+      | #LTppc''
+        cut (nat_of_bitvector … ppc' < |instr_list|)
+        [ normalize nodelta in LTppc'';
+          @(transitive_le … (nat_of_bitvector … ppc))
+          [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
+             [ //
+             | <p_refl in instr_list_ok; #instr_list_ok
+               @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
+          | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
+            [ >commutative_plus #H @H 
+            | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
+              @(transitive_le … (|instr_list|))
+              [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
+              | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
+                >length_append >nat_of_bitvector_bitvector_of_nat_inverse
+                [2: <p_refl in instr_list_ok; >prf >length_append #H
+                    @(transitive_le … H) //
+                | @le_S_S // ]]]]]
       #X lapply (IH2 ppc' X)
       @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
@@ -952 +971 @@
            | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
              [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
-qed.
+*)qed.
 
 definition assembly_unlabelled_program: