Ignore:
Timestamp:
Sep 3, 2012, 9:03:24 AM (7 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/PolicyFront.ma

    r2273 r2316  
    1717  ∀i.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?).
    1818
    19 (* If instruction i is a jump, then there will be something in the policy at
    20  * position i *)
    21 definition is_jump' ≝
    22   λx:preinstruction Identifier.
    23   match x with
    24   [ JC _ ⇒ true
    25   | JNC _ ⇒ true
    26   | JZ _ ⇒ true
    27   | JNZ _ ⇒ true
    28   | JB _ _ ⇒ true
    29   | JNB _ _ ⇒ true
    30   | JBC _ _ ⇒ true
    31   | CJNE _ _ ⇒ true
    32   | DJNZ _ _ ⇒ true
    33   | _ ⇒ false
    34   ].
    35 
    36 definition is_relative_jump ≝
    37   λinstr:pseudo_instruction.
    38   match instr with
    39   [ Instruction i ⇒ is_jump' i
    40   | _             ⇒ false
    41   ].
    42    
    43 definition is_jump ≝
    44   λinstr:pseudo_instruction.
    45   match instr with
    46   [ Instruction i   ⇒ is_jump' i
    47   | Call _ ⇒ true
    48   | Jmp _ ⇒ true
    49   | _ ⇒ false
    50   ].
    51 
    52 definition is_call ≝
    53   λinstr:pseudo_instruction.
    54   match instr with
    55   [ Call _ ⇒ true
    56   | _ ⇒ false
    57   ].
    58  
    59 definition is_jump_to ≝
    60   λx:pseudo_instruction.λd:Identifier.
    61   match x with
    62   [ Instruction i ⇒ match i with
    63     [ JC j ⇒ d = j
    64     | JNC j ⇒ d = j
    65     | JZ j ⇒ d = j
    66     | JNZ j ⇒ d = j
    67     | JB _ j ⇒ d = j
    68     | JNB _ j ⇒ d = j
    69     | JBC _ j ⇒ d = j
    70     | CJNE _ j ⇒ d = j
    71     | DJNZ _ j ⇒ d = j
    72     | _ ⇒ False
    73     ]
    74   | Call c ⇒ d = c
    75   | Jmp j ⇒ d = j
    76   | _ ⇒ False
    77   ].
    78  
    7919definition not_jump_default ≝
    8020  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
     
    250190    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    251191       pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
     192         (λx.zero ?)
    252193         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    253194         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
     
    258199(* jumps are of the proper size *)
    259200definition sigma_safe ≝
    260  λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ.
     201 λprefix:list labelled_instruction.λlabels:label_map.
    261202 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
    262203 ∀i.i < |prefix| →
    263  let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
    264  let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
    265204 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
    266205 ∀dest.is_jump_to instr dest →
    267    let paddr ≝ lookup_def … labels dest 0 in
    268    let addr ≝ bitvector_of_nat ? (if leb paddr (|prefix|) (* jump to address already known *)
    269    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)
    270    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
     206 let paddr ≝ lookup_def … labels dest 0 in
     207 let 〈j,src,dest〉 ≝
     208   if leb paddr i then (* backward jump *)
     209     let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
     210     let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
     211     let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
     212     〈j,pc_plus_jmp_length,addr〉
     213   else   
     214     let 〈pc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉 in
     215     let 〈npc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
     216     let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd old_sigma) 〈0,short_jump〉)) in
     217     let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)) in
     218     〈j,pc_plus_jmp_length,addr〉 in     
    271219   match j with
    272    [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
    273        bool_to_Prop (¬is_call instr)
    274    | absolute_jump ⇒  \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧
    275        \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    276        bool_to_Prop (¬is_relative_jump instr)
    277    | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    278        \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
     220   [ short_jump ⇒ \fst (short_jump_cond src dest) = true
     221   | absolute_jump ⇒  \fst (absolute_jump_cond src dest) = true (*∧
     222       \fst (short_jump_cond src dest) = false*)
     223   | long_jump   ⇒ True (* do not talk about long jump *)
    279224   ].
     225
     226definition sigma_jumps ≝
     227  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
     228  ∀i.i < |prefix| →
     229  let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment []〉 in
     230  (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump →
     231    bool_to_Prop (¬is_call instr)) ∧
     232  (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = absolute_jump →
     233    bool_to_Prop (¬is_relative_jump instr)).
    280234 
    281235(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
     
    326280(* General note on jump length selection: the jump displacement is added/replaced
    327281 * AFTER the fetch (and attendant PC increase), but we calculate before the
    328  * fetch, which means that in the case of a short and medium jump we are 2
    329  * bytes off and have to compensate.
    330  * For the long jump we don't care, because the PC gets replaced integrally anyway. *)
    331 definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
    332   Identifier → jump_length ≝
    333   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
    334   let pc ≝ \fst inc_sigma in
    335   let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    336   let paddr ≝ lookup_def … labels lbl 0 in
    337   let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
    338   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
    339   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    340   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
     282 * fetch, which means that we are [jump_length] bytes off and have to compensate. *)
     283definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ →
     284  Identifier → ℕ → jump_length ≝
     285  λlabels.λold_sigma.λinc_sigma.λppc.λlbl.λins_len.
     286  let paddr ≝ lookup_def ?? labels lbl 0 in
     287  let 〈src,dest〉 ≝
     288    if leb paddr ppc then (* backward jump *)
     289      let pc ≝ \fst inc_sigma in
     290      let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
     291      〈bitvector_of_nat ? (pc+ins_len), bitvector_of_nat ? addr〉
     292    else
     293      let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in
     294      let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in
     295      〈bitvector_of_nat ? (pc+ins_len), bitvector_of_nat ? addr〉 in
     296  let 〈sj_possible, disp〉 ≝ short_jump_cond src dest in
    341297  if sj_possible
    342298  then short_jump
    343299  else long_jump.
    344300
    345 definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
     301definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ →
    346302  Identifier → jump_length ≝
    347   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
    348   let pc ≝ \fst inc_sigma in
    349   let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    350   let paddr ≝ lookup_def ? ? labels lbl 0 in
    351   let addr ≝ bitvector_of_nat ?
    352     (if leb paddr ppc (* jump to address already known *)
    353     then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)
    354     else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    355   let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in   
     303  λlabels.λold_sigma.λinc_sigma.λppc.λlbl.
     304  let paddr ≝ lookup_def ?? labels lbl 0 in
     305  let 〈src,dest〉 ≝
     306    if leb paddr ppc then (* backward jump *)
     307      let pc ≝ \fst inc_sigma in
     308      let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
     309      〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉
     310    else
     311      let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in
     312      let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in
     313      〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 in
     314  let 〈aj_possible, disp〉 ≝ absolute_jump_cond src dest in   
    356315  if aj_possible
    357316  then absolute_jump
    358317  else long_jump.
    359318 
    360 definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
     319definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ →
    361320  Identifier → jump_length ≝
    362   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
    363   let pc ≝ \fst inc_sigma in
    364   let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    365   let paddr ≝ lookup_def … labels lbl 0 in
    366   let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
    367   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
    368   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    369   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
     321  λlabels.λold_sigma.λinc_sigma.λppc.λlbl.
     322  let paddr ≝ lookup_def ?? labels lbl 0 in
     323  let 〈src,dest〉 ≝
     324    if leb paddr ppc then (* backward jump *)
     325      let pc ≝ \fst inc_sigma in
     326      let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
     327      〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉
     328    else
     329      let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in
     330      let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in
     331      〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 in
     332  let 〈sj_possible, disp〉 ≝ short_jump_cond src dest in
    370333  if sj_possible
    371334  then short_jump
    372   else select_call_length labels old_sigma inc_sigma added ppc lbl.
     335  else select_call_length labels old_sigma inc_sigma ppc lbl.
    373336
    374337definition destination_of: preinstruction Identifier → option Identifier ≝
     
    387350  ].
    388351
     352definition length_of: preinstruction Identifier → ℕ ≝
     353  λi.
     354  match i with
     355  [ JC j     ⇒ 2
     356  | JNC j    ⇒ 2
     357  | JZ j     ⇒ 2
     358  | JNZ j    ⇒ 2
     359  | JB _ j   ⇒ 3
     360  | JBC _ j  ⇒ 3
     361  | JNB _ j  ⇒ 3
     362  | CJNE _ j ⇒ 3
     363  | DJNZ x j ⇒ match x with [ REGISTER _ ⇒ 2 | _ ⇒ 3 ]
     364  | _        ⇒ 0
     365  ].
     366
    389367definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
    390   ℕ → ℕ → preinstruction Identifier → option jump_length ≝
    391   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
     368  ℕ → preinstruction Identifier → option jump_length ≝
     369  λlabels.λold_sigma.λinc_sigma.λppc.λi.
     370  let ins_len ≝ length_of i in
    392371  match destination_of i with
    393   [ Some j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     372  [ Some j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma ppc j ins_len)
    394373  | None       ⇒ None ?
    395374  ].
     
    470449      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    471450    | @bitvector_of_nat_abs
    472       [ / by /
     451      [ @ltb_true_to_lt / by refl/
    473452      | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm
    474453        @le_S_S @le_plus_n_r
    475       | @lt_to_not_eq / by /
     454      | @lt_to_not_eq @ltb_true_to_lt / by refl/
    476455      ]
    477456    ]
     
    617596 #a #b #i cases i
    618597 [2,3,6: #x [3: #y] #H cases H
    619  |4,5: #id #_ cases a cases b / by le_n/
     598 |4,5: #id #_ cases a cases b @leb_true_to_le / by refl/
    620599 |1: #pi cases pi
    621600    try (#x #y #H) try (#x #H) try (#H) cases H
     
    630609  ∀old_sigma.∀sigma.
    631610  sigma_pc_equal program old_sigma sigma →
    632   sigma_safe program (create_label_map program) 0 old_sigma sigma →
     611  sigma_jump_equal program old_sigma sigma →
     612  sigma_jumps program old_sigma →
     613  sigma_safe program (create_label_map program) old_sigma sigma →
    633614  sigma_compact_unsafe program (create_label_map program) sigma →
    634615  sigma_compact program (create_label_map program) sigma.
    635   #program cases program -program #program #Hprogram #old_sigma #sigma #Hequal
    636   #Hsafe #Hcp_unsafe #i #Hi
    637   lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
     616  #program cases program -program #program #Hprogram #old_sigma #sigma
     617  #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #i #Hi
     618  lapply (Hcp_unsafe i Hi) -Hcp_unsafe lapply (Hsafe i Hi) -Hsafe
    638619  inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))
    639620  [ / by /
    640   | #x cases x -x #x1 #x2 #EQ
    641     cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))
     621  | #x cases x -x #pc #jl #EQ
     622    inversion (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))
    642623    [ / by /
    643     | #y cases y -y #y1 #y2 normalize nodelta #H #H2
     624    | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hsafe #Hcp_unsafe
    644625      (*CSC: make a lemma here; to shorten the proof, reimplement the
    645626        safe case so that it also does a pattern matching on the jump_length
    646627        type *)
    647       cut (instruction_size_jmplen x2
     628      cut (instruction_size_jmplen jl
    648629       (\snd (nth i ? program 〈None ?, Comment []〉)) =
    649630       instruction_size … (bitvector_of_nat ? i)
    650631       (\snd (nth i ? program 〈None ?, Comment []〉)))
    651       [5: #H3 <H3 @H2
    652       |4: whd in match (instruction_size_jmplen ??);
    653           whd in match (instruction_size …);
     632      [6: #H <H @Hcp_unsafe
     633      |5: whd in match (instruction_size_jmplen ??);
     634          whd in match (instruction_size …); 
    654635          whd in match (assembly_1_pseudoinstruction …);
    655636          whd in match (expand_pseudo_instruction …);
    656           normalize nodelta whd in match (append …) in H; lapply H
    657           inversion (nth i ? program 〈None ?,Comment []〉)
     637          normalize nodelta inversion (nth i ? program 〈None ?,Comment []〉) in Hsafe;
    658638          #lbl #instr cases instr
    659           [2,3,6: #x [3: #y] normalize nodelta #H #_ %
    660           |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Heq #Hj
    661             lapply (Hj x (refl ? x)) -Hj normalize nodelta
     639          [1: #pi normalize nodelta cases pi
     640              try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe)
     641              try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
     642          |2,3,6: #x [3: #y] normalize nodelta #Hnth_eq #_ %]
     643            #id lapply (Hpc_equal i (le_S_to_le … Hi))
     644            lapply (Hpc_equal (S i) Hi)
     645            lapply (Hjump_equal i Hi)
     646            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #jeq #OSeq #Oeq #Hnth_eq #Hsafe
     647            lapply (Hsafe id (refl ? id)) -Hsafe normalize nodelta
     648            whd in match expand_relative_jump;
     649            whd in match expand_relative_jump_internal; normalize nodelta
    662650            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
    663             cases x2 normalize nodelta
    664             [1,4: whd in match short_jump_cond; normalize nodelta
    665               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    666               [1,3: cases (create_label_map program) #clm #Hclm
    667                 @le_S_to_le @(Hclm x ?)
    668                 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    669                 |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
    670                 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
    671                   [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    672                 |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
    673                   >nth_safe_nth
    674                   [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
    675                     [1,3: >Heq / by refl/
    676                     |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    677                     ]
    678                   ]
    679                 |3,6: / by /
     651            >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) in OSeq; #OSeq >Hcp_unsafe
     652            inversion (leb (lookup_def … (create_label_map program) id 0) i) #Hli
     653            normalize nodelta
     654            [1,3,5,7,9,11,13,15,17,19,21: (* JC JNC JB JNB JBC JZ JNZ CJNE DJNZ Jmp Call *)
     655              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     656              cases jl in jeq; normalize nodelta #jeq
     657              [2,5,8,11,14,17,20,23,26: lapply (Hjumps i Hi) >Hnth_eq >jeq normalize nodelta #abs
     658                cases ((proj2 ?? abs) (refl ? absolute_jump)) (* no absolute reljmps *)
     659              |31: lapply (Hjumps i Hi) >Hnth_eq >jeq normalize nodelta #abs
     660                cases ((proj1 ?? abs) (refl ? short_jump)) (* no short calls *)
     661              |28: >Hnth_eq #Hold cases (short_jump_cond ??) in Hold;
     662                #sj_poss #disp #Hold normalize nodelta >Hold normalize nodelta %
     663              |1,4,7,10,13,16,19,22,25: >Hnth_eq #Hold cases (short_jump_cond ??) in Hold;
     664                #sj_poss #disp #Hold normalize nodelta >Hold
     665                try % try (@(subaddressing_mode_elim … x) #w %)
     666                cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     667                @(subaddressing_mode_elim … a1) #w %
     668              |3,6,9,12,15,18,21,24,27: >Hnth_eq #_ whd in match (jmpeqb ??);
     669                cases (short_jump_cond ??); #sj_poss #disp normalize nodelta
     670                cases sj_poss normalize nodelta try % try (@(subaddressing_mode_elim … x) #w %)
     671                cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     672                @(subaddressing_mode_elim … a1) #w %
     673              |29,32: >Hnth_eq #Hold cases (absolute_jump_cond ??) in Hold;
     674                #aj_poss #disp #Hold >Hold normalize nodelta
     675                cases (short_jump_cond ??);
     676                [1,2: #sj_poss #disp2 normalize nodelta cases sj_poss %
     677                |3,4: @(zero 16)
    680678                ]
    681               |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    682               cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    683               #result #flags normalize nodelta
    684               cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    685               cases (get_index' bool 2 0 flags) normalize nodelta
    686               [3,4: #H cases (proj2 ?? H)
    687               |1,2: cases (eq_bv 9 upper ?)
    688                 [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
    689                 |1,3: #_ normalize nodelta @refl
     679              |30,33: >Hnth_eq #_ whd in match (jmpeqb ??); cases (absolute_jump_cond ??);
     680                #mj_poss #disp2 normalize nodelta cases (short_jump_cond ??);
     681                [1,2: #sj_poss #disp normalize nodelta cases sj_poss cases mj_poss %
     682                |3,4: @(zero 16) (* where does this come from? *)
    690683                ]
    691684              ]
     685            |*: cases (lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) in Oeq jeq;
     686              #opc #ojl #Oeq #jeq normalize nodelta
     687              cases (lookup … (bitvector_of_nat ? (S i)) (\snd old_sigma) 〈0,short_jump〉) in OSeq;
     688              #oSpc #oSjl #OSeq normalize nodelta >jeq
     689              >OSeq >Hcp_unsafe -Hcp_unsafe >Hnth_eq lapply (Hpc_equal (lookup_def … (create_label_map program) id 0) ?)
     690              [1,3,5,7,9,11,13,15,17,19,21:
     691                @(le_S_to_le … (pi2 ?? (create_label_map program) id ?))
     692                cut (i < 2^16)
     693                [1,3,5,7,9,11,13,15,17,19,21:
     694                  @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ] #Hi2
     695                @(proj2 ?? ((proj2 ?? Hprogram) id (bitvector_of_nat ? i) ???))
     696                [1,5,9,13,17,21,25,29,33,37,41:
     697                  whd in match fetch_pseudo_instruction; normalize nodelta
     698                  >(nth_safe_nth … 〈None ?, Comment []〉) >nat_of_bitvector_bitvector_of_nat_inverse
     699                  [1: >Hnth_eq in ⊢ (??%?);
     700                  |3: >Hnth_eq in ⊢ (??%?);
     701                  |5: >Hnth_eq in ⊢ (??%?);
     702                  |7: >Hnth_eq in ⊢ (??%?);
     703                  |9: >Hnth_eq in ⊢ (??%?);
     704                  |11: >Hnth_eq in ⊢ (??%?);
     705                  |13: >Hnth_eq in ⊢ (??%?);
     706                  |15: >Hnth_eq in ⊢ (??%?);
     707                  |17: >Hnth_eq in ⊢ (??%?);
     708                  |19: >Hnth_eq in ⊢ (??%?);
     709                  |21: >Hnth_eq in ⊢ (??%?); ]
     710                  [1,2,3,4,5,6,7,8,9,10,11: %
     711                  |*: assumption]
     712                |3,7,11,15,19,23,27,31,35,39,43:
     713                  >nat_of_bitvector_bitvector_of_nat_inverse assumption
     714                |4,8,12,16,20,24,28,32,36,40,44: %
     715                ]
     716              |*: #Hpc lapply (Hjumps i Hi) >Hnth_eq >(Hjump_equal i Hi)
     717                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     718                cases jl normalize nodelta
     719                [31: #abs cases ((proj1 ?? abs) (refl ? short_jump)) (* no short calls *)
     720                |2,5,8,11,14,17,20,23,26: #abs cases ((proj2 ?? abs) (refl ? absolute_jump)) (* no absolute RJs *)
     721                |1,4,7,10,13,16,19,22,25,28:                 
     722                  >Hpc cases (short_jump_cond ??); #sj_poss #disp #_ #H normalize nodelta
     723                  >H normalize nodelta try % try (@(subaddressing_mode_elim … x) #w %)
     724                  cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     725                  @(subaddressing_mode_elim … a1) #w %
     726                |3,6,9,12,15,18,21,24,27: >Hpc #_ #_ cases (short_jump_cond ??);
     727                  #sj_poss #disp normalize nodelta normalize nodelta
     728                  whd in match (jmpeqb ??); cases sj_poss
     729                  try % try (@(subaddressing_mode_elim … x) #w %)
     730                  cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     731                  @(subaddressing_mode_elim … a1) #w %
     732                |29,32: >Hpc #_ #Hold cases (absolute_jump_cond ??) in Hold;
     733                  #aj_poss #disp #Hold >Hold normalize nodelta cases (short_jump_cond ??)
     734                  [1,2: #sj_poss #disp2 cases sj_poss normalize nodelta %
     735                  |3,4: @(zero 16)
     736                  ]
     737               |30,33: >Hnth_eq #_ #_ whd in match (jmpeqb ??); cases (absolute_jump_cond ??);
     738                  #mj_poss #disp2 normalize nodelta cases (short_jump_cond ??);
     739                  [1,2: #sj_poss #disp normalize nodelta cases sj_poss cases mj_poss %
     740                  |3,4: @(zero 16)
     741                  ]
     742                ]
    692743              ]
    693             |2,3,5,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    694               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    695               [1,3,5,7: cases (create_label_map program) #clm #Hclm
    696                 @le_S_to_le @(Hclm x ?)
    697                 [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    698                 |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
    699                 [1,4,7,10: >nat_of_bitvector_bitvector_of_nat_inverse
    700                   [2,4,6,8: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    701                 |2,5,8,11: whd in match fetch_pseudo_instruction; normalize nodelta
    702                   >nth_safe_nth
    703                   [1,3,5,7: >nat_of_bitvector_bitvector_of_nat_inverse
    704                     [1,3,5,7: >Heq / by refl/
    705                     |*: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    706                     ]
    707                   ]
    708                 |*: / by /
    709                 ]
    710               |*: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    711               normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
    712               cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    713               cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    714               #result #flags normalize nodelta
    715               cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    716               cases (get_index' bool 2 0 flags) normalize nodelta
    717               #H
    718               [1,2,5,6: >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
    719               |*: >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
    720               ]]]
    721           |1: normalize nodelta
    722               cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
    723               [#A #B * / by refl/] #fst_foo
    724               cut (∀x.
    725                     instruction_has_label x (\snd  (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) →
    726                lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    727               [#x #Heq cases (create_label_map program) #clm #Hclm
    728                @le_S_to_le @(Hclm x ?)
    729                @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    730                [ >nat_of_bitvector_bitvector_of_nat_inverse
    731                  [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    732                | whd in match fetch_pseudo_instruction; normalize nodelta
    733                  >nth_safe_nth
    734                  [ >nat_of_bitvector_bitvector_of_nat_inverse
    735                    [ @pair_elim // ]
    736                    @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ]
    737                  | assumption ]] #lookup_in_program
    738               -H #pi cases pi
    739               try (#y #x #Heq #H) try (#x #Heq #H) try (#Heq #H) try % lapply H -H
    740               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    741               #Hj lapply (Hj x (refl ? x)) -Hj
    742               whd in match expand_relative_jump; normalize nodelta
    743               whd in match expand_relative_jump_internal; normalize nodelta
    744               whd in match expand_relative_jump_unsafe; normalize nodelta
    745               whd in match expand_relative_jump_internal_unsafe;
    746               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
    747               <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
    748               [1,4,7,10,13,16,19,22,25:
    749                 >fst_foo @pair_elim #sj_possible #disp #H #H2
    750                 @(pair_replace ?????????? (eq_to_jmeq … H))
    751                 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
    752                   try % >Heq % ]
    753                 >(proj1 ?? H2) try (@refl) normalize nodelta
    754                 [1,2,3,5: @(subaddressing_mode_elim … y) #w %
    755                 | cases y * #sth #sth2 @(subaddressing_mode_elim … sth)
    756                   @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
    757                 ]
    758               |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs
    759               ]
    760               * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
    761               @(pair_replace ?????????? (eq_to_jmeq … H))
    762                 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
    763                   try % >Heq % ]
    764                 #H2 >H2 try (@refl) normalize nodelta
    765                 [1,2,3,5: @(subaddressing_mode_elim … y) #w %
    766                 | cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w
    767                   [1,2: %] whd in match (map ????); whd in match (flatten ??);
    768                   whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
    769                   >length_append >length_append %]]]]]
     744            ]
     745          ]
     746        ]
     747      ]
    770748qed.
    771749
Note: See TracChangeset for help on using the changeset viewer.