Changeset 2237

Timestamp:

Jul 23, 2012, 11:11:27 PM (7 years ago)

Author:

sacerdot

Message:

Even shorter version.

File:

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

src/ASM/PolicyStep.ma

@@ -115 +115 @@
 
 lemma jump_expansion_step3:
-∀program.(* :
-  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
- ∀labels :
-  label_map(*Σ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))*)
+ ∀program.
+ ∀labels : label_map.
+ ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy.
+ ∀prefix,x,tl. program=prefix@[x]@tl →
  ∀inc_added : ℕ.
- ∀inc_pc_sigma : ppc_pc_map. (*
- p : (acc≃〈inc_added,inc_pc_sigma〉)*)
+ ∀inc_pc_sigma : ppc_pc_map.
  ∀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]*)
+ ∀p1 : x≃〈label,instr〉.
  ∀inc_pc : ℕ.
- ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).(*
- Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*)
+ ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
  ∀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 : ℕ*)
+   〈O,short_jump〉 =〈old_pc,old_length〉.
+ ∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉.
  ∀policy : ppc_pc_map.
  ∀new_length : jump_length.
@@ -239 +162 @@
    =〈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)*)
+ ∀prefix_ok : |prefix|< 2 \sup 16.
  ∀Heq2b :
   〈inc_pc+isize,
@@ -303 +201 @@
         [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program
         >lookup_insert_miss
-        [ >lookup_insert_hit inversion (is_jump instr) normalize nodelta
-          [ cases instr in Heq1; normalize nodelta
-            [ #pi whd in match jump_expansion_step_instruction; normalize nodelta
-              lapply (destination_of_None_to_is_jump_false pi)
-              cases (destination_of ?) normalize nodelta
-              [ #abs #_ whd in match is_jump; normalize nodelta >abs try % #abs'
-                destruct(abs')
-              | #tgt #_ #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
-              ]
-            |2,3,6: #x [3: #y] #_ #Hj normalize in Hj; destruct(Hj)
-            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
-            ]
-          | lapply Heq1 -Heq1; inversion instr normalize nodelta
-            [ 4,5: #x #_ #_ #abs @⊥ normalize in abs; destruct(abs)
-            | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
-              lapply (destination_of_Some_to_is_jump_true pi)
-              cases (destination_of pi) normalize nodelta
-              [2: #tgt #abs #_ whd in match is_jump; normalize nodelta >abs try %
-                  #abs' destruct(abs')]
-              #_
-            |*: #x [3: #y] #Heqi ]
-            #Hj #Hx <(proj1 ?? (pair_destruct ?????? Hj))
-              lapply (pi2 ?? old_sigma (|prefix|) ??)
-              [1,4,7,10: >prf >nth_append_second
-                [1,3,5,7: <minus_n_n whd in match (nth ????); >p1 >Heqi >Hj try % >Hx %
-                |*: @le_n
-                ]
-              |2,5,8,11: @lt_prefix_program
-              |*: >Holdeq #EQ2 >EQ2 %2 @refl]]
+        [ >lookup_insert_hit normalize nodelta
+          inversion instr in Heq1; normalize nodelta
+          [4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
+          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
+            lapply (destination_of_None_to_is_jump_false pi)
+            lapply (destination_of_Some_to_is_jump_true pi)
+            cases (destination_of ?) normalize nodelta
+            [ #tgt #Hx
+            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
+            ]
+          |2,3,6: #x [3: #y] #Heqi ]
+          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
+          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
+          [1,3,5,7: >prf >nth_append_second try @le_n
+            <minus_n_n whd in match (nth ????); >p1 >Heqi
+            whd in match is_jump; normalize nodelta try % >Hx %
+          |*: >Holdeq #EQ2 >EQ2 %2 %]
         | @bitvector_of_nat_abs
           [ @le_S_to_le ]
@@ -511 +397 @@
     <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
   | (* jump_increase *)
+    @(jump_expansion_step3 …)
     cases daemon (*XXX*)
   | (* sigma_compact_unsafe *) cases daemon (*