Changeset 2316 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Sep 3, 2012, 9:03:24 AM (8 years ago)
Author:
boender
Message:
  • committed temporary version: true version has to wait until I recuperate my hard disk
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2264 r2316  
    3636 ∀isize : ℕ.
    3737 let add_instr ≝ match instr with
    38   [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    39   | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    40   | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     38  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
     39  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
     40  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
    4141  | _             ⇒ None ?
    4242  ] in
     
    7575           <minus_n_n #abs cases abs
    7676     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    77          #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
     77         #H #non_jump whd in match (jump_expansion_step_instruction ?????) in H;
    7878         >not_is_jump_to_destination_of_None in H; normalize nodelta // ]         
    7979   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
     
    119119 ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy.
    120120 ∀prefix,x,tl. program=prefix@[x]@tl →
    121  ∀inc_added : ℕ.
     121(* ∀inc_added : ℕ. *)
    122122 ∀inc_pc_sigma : ppc_pc_map.
    123123 ∀label : option Identifier.
     
    142142    with 
    143143   [Instruction (i:(preinstruction Identifier))⇒
    144     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     144    jump_expansion_step_instruction labels old_sigma inc_pc_sigma
    145145    (|prefix|) i
    146146   |Comment (_:String)⇒None jump_length
     
    148148   |Jmp (j:Identifier)⇒
    149149    Some jump_length
    150     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     150    (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
    151151   |Call (c:Identifier)⇒
    152152    Some jump_length
    153     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     153    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    154154   |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
    155155    in option
     
    173173   =policy.
    174174 jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
    175  #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
     175 #program #labels #old_sigma #prefix #x #tl #prf #inc_pc_sigma #label
    176176 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length
    177177 #isize #Heq1 #prefix_ok1 #prefix_ok #Heq2
     
    258258    with 
    259259   [Instruction (i:(preinstruction Identifier))⇒
    260     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    261     (|prefix|) i
     260    jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
    262261   |Comment (_:String)⇒None jump_length
    263262   |Cost (_:costlabel)⇒None jump_length
    264263   |Jmp (j:Identifier)⇒
    265264    Some jump_length
    266     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     265    (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
    267266   |Call (c:Identifier)⇒
    268267    Some jump_length
    269     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     268    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    270269   |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
    271270    in option
     
    360359          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
    361360          cases instr in Heq1; normalize nodelta
    362           [1: #pi cases (jump_expansion_step_instruction ??????) normalize nodelta]
     361          [1: #pi cases (jump_expansion_step_instruction ?????) normalize nodelta]
    363362          try (#x #y #Heq1) try (#x #Heq1) try #Heq1
    364363          @eq_f <(proj2 ?? (pair_destruct ?????? Heq1))
     
    390389 ∀isize : ℕ.
    391390 let add_instr ≝ match instr with
    392   [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    393   | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    394   | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     391  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
     392  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
     393  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
    395394  | _             ⇒ None ?
    396395  ] in
     
    480479 ∀isize : ℕ.
    481480 let add_instr ≝ match instr with
    482   [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    483   | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    484   | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     481  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
     482  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
     483  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
    485484  | _             ⇒ None ?
    486485  ] in
     
    671670 ∀isize : ℕ.
    672671 let add_instr ≝ match instr with
    673   [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    674   | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    675   | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     672  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
     673  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
     674  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
    676675  | _             ⇒ None ?
    677676  ] in
     
    753752qed.
    754753
     754(*definition sigma_safe_weak ≝
     755 λprefix:list labelled_instruction.λlabels:label_map.
     756 λsigma:ppc_pc_map.
     757 ∀i.i < |prefix| →
     758 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
     759 ∀lbl.is_jump_to instr lbl →
     760 let paddr ≝ lookup_def … labels lbl 0 in
     761 let 〈j,src,dest〉 ≝
     762   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
     763   let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
     764   let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
     765   〈j,pc_plus_jmp_length,addr〉 in     
     766 i < paddr →
     767 match j with
     768 [ short_jump ⇒ \fst (short_jump_cond src dest) = true
     769 | absolute_jump ⇒  \fst (absolute_jump_cond src dest) = true (*∧
     770      \fst (short_jump_cond src dest) = false*)
     771 | long_jump   ⇒ True (* do not talk about long jump *)
     772 ].*)
     773
     774(*lemma sigma_safe_weak_sigma_safe:
     775  ∀program.∀labels.∀old_sigma.∀sigma.
     776  sigma_safe program labels old_sigma sigma →
     777  sigma_safe_weak program labels sigma.
     778 #program #labels #old_sigma #sigma #Hsigma_safe
     779 #i #Hi lapply (Hsigma_safe i Hi)
     780 cases (nth i ? program 〈None ?, Comment []〉) #label #instr normalize nodelta
     781 #Hsigma_safe #dest #Hjump lapply (Hsigma_safe dest Hjump) -Hsigma_safe
     782 cases (lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) #pc #j
     783 normalize nodelta #Hsigma_safe #Hle
     784 >(not_le_to_leb_false … (lt_to_not_le … Hle)) in Hsigma_safe; normalize nodelta
     785 
     786qed.*)
     787
     788lemma length_of_is_isize: ∀i.is_jump (Instruction i) →
     789  length_of i = instruction_size_jmplen short_jump (Instruction i).
     790 #i cases i
     791 try (#x #y #Hj) try (#x #Hj) try (#Hj) try (cases Hj) try (%)
     792 try ( @(subaddressing_mode_elim … x) #w )  try (%)
     793 cases x * #a1 #a2 normalize nodelta
     794 @(subaddressing_mode_elim … a1) try (#w %)
     795 @(subaddressing_mode_elim … a2) #w %
     796qed.
     797
    755798lemma jump_expansion_step9:
    756 (*
    757  program :
    758   (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
     799 ∀program : list labelled_instruction.
     800  (*(Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l).*)
    759801 ∀labels : label_map.(*
    760802  (Σlm:label_map
     
    774816    ∧sigma_compact_unsafe program labels policy
    775817    ∧\fst  policy≤ 2 \sup 16 )*)
    776  ∀prefix : list (option Identifier×pseudo_instruction).(*
    777  x : (option Identifier×pseudo_instruction)
    778  tl : (list (option Identifier×pseudo_instruction))
    779  prf : (program=prefix@[x]@tl)
    780  acc :
     818 ∀prefix : list (option Identifier×pseudo_instruction).
     819 ∀x : (option Identifier×pseudo_instruction).
     820 ∀tl : (list (option Identifier×pseudo_instruction)).
     821 ∀prf : (program=prefix@[x]@tl).
     822 (*acc :
    781823  (Σx0:ℕ×ppc_pc_map
    782824   .(let 〈added,policy〉 ≝x0 in 
     
    798840                   (\snd  old_sigma) 〈O,short_jump〉)
    799841       +added
    800      ∧sigma_safe prefix labels added old_sigma policy))
    801  inc_added : ℕ
    802  inc_pc_sigma : ppc_pc_map
    803  p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     842     ∧sigma_safe prefix labels added old_sigma policy))*)
     843 (*∀inc_added:ℕ.*)
     844 ∀inc_pc_sigma : ppc_pc_map.
     845 (*p : (acc≃〈inc_added,inc_pc_sigma〉)*)
    804846 ∀label : option Identifier.
    805  ∀instr : pseudo_instruction.(*
    806  p1 : (x≃〈label,instr〉)
    807  add_instr ≝
     847 ∀instr : pseudo_instruction.
     848 ∀p1 : (x≃〈label,instr〉).
     849 (*add_instr ≝
    808850  match instr
    809851   in pseudo_instruction
     
    821863   Some jump_length
    822864   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    823   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    824  inc_pc : ℕ
    825  inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
    826  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
    827  old_pc : ℕ
    828  old_length : jump_length
    829  Holdeq :
    830   (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
    831    〈O,short_jump〉
    832    =〈old_pc,old_length〉)
    833  Hpolicy :
     865  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     866 ∀inc_pc : ℕ.
     867 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
     868 ∀Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉).
     869 ∀old_pc : ℕ.
     870 ∀old_length : jump_length.
     871 ∀Holdeq :
     872  bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     873   〈O,short_jump〉=〈old_pc,old_length〉.
     874 (*Hpolicy :
    834875  (not_jump_default prefix 〈inc_pc,inc_sigma〉
    835876   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     
    849890   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
    850891 ∀added : ℕ.
    851  ∀policy : ppc_pc_map.(*
    852  new_length : jump_length
    853  isize : ℕ
    854  Heq1 :
     892 ∀policy : ppc_pc_map.
     893 ∀new_length : jump_length.
     894 ∀isize : ℕ.
     895 Heq1 :
    855896  (match 
    856897   match instr
     
    859900    with 
    860901   [Instruction (i:(preinstruction Identifier))⇒
    861     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     902    jump_expansion_step_instruction labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) i
     903   |Comment (_:String)⇒None jump_length
     904   |Cost (_:costlabel)⇒None jump_length
     905   |Jmp (j:Identifier)⇒
     906    Some jump_length
     907    (select_jump_length labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) j)
     908   |Call (c:Identifier)⇒
     909    Some jump_length
     910    (select_call_length labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) c)
     911   |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     912    in option
     913    return λ_:(option jump_length).(jump_length×ℕ)
     914    with 
     915   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     916   |Some (pl:jump_length)⇒
     917    〈max_length old_length pl,
     918    instruction_size_jmplen (max_length old_length pl) instr〉]
     919   =〈new_length,isize〉).
     920 ∀prefix_ok1 : (S (|prefix|)< 2 \sup 16 ).
     921 ∀prefix_ok : (|prefix|< 2 \sup 16 ).
     922 (*∀Heq2a :
     923  (match 
     924   match instr
     925    in pseudo_instruction
     926    return λ_:pseudo_instruction.(option jump_length)
     927    with 
     928   [Instruction (i:(preinstruction Identifier))⇒
     929    jump_expansion_step_instruction labels old_sigma inc_pc_sigma
    862930    (|prefix|) i
    863931   |Comment (_:String)⇒None jump_length
     
    865933   |Jmp (j:Identifier)⇒
    866934    Some jump_length
    867     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     935    (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
    868936   |Call (c:Identifier)⇒
    869937    Some jump_length
    870     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    871    |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     938    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
     939   |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
    872940    in option
    873     return λ_0:(option jump_length).(jump_length×ℕ)
    874     with 
    875    [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
    876    |Some (pl:jump_length)⇒
    877     〈max_length old_length pl,
    878     instruction_size_jmplen (max_length old_length pl) instr〉]
    879    =〈new_length,isize〉)
    880  prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
    881  prefix_ok : (|prefix|< 2 \sup 16 )
    882  Heq2a :
    883   (match 
    884    match instr
    885     in pseudo_instruction
    886     return λ_0:pseudo_instruction.(option jump_length)
    887     with 
    888    [Instruction (i:(preinstruction Identifier))⇒
    889     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    890     (|prefix|) i
    891    |Comment (_0:String)⇒None jump_length
    892    |Cost (_0:costlabel)⇒None jump_length
    893    |Jmp (j:Identifier)⇒
    894     Some jump_length
    895     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    896    |Call (c:Identifier)⇒
    897     Some jump_length
    898     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    899    |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    900     in option
    901     return λ_0:(option jump_length).ℕ
     941    return λ_:(option jump_length).ℕ
    902942    with 
    903943   [None⇒inc_added
    904944   |Some (x0:jump_length)⇒
    905945    inc_added+(isize-instruction_size_jmplen old_length instr)]
    906    =added)
    907  Heq2b :
    908   (〈inc_pc+isize,
     946   =added).*)
     947 ∀Heq2b:
     948  〈inc_pc+isize,
    909949   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
    910950   〈inc_pc+isize,
     
    913953   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    914954    〈inc_pc,new_length〉 inc_sigma)〉
    915    =policy)
    916 *)
    917  sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy.
    918 cases daemon(*
    919     #i >append_length >commutative_plus #Hi normalize in Hi;
    920     elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    921     [ >nth_append_first [2: @Hi]
    922       <Heq2b >lookup_insert_miss
     955   =policy.
     956 sigma_compact_unsafe program labels old_sigma →
     957 \fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     958                〈O,short_jump〉)
     959    =old_pc+added →
     960 inc_pc = \fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     961                 〈O,short_jump〉) → 
     962 sigma_safe prefix labels old_sigma 〈inc_pc,inc_sigma〉 →
     963 (*sigma_safe_weak program labels old_sigma → *)
     964 sigma_safe (prefix@[〈label,instr〉]) labels old_sigma policy.
     965 #program #labels #old_sigma #prefix #x #tl #prf (*#inc_added*) #inc_pc_sigma
     966 #label #instr #p1 #inc_pc #inc_sigma #Hips #old_pc #old_length #Holdeq #added
     967 #policy #new_length #isize #Heq1 #prefix_ok1 #prefix_ok (*#Heq2a*) #Heq2b
     968 #Hold_compact #Hold_pc #Hinc_pc #Hsigma_safe
     969 #i >append_length >commutative_plus #Hi normalize in Hi;
     970 <Heq2b
     971 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     972 [ >nth_append_first [2: @Hi] lapply (Hsigma_safe i Hi)
     973   inversion (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins #Heq normalize nodelta
     974   #Hsafe #dest #Hjump lapply (Hsafe dest Hjump) -Hsafe
     975   inversion (leb (lookup_def … labels dest 0) i) #Hle normalize nodelta
     976   [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
     977     [ >lookup_insert_miss
     978       [ >lookup_insert_miss
     979         [ >lookup_insert_miss
     980           [ >lookup_insert_miss
     981             [ >lookup_insert_miss
     982               [ >lookup_insert_miss
     983                 [ #H @H
     984                 ]
     985               ]
     986             ]
     987            ]
     988          ]
     989        ]
     990        @bitvector_of_nat_abs try assumption
     991        try (@(transitive_lt … prefix_ok))
     992        try (@lt_to_not_eq)
     993        try (@(transitive_lt … Hi) @le_S_S @leb_true_to_le @Hle)
     994        try assumption
     995        try (@le_S_S) try (@(le_S_to_le … Hi))
     996        [ @(lt_to_le_to_le ? (S i))
     997          [ @le_S_S @leb_true_to_le @Hle
     998          | @le_S_to_le @Hi
     999          ]
     1000        | @le_S_to_le @le_S_to_le @Hi
     1001        ]
     1002      ]
     1003    | #H >lookup_insert_miss
     1004      [2: @bitvector_of_nat_abs [ @(transitive_lt … prefix_ok) @Hi | @prefix_ok1 |
     1005        @lt_to_not_eq @(transitive_lt … Hi) @le_n ] ]
     1006      >lookup_insert_miss
     1007      [2: @bitvector_of_nat_abs [ @(transitive_lt … prefix_ok) @Hi | @prefix_ok |
     1008        @lt_to_not_eq @Hi ] ]
     1009      @H
     1010    ]
     1011  | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
     1012    #dest #Hjump (*cases instr in Hjump Heq1;
     1013    [2,3,6: #y [3: #id] normalize nodelta #abs cases abs
     1014    |1: #pi normalize nodelta cases pi
     1015        try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
     1016        try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id]
     1017    #id #Hjump normalize nodelta*)
     1018    >lookup_insert_miss
     1019    [2: @bitvector_of_nat_abs [ @prefix_ok | @prefix_ok1 | @lt_to_not_eq @le_n ] ]
     1020    >lookup_insert_hit >lookup_insert_hit
     1021    inversion (leb (lookup_def … labels dest 0) (|prefix|)) #Hle normalize nodelta
     1022    [ >lookup_insert_miss [2: @bitvector_of_nat_abs
     1023      [ @(le_to_lt_to_lt … prefix_ok) @leb_true_to_le @Hle
     1024      | @prefix_ok1
     1025      | @lt_to_not_eq @le_S_S @leb_true_to_le @Hle
     1026      ]]
     1027      elim (le_to_or_lt_eq … (leb_true_to_le … Hle)) -Hle #Hle
    9231028      [ >lookup_insert_miss
     1029        [2: @bitvector_of_nat_abs
     1030          [3: @lt_to_not_eq @Hle
     1031          |1: @(transitive_lt ??? Hle)
     1032          ] @prefix_ok
     1033        ]
     1034      | >Hle >lookup_insert_hit
     1035      ]
     1036      normalize nodelta cases instr in Hjump Heq1;
     1037      [1,7: #pi normalize nodelta cases pi
     1038        try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
     1039        try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
     1040      |2,3,6,8,9,12: #y [3,6: #id] normalize nodelta #abs cases abs
     1041      ]
     1042      #id #Hjump normalize nodelta #Heq1
     1043      <(proj1 ?? (pair_destruct ?????? Heq1))
     1044      <(proj2 ?? (pair_destruct ?????? Heq1)) <Hjump
     1045      whd in match (select_jump_length labels old_sigma ? (|prefix|) dest);
     1046      whd in match (select_call_length labels old_sigma ? (|prefix|) dest);
     1047      whd in match (select_reljump_length labels old_sigma ? (|prefix|) dest ?);
     1048      try (>(le_to_leb_true … (le_S_to_le … Hle)))
     1049      try (>Hle >(le_to_leb_true … (le_n (|prefix|))) >(le_to_leb_true … (le_n (|prefix|))))
     1050      normalize nodelta
     1051      inversion (absolute_jump_cond ??) #aj_poss #disp2 normalize nodelta
     1052      inversion (short_jump_cond ??); #sj_poss #disp normalize nodelta
     1053      cases sj_poss #Hsj #Haj cases old_length normalize nodelta
     1054      try (>Hsj %) try (cases aj_poss @I)
     1055      [1,2,3: @(subaddressing_mode_elim … y) #w >Hsj %
     1056      |4: cases y in Hsj; #y cases y #a1 #a2 #Hsj normalize nodelta
     1057        @(subaddressing_mode_elim … a1) [2,3: #w >Hsj %]
     1058        @(subaddressing_mode_elim … a2) #w >Hsj %
     1059      |5: cases y in Hsj; * try (#a1 #a2 #Hsj) try (#a1 #Hsj) normalize nodelta
     1060        try (>Hsj %) try (cases a2) try (cases a1)
     1061      ]
     1062      <Hinc_pc in Hsj; #Hsj
     1063      try (>Hsj %)
     1064      [1,2,3: @(subaddressing_mode_elim … y) #w >Hsj %
     1065      |4: cases y in Hsj; #y cases y #a1 #a2 #Hsj normalize nodelta
     1066        @(subaddressing_mode_elim … a1) [2,3: #w >Hsj %]
     1067        @(subaddressing_mode_elim … a2) #w >Hsj %
     1068      |5: cases y in Hsj; * try (#a1 #a2 #Hsj) try (#a1 #Hsj) normalize nodelta
     1069        try (>Hsj %) try (cases a2) try (cases a1)
     1070      ]
     1071      try (cases aj_poss in Haj; #Haj >Haj %) cases aj_poss in Haj; #Haj try @I
     1072      normalize nodelta
     1073      <Hinc_pc in Haj; #Haj >Haj %
     1074    | normalize nodelta lapply (Hold_compact (|prefix|) ?)
     1075      [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ]
     1076      inversion (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
     1077      [ #_ #H cases H
     1078      | #x cases x -x #opc #ojl #EQ normalize nodelta
     1079        inversion (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
     1080        [ #_ #H cases H
     1081        | #x cases x -x #oSpc #oSjl #SEQ normalize nodelta -Hold_compact #Hold_compact
     1082          >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hold_compact
     1083          >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; normalize nodelta
     1084          #Holdeq >prf >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     1085          >p1 cases instr in Hjump Heq1;
     1086          [1,7: #pi normalize nodelta cases pi
     1087            try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
     1088            try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
     1089          |2,3,6,8,9,12: #y [3,6: #id] normalize nodelta #abs cases abs
     1090          ]
     1091          #id #Hjump normalize nodelta <Hjump #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1))
     1092          whd in match (select_jump_length labels old_sigma ? (|prefix|) dest);
     1093          whd in match (select_call_length labels old_sigma ? (|prefix|) dest);
     1094          whd in match (select_reljump_length labels old_sigma ? (|prefix|) dest ?); >Hle normalize nodelta
     1095          >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) <(proj2 ?? (pair_destruct ?????? Holdeq))
     1096          cases ojl normalize nodelta
     1097          [1,2,4,5,8,11,14,16,17,19,20,23,26:
     1098            inversion (short_jump_cond ??); #sj_poss #disp #Hsj cases sj_poss try (%) @I
     1099          |3,6,9,12,15,18,21,24,27,30,33: @I
     1100          |28,29: inversion (short_jump_cond ??); #sj_poss #disp #Hsj normalize nodelta
     1101            cases sj_poss [1,3: % |2,4: inversion (absolute_jump_cond ??);
     1102            #aj_poss #disp2 #Haj cases aj_poss try (%) @I ]
     1103          |31,32: inversion (absolute_jump_cond ??); #aj_poss #disp #Haj cases aj_poss
     1104            %
     1105          ]
     1106          [1,2,3,5: @(subaddressing_mode_elim … y) #w
     1107            cases (short_jump_cond ??) #sj_poss #disp cases sj_poss
     1108            try (%) @I
     1109          |4: cases y * try (#a1 #a2) try (#a1) normalize nodelta
     1110            @(subaddressing_mode_elim … a1)
     1111            [2,3: #w cases (short_jump_cond ??); #sj_poss #disp cases sj_poss try (%) @I]
     1112            @(subaddressing_mode_elim … a2) #w whd in match (length_of ?);
     1113            normalize nodelta cases (short_jump_cond ??); #sj_poss #disp cases sj_poss
     1114            try (%) @I
     1115          ]
     1116        ]
     1117      ]
     1118    ] 
     1119  ]
     1120  <Hi >lookup_insert_miss
     1121  [ >lookup_insert_miss
     1122    [ >lookup_insert_miss
     1123      [ >lookup_insert_hit >lookup_insert_miss
    9241124        [ >lookup_insert_miss
    925           [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
    926             [ >lookup_insert_miss
    927               [ (* USE[pass]: sigma_safe *)
    928                 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
    929                 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
    930                 #pc #j normalize nodelta
    931                 cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
    932                 #Spc #Sj normalize nodelta
    933                 cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
    934                 #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj
    935                 lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|))))
    936                 cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); #H
    937                 [ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H
    938                   [ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
    939                     >lookup_insert_miss
    940                     [ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H
    941                       [ >lookup_insert_miss
    942                         [ #H2 @H2
    943                         | @bitvector_of_nat_abs
    944                           [3: @lt_to_not_eq @H
    945                           |1: @(transitive_lt ??? H)
    946                           ]
    947                           @prefix_ok
    948                         ]
    949                       | >H >lookup_insert_hit
    950                         (* USE: inc_pc = lookup |prefix| *)
    951                         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    952                         #H2 @H2
    953                       ]
    954                     | @bitvector_of_nat_abs
    955                       [3: @lt_to_not_eq @H
    956                       |1: @(transitive_lt ??? H)
    957                       ]
    958                       @prefix_ok1
    959                     ]
    960                   | >H >lookup_insert_hit normalize nodelta
    961                     >(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (|prefix|)))))
    962                     normalize nodelta
    963                     >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    964                     #H2 >(proj2 ?? (proj1 ?? Hpolicy))
    965                   ]
    966                 |
    967                        
    968                        
    969                        
    970                 [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
    971                   [1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) #H
    972                     [1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H
    973                       [1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
    974                         >lookup_insert_miss
    975                         [2,4,6: @bitvector_of_nat_abs
    976                           [3,6,9: @lt_to_not_eq @H
    977                           |1,4,7: @(transitive_lt ??? H)
    978                           ]
    979                           @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    980                           @le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    981                         ]
    982                         cases (le_to_or_lt_eq … H) -H #H
    983                         [1,3,5: >lookup_insert_miss
    984                           [1,3,5: #H @H
    985                           |2,4,6: @bitvector_of_nat_abs
    986                             [3,6,9: @lt_to_not_eq @(le_S_S_to_le … H)
    987                             |1,4,7: @(transitive_lt ??? (le_S_S_to_le … H))
    988                             ]
    989                             @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    990                             >append_length @le_S_S @le_plus_n_r
    991                           ]
    992                         |2,4,6: >(injective_S … H) >lookup_insert_hit
    993                           (* USE: blerp *)
    994                           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    995                           #H @H
    996                         ]
    997                       |2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false)
    998                         [2,4,6: @le_to_not_lt @le_n]
    999                         normalize nodelta
    1000                         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1001                         [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
    1002                          lapply (refl ? (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1003                           cases (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1004                           [1,3,5: normalize nodelta #_ #abs cases abs
    1005                           |2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ
    1006                             lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1007                             cases (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1008                             [1,3,5: normalize nodelta #_ #abs cases abs
    1009                             |2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact
    1010                               >(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉)
    1011                               >(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq;
    1012                               #H >Pcompact >(proj1 ?? (pair_destruct ?????? H))
    1013                               >commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy))
    1014                               <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    1015                               >prf >nth_append_second
    1016                               [1,3,5: <minus_n_n whd in match (nth ????); >p1
    1017                                 cases daemon (* to be lemmatized *)
    1018                               |2,4,6: @le_n
    1019                               ]
    1020                             ]
    1021                           ]
    1022                         ]
    1023                       |2,4,6: >(not_le_to_leb_false … H)
    1024                         >not_le_to_leb_false
    1025                         [2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H
    1026                         |1,3,5: normalize nodelta #H @H
    1027                         ]
    1028                       ]
    1029                     |2,5,8: cases daemon (* like previous case *)
    1030                     |3,6,9: cases daemon (* like previous case *)
    1031                     ]
    1032                   |4,5: #x normalize nodelta cases daemon (* blerp *)
    1033                   |1: cases daemon (* blerp *)
    1034                   ]
    1035                
    1036                                
    1037                          
    1038 
    1039    (*(\fst  (short_jump_cond (bitvector_of_nat 16 Spc)
    1040               (bitvector_of_nat 16
    1041                (inc_pc
    1042                 +instruction_size_jmplen
    1043                  (max_length old_length
    1044                   (select_jump_length labels old_sigma inc_pc_sigma inc_added
    1045                    (|prefix|) xx)) (Jmp xx))))
    1046   =true                   *)
    1047                        
    1048                  
    1049   ]       
    1050               [ >lookup_insert_miss
    1051                 [ (* USE[pass]: sigma_safe *)
    1052                   lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
    1053                   cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
    1054                   #pc #j normalize nodelta
    1055                   cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
    1056                   #Spc #Sj normalize nodelta
    1057                   cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
    1058                   #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
    1059                   [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
    1060                     [1,4,7: *)
     1125          [ >Hinc_pc <Hi #H @H
     1126          ]
     1127        ]
     1128      ]
     1129    ]
     1130  ]
     1131  @bitvector_of_nat_abs
     1132  try (>Hi @prefix_ok) try (>Hi @prefix_ok1)
     1133  [1,3: @(transitive_lt … prefix_ok) <Hi @le_S_S
     1134  | @lt_to_not_eq @le_S_S
     1135  | @lt_to_not_eq @le_S @le_S_S
     1136  |5,7: @lt_to_not_eq @le_n
     1137  |6,8: whd >Hi @le_S_to_le @prefix_ok
     1138  |9: @lt_to_not_eq @le_S @le_n
     1139  ]
     1140  @leb_true_to_le @Hle
    10611141qed.
    10621142
     
    11051185      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
    11061186       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
    1107       (sigma_safe prefix labels added old_sigma policy))
     1187      (sigma_safe prefix labels old_sigma policy))
    11081188    program
    11091189    (λprefix.λx.λtl.λprf.λacc.
     
    11201200       *)
    11211201      let add_instr ≝ match instr with
    1122       [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    1123       | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    1124       | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     1202      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
     1203      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
     1204      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
    11251205      | _             ⇒ None ?
    11261206      ] in
     
    12261306      … Heq1 prefix_ok1 prefix_ok Heq2b)
    12271307    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1228     cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
     1308    cases (pi2 … old_sigma) * * * #Hnjd #_ #_ #_ #_ @Hnjd
    12291309  | (* sigma_compact_unsafe *)
    12301310    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
     
    12331313    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
    12341314  | (* policy_jump_equal → added = 0 *)
    1235     @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
     1315    @(jump_expansion_step5 … inc_added … Holdeq … Heq1 … Heq2b) try assumption
    12361316    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
    12371317    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     
    12501330    | @(proj2 ?? (proj1 ?? Hpolicy)) ]
    12511331  | (* sigma_safe *)
    1252     @jump_expansion_step9 (*try assumption
    1253     @(proj2 ?? Hpolicy) *)
    1254   ]     
     1332    @(jump_expansion_step9 … prf … p1 … Holdeq … Heq1 prefix_ok1 prefix_ok)
     1333    [ @inc_pc_sigma
     1334    | >Hips %
     1335    | @inc_added
     1336    | >Hips @Heq2b
     1337    | @(proj2 ?? (proj1 ?? (pi2 ?? old_sigma)))
     1338    | >Hips @(proj2 ?? (proj1 ?? Hpolicy))
     1339    | >Hips @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1340    | >Hips @(proj2 ?? Hpolicy)
     1341    ]
     1342  ]
    12551343| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    12561344  [ #i cases i
Note: See TracChangeset for help on using the changeset viewer.