Changeset 2242 for src/ASM

Timestamp:

Jul 24, 2012, 1:01:55 PM (9 years ago)

Author:

sacerdot

Message:

jump_expansion_step3 streamlined

File:

• src/ASM/PolicyStep.ma (modified) (2 diffs)

src/ASM/PolicyStep.ma

@@ -918 +918 @@
 
 lemma jump_expansion_step7:
-(*
- program :
-  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
- labels :
-  (Σlm:label_map
-   .(∀l:identifier ASMTag
-     .occurs_exactly_once ASMTag pseudo_instruction l program
-      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
-       =address_of_word_labels_code_mem program l))
- old_sigma :
-  (Σpolicy:ppc_pc_map
-   .not_jump_default program policy
-    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
-                 〈O,short_jump〉)
-     =O
-    ∧\fst  policy
-     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
-                  (\snd  policy) 〈O,short_jump〉)
-    ∧sigma_compact_unsafe program labels policy
-    ∧\fst  policy≤ 2 \sup 16 )*)
- ∀prefix : list (option Identifier×pseudo_instruction).(*
- x : (option Identifier×pseudo_instruction)
- tl : (list (option Identifier×pseudo_instruction))
- prf : (program=prefix@[x]@tl)
- acc :
-  (Σx0:ℕ×ppc_pc_map
-   .(let 〈added,policy〉 ≝x0 in 
-     not_jump_default prefix policy
-     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
-                  〈O,short_jump〉)
-      =O
-     ∧\fst  policy
-      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
-                   (\snd  policy) 〈O,short_jump〉)
-     ∧jump_increase prefix old_sigma policy
-     ∧sigma_compact_unsafe prefix labels policy
-     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
-     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
-     ∧out_of_program_none prefix policy
-     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
-                  (\snd  policy) 〈O,short_jump〉)
-      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
-                   (\snd  old_sigma) 〈O,short_jump〉)
-       +added
-     ∧sigma_safe prefix labels added old_sigma policy))
- inc_added : ℕ
- inc_pc_sigma : ppc_pc_map
- p : (acc≃〈inc_added,inc_pc_sigma〉)*)
+ ∀old_sigma : ppc_pc_map.
+ ∀prefix : list (option Identifier×pseudo_instruction).
  ∀label : option Identifier.
