Changeset 1417 for src/ASM/Assembly.ma

Timestamp:

Oct 19, 2011, 5:10:27 PM (8 years ago)

Author:

boender

Message:

• proved that jumps always increase - this should make termination easy

File:

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

src/ASM/Assembly.ma

@@ -773 +773 @@
   ].
 
+lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x).
+ #x #y
+ cases y
+ [ //
+ | cases x //
+ | //
+ ]
+qed.
+
 definition is_jump' ≝
   λx:preinstruction Identifier.
@@ -807 +816 @@
   (Σpolicy.
     jump_in_policy program policy ∧
-    (jump_in_policy program policy → True)) ≝ 
+    (jump_in_policy program policy → 
+     (∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
+     jmpleq
+       (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
+       (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
+    )
+   ) ≝ 
   let labels ≝ create_label_trie program old_policy in
   let 〈final_pc, final_policy〉 ≝
@@ -813 +828 @@
     (λprefix.ℕ × Σpolicy.
       jump_in_policy prefix policy ∧
-      (jump_in_policy prefix policy → True)
+      (jump_in_policy prefix policy → 
+       (∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
+       jmpleq
+         (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
+         (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
+      )
     )
     program
@@ -819 +839 @@
       let 〈pc, policy〉 ≝ acc in
       let 〈label,instr〉 ≝ x in
-      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) policy in
+      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
       let add_instr ≝
         match instr with
@@ -828 +848 @@
         ] in
       let 〈new_pc, new_policy〉 ≝
-        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, short_jump〉 in
+        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in
         match add_instr with
         [ None    ⇒ (* i.e. it's not a jump *)
@@ -845 +865 @@
       -n #n #Hn
       % [ @h | % [ @n | normalize nodelta cases instr normalize nodelta
-      [2,3: #x cases (lookup ??? policy ?) #y #z @Hn
-      |6: #x #y cases (lookup ??? policy ?) #w #z @Hn
-      |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???) 
+      [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn
+      |6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn
+      |1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???) 
         [ @Hn
         | #z normalize nodelta <Hn @lookup_opt_insert_miss
@@ -855 +875 @@
           ] ] 
         ]
-      |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hn
+      |4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn
         @lookup_opt_insert_miss @notb_elim >eq_bv_false
         [1,3: //
@@ -873 +893 @@
           |9,10,14,15: #j normalize nodelta #_
             % [1,3,5,7: @pc
-              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
-                cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)          
+              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
+                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)
                 #x #y #Hl normalize nodelta
             % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
@@ -881 +901 @@
           |11,12,13,16,17: #x #j normalize nodelta #_
             % [1,3,5,7,9: @pc
-              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
-                cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)          
+              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
+                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)          
                 #x #y #Hl normalize nodelta
             % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
@@ -890 +910 @@
         |4,5: #j normalize nodelta #_
           % [1,3: @pc
-            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
+            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
                 #x #y normalize nodelta
             % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
@@ -901 +921 @@
       ]
     ]
-  | //
+  | #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
+    [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
+      lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta
+      [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #y #z
+        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
+      |6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #w #z
+        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
+      |1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
+        cases (jump_expansion_step_instruction ???)
+        [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
+        | #z normalize nodelta 
+          whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss
+          [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
+          | @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
+            [ @(bitvector_of_nat_ok … H)
+            | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
+            ] ]
+          ]
+        ] 
+      |4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
+        normalize nodelta >lookup_insert_miss
+        [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
+        |2,4: @notb_elim >eq_bv_false [1,3: // | 2,4: @nmk #H @(absurd (i = (|prefix|)))
+          [1,3: @(bitvector_of_nat_ok … H)
+          |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
+          ] ]
+        ]
+      ]
+    | #Hi >nth_append_second >(injective_S … Hi)
+      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
+        [2,3: #x #Hj @⊥ @Hj
+        |6: #x #y #Hj @⊥ @Hj
+        |1: #pi cases pi
+          [35,36,37: #Hj @⊥ @Hj
+          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
+          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
+          |9,10,14,15: #j normalize nodelta #_
+            cases (lookup ???? 〈0,short_jump〉) #x #y
+            whd in match (snd ℕ jump_expansion_policy ?) 
+            >lookup_insert_hit normalize @jmpleq_max_length
+          |11,12,13,16,17: #z #j normalize nodelta #_
+            cases (lookup ???? 〈0,short_jump〉) #x #y           
+            whd in match (snd ℕ jump_expansion_policy ?)
+            >lookup_insert_hit normalize @jmpleq_max_length
+          ]
+        |4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y
+              whd in match (snd ℕ jump_expansion_policy ?)
+              >lookup_insert_hit normalize @jmpleq_max_length
+        ]
+      | @le_n
+      ]
+    ]
   ]
 | @conj
   [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
-  | //
+  | #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
   ]
 ]