Changeset 2242


Ignore:
Timestamp:
Jul 24, 2012, 1:01:55 PM (7 years ago)
Author:
sacerdot
Message:

jump_expansion_step3 streamlined

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2241 r2242  
    918918
    919919lemma jump_expansion_step7:
    920 (*
    921  program :
    922   (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
    923  labels :
    924   (Σlm:label_map
    925    .(∀l:identifier ASMTag
    926      .occurs_exactly_once ASMTag pseudo_instruction l program
    927       →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
    928        =address_of_word_labels_code_mem program l))
    929  old_sigma :
    930   (Σpolicy:ppc_pc_map
    931    .not_jump_default program policy
    932     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    933                  〈O,short_jump〉)
    934      =O
    935     ∧\fst  policy
    936      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
    937                   (\snd  policy) 〈O,short_jump〉)
    938     ∧sigma_compact_unsafe program labels policy
    939     ∧\fst  policy≤ 2 \sup 16 )*)
    940  ∀prefix : list (option Identifier×pseudo_instruction).(*
    941  x : (option Identifier×pseudo_instruction)
    942  tl : (list (option Identifier×pseudo_instruction))
    943  prf : (program=prefix@[x]@tl)
    944  acc :
    945   (Σx0:ℕ×ppc_pc_map
    946    .(let 〈added,policy〉 ≝x0 in 
    947      not_jump_default prefix policy
    948      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    949                   〈O,short_jump〉)
    950       =O
    951      ∧\fst  policy
    952       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    953                    (\snd  policy) 〈O,short_jump〉)
    954      ∧jump_increase prefix old_sigma policy
    955      ∧sigma_compact_unsafe prefix labels policy
    956      ∧(sigma_jump_equal prefix old_sigma policy→added=O)
    957      ∧(added=O→sigma_pc_equal prefix old_sigma policy)
    958      ∧out_of_program_none prefix policy
    959      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    960                   (\snd  policy) 〈O,short_jump〉)
    961       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    962                    (\snd  old_sigma) 〈O,short_jump〉)
    963        +added
    964      ∧sigma_safe prefix labels added old_sigma policy))
    965  inc_added : ℕ
    966  inc_pc_sigma : ppc_pc_map
    967  p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     920 ∀old_sigma : ppc_pc_map.
     921 ∀prefix : list (option Identifier×pseudo_instruction).
    968922 ∀label : option Identifier.
    969  ∀instr : pseudo_instruction.(*
    970  p1 : (x≃〈label,instr〉)
    971  add_instr ≝
    972   match instr
    973    in pseudo_instruction
    974    return λ_:pseudo_instruction.(option jump_length)
    975    with 
    976   [Instruction (i:(preinstruction Identifier))⇒
    977    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    978    (|prefix|) i
    979   |Comment (_:String)⇒None jump_length
    980   |Cost (_:costlabel)⇒None jump_length
    981   |Jmp (j:Identifier)⇒
    982    Some jump_length
    983    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    984   |Call (c:Identifier)⇒
    985    Some jump_length
    986    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    987   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    988  inc_pc : ℕ
    989  inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
    990  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
    991  old_pc : ℕ
    992  old_length : jump_length
    993  Holdeq :
    994   (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
    995    〈O,short_jump〉
    996    =〈old_pc,old_length〉)
    997  Hpolicy :
    998   (not_jump_default prefix 〈inc_pc,inc_sigma〉
    999    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
    1000                 〈O,short_jump〉)
    1001     =O
    1002    ∧inc_pc
    1003     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    1004                  〈O,short_jump〉)
    1005    ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
    1006    ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
    1007    ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
    1008    ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
    1009    ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
    1010    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    1011                 〈O,short_jump〉)
    1012     =old_pc+inc_added
    1013    ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
    1014  added : ℕ*)
    1015  ∀policy : ppc_pc_map.(*
    1016  new_length : jump_length
    1017  isize : ℕ
    1018  Heq1 :
    1019   (match 
    1020    match instr
    1021     in pseudo_instruction
    1022     return λ_:pseudo_instruction.(option jump_length)
    1023     with 
    1024    [Instruction (i:(preinstruction Identifier))⇒
    1025     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    1026     (|prefix|) i
    1027    |Comment (_:String)⇒None jump_length
    1028    |Cost (_:costlabel)⇒None jump_length
    1029    |Jmp (j:Identifier)⇒
    1030     Some jump_length
    1031     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    1032    |Call (c:Identifier)⇒
    1033     Some jump_length
    1034     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    1035    |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    1036     in option
    1037     return λ_0:(option jump_length).(jump_length×ℕ)
    1038     with 
    1039    [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
    1040    |Some (pl:jump_length)⇒
    1041     〈max_length old_length pl,
    1042     instruction_size_jmplen (max_length old_length pl) instr〉]
    1043    =〈new_length,isize〉)
    1044  prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
    1045  prefix_ok : (|prefix|< 2 \sup 16 )
    1046  Heq2a :
    1047   (match 
    1048    match instr
    1049     in pseudo_instruction
    1050     return λ_0:pseudo_instruction.(option jump_length)
    1051     with 
    1052    [Instruction (i:(preinstruction Identifier))⇒
    1053     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    1054     (|prefix|) i
    1055    |Comment (_0:String)⇒None jump_length
    1056    |Cost (_0:costlabel)⇒None jump_length
    1057    |Jmp (j:Identifier)⇒
    1058     Some jump_length
    1059     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    1060    |Call (c:Identifier)⇒
    1061     Some jump_length
    1062     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    1063    |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    1064     in option
    1065     return λ_0:(option jump_length).ℕ
    1066     with 
    1067    [None⇒inc_added
    1068    |Some (x0:jump_length)⇒
    1069     inc_added+(isize-instruction_size_jmplen old_length instr)]
    1070    =added)
    1071  Heq2b :
    1072   (〈inc_pc+isize,
     923 ∀instr : pseudo_instruction.
     924 ∀inc_pc : ℕ.
     925 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
     926 ∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉.
     927 ∀policy : ppc_pc_map.
     928 ∀new_length : jump_length.
     929 ∀isize : ℕ.
     930 ∀Heq2b :
     931  〈inc_pc+isize,
    1073932   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
    1074933   〈inc_pc+isize,
     
    1077936   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    1078937    〈inc_pc,new_length〉 inc_sigma)〉
    1079    =policy)
    1080 *)
     938   =policy.
    1081939 out_of_program_none (prefix@[〈label,instr〉]) policy.
    1082 cases daemon (*
     940 #old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length
     941 #isize #Heq2b
    1083942    #i #Hi2 >append_length <commutative_plus @conj
    1084     [ (* → *) #Hi normalize in Hi;
    1085       cases instr in Heq2; normalize nodelta
    1086       #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
    1087       [1,3,5,7,9,11: >lookup_opt_insert_miss
    1088         [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
    1089           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
    1090           @le_S_to_le @Hi
    1091         |2,4,6,8,10,12: @bitvector_of_nat_abs
    1092           [1,4,7,10,13,16: @Hi2
    1093           |2,5,8,11,14,17: @(transitive_lt … Hi2)
    1094           |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
    1095           ] @le_S_to_le @Hi
    1096         ]
    1097       |2,4,6,8,10,12: @bitvector_of_nat_abs
    1098         [1,4,7,10,13,16: @Hi2
    1099         |2,5,8,11,14,17: @(transitive_lt … Hi2)
    1100         |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
    1101         ] @Hi
    1102       ]
    1103     | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
    1104       elim (decidable_lt i (|prefix|))
    1105       [ #Hi
     943    [ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss
     944      [ >lookup_opt_insert_miss
     945        [ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi
     946        | @bitvector_of_nat_abs try assumption
     947          [ @(transitive_lt … Hi2) @le_S_to_le assumption
     948          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i)))
     949            @(transitive_le … abs) %2 % ]]
     950      | @bitvector_of_nat_abs try assumption
     951          [ @(transitive_lt … Hi2) assumption
     952          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]]
     953    | (* ← *) <Heq2b #Hl normalize
     954      @(leb_elim (S i) (|prefix|))
     955      [ #Hi
    1106956        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
    1107957        #Hl2 (* USE[pass]: out_of_program_none ← *)
    1108         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
    1109         #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
     958        cases (Hpolicy1 i Hi2) #_
     959        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption
    1110960      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
    1111961        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
    1112           [ / by /
     962          [ #X @X
    1113963          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
    1114964          ]
    1115965        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
    1116           >X >eq_bv_refl #H normalize in H; destruct (H)
    1117         ]
    1118       ]
    1119     ]*)
     966          >X >eq_bv_refl #H normalize in H; destruct (H)]]]
    1120967qed.
    1121968
Note: See TracChangeset for help on using the changeset viewer.