- ∀instr : pseudo_instruction.(*
- p1 : (x≃〈label,instr〉)
- add_instr ≝
-  match instr
-   in pseudo_instruction
-   return λ_:pseudo_instruction.(option jump_length)
-   with 
-  [Instruction (i:(preinstruction Identifier))⇒
-   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
-   (|prefix|) i
-  |Comment (_:String)⇒None jump_length
-  |Cost (_:costlabel)⇒None jump_length
-  |Jmp (j:Identifier)⇒
-   Some jump_length
-   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
-  |Call (c:Identifier)⇒
-   Some jump_length
-   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
-  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
- inc_pc : ℕ
- inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
- Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
- old_pc : ℕ
- old_length : jump_length
- Holdeq :
-  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
-   〈O,short_jump〉
-   =〈old_pc,old_length〉)
- Hpolicy :
-  (not_jump_default prefix 〈inc_pc,inc_sigma〉
-   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
-                〈O,short_jump〉)
-    =O
-   ∧inc_pc
-    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
-                 〈O,short_jump〉)
-   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
-   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
-   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
-   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
-   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
-   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
-                〈O,short_jump〉)
-    =old_pc+inc_added
-   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
- added : ℕ*)
- ∀policy : ppc_pc_map.(*
- new_length : jump_length
- isize : ℕ
- Heq1 :
-  (match 
-   match instr
-    in pseudo_instruction
-    return λ_:pseudo_instruction.(option jump_length)
-    with 
-   [Instruction (i:(preinstruction Identifier))⇒
-    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
-    (|prefix|) i
-   |Comment (_:String)⇒None jump_length
-   |Cost (_:costlabel)⇒None jump_length
-   |Jmp (j:Identifier)⇒
-    Some jump_length
-    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
-   |Call (c:Identifier)⇒
-    Some jump_length
-    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
-   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
-    in option
-    return λ_0:(option jump_length).(jump_length×ℕ)
-    with 
-   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
-   |Some (pl:jump_length)⇒
-    〈max_length old_length pl,
-    instruction_size_jmplen (max_length old_length pl) instr〉]
-   =〈new_length,isize〉)
- prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
- prefix_ok : (|prefix|< 2 \sup 16 )
- Heq2a :
-  (match 
-   match instr
-    in pseudo_instruction
-    return λ_0:pseudo_instruction.(option jump_length)
-    with 
-   [Instruction (i:(preinstruction Identifier))⇒
-    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
-    (|prefix|) i
-   |Comment (_0:String)⇒None jump_length
-   |Cost (_0:costlabel)⇒None jump_length
-   |Jmp (j:Identifier)⇒
-    Some jump_length
-    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
-   |Call (c:Identifier)⇒
-    Some jump_length
-    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
-   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
-    in option
-    return λ_0:(option jump_length).ℕ
-    with 
-   [None⇒inc_added
-   |Some (x0:jump_length)⇒
-    inc_added+(isize-instruction_size_jmplen old_length instr)]
-   =added)
- Heq2b :
-  (〈inc_pc+isize,
+ ∀instr : pseudo_instruction.
+ ∀inc_pc : ℕ.
+ ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
+ ∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉.
+ ∀policy : ppc_pc_map.
+ ∀new_length : jump_length.
+ ∀isize : ℕ.
+ ∀Heq2b :
+  〈inc_pc+isize,
    insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
    〈inc_pc+isize,
@@ -1077 +936 @@
    (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     〈inc_pc,new_length〉 inc_sigma)〉
-   =policy)
-*)
+   =policy.
  out_of_program_none (prefix@[〈label,instr〉]) policy.
-cases daemon (*
+ #old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length
+ #isize #Heq2b
     #i #Hi2 >append_length <commutative_plus @conj
-    [ (* → *) #Hi normalize in Hi;
-      cases instr in Heq2; normalize nodelta
-      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
-      [1,3,5,7,9,11: >lookup_opt_insert_miss
-        [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
-          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
-          @le_S_to_le @Hi
-        |2,4,6,8,10,12: @bitvector_of_nat_abs
-          [1,4,7,10,13,16: @Hi2
-          |2,5,8,11,14,17: @(transitive_lt … Hi2) 
-          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq 
-          ] @le_S_to_le @Hi
-        ]
-      |2,4,6,8,10,12: @bitvector_of_nat_abs
-        [1,4,7,10,13,16: @Hi2
-        |2,5,8,11,14,17: @(transitive_lt … Hi2)
-        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
-        ] @Hi
-      ]
-    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
-      elim (decidable_lt i (|prefix|))
-      [ #Hi 
+    [ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss
+      [ >lookup_opt_insert_miss
+        [ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi
+        | @bitvector_of_nat_abs try assumption
+          [ @(transitive_lt … Hi2) @le_S_to_le assumption
+          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i)))
+            @(transitive_le … abs) %2 % ]]
+      | @bitvector_of_nat_abs try assumption
+          [ @(transitive_lt … Hi2) assumption
+          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]]
+    | (* ← *) <Heq2b #Hl normalize
+      @(leb_elim (S i) (|prefix|))
+      [ #Hi
         lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
         #Hl2 (* USE[pass]: out_of_program_none ← *)
-        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
-        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
+        cases (Hpolicy1 i Hi2) #_
+        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption
       | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
         [ #Hi3 elim (le_to_or_lt_eq … Hi3)
-          [ / by /
+          [ #X @X
           | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
           ]
         | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
-          >X >eq_bv_refl #H normalize in H; destruct (H)
-        ]
-      ]
-    ]*)
+          >X >eq_bv_refl #H normalize in H; destruct (H)]]]
 qed.