Changeset 2316


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
Location:
src/ASM
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2143 r2316  
    10061006  | _ ⇒ False
    10071007  ].
     1008
     1009
     1010(* If instruction i is a jump, then there will be something in the policy at
     1011 * position i *)
     1012definition is_jump' ≝
     1013  λx:preinstruction Identifier.
     1014  match x with
     1015  [ JC _ ⇒ true
     1016  | JNC _ ⇒ true
     1017  | JZ _ ⇒ true
     1018  | JNZ _ ⇒ true
     1019  | JB _ _ ⇒ true
     1020  | JNB _ _ ⇒ true
     1021  | JBC _ _ ⇒ true
     1022  | CJNE _ _ ⇒ true
     1023  | DJNZ _ _ ⇒ true
     1024  | _ ⇒ false
     1025  ].
     1026
     1027definition is_relative_jump ≝
     1028  λinstr:pseudo_instruction.
     1029  match instr with
     1030  [ Instruction i ⇒ is_jump' i
     1031  | _             ⇒ false
     1032  ].
     1033   
     1034definition is_jump ≝
     1035  λinstr:pseudo_instruction.
     1036  match instr with
     1037  [ Instruction i   ⇒ is_jump' i
     1038  | Call _ ⇒ true
     1039  | Jmp _ ⇒ true
     1040  | _ ⇒ false
     1041  ].
     1042
     1043definition is_call ≝
     1044  λinstr:pseudo_instruction.
     1045  match instr with
     1046  [ Call _ ⇒ true
     1047  | _ ⇒ false
     1048  ].
     1049 
     1050definition is_jump_to ≝
     1051  λx:pseudo_instruction.λd:Identifier.
     1052  match x with
     1053  [ Instruction i ⇒ match i with
     1054    [ JC j ⇒ d = j
     1055    | JNC j ⇒ d = j
     1056    | JZ j ⇒ d = j
     1057    | JNZ j ⇒ d = j
     1058    | JB _ j ⇒ d = j
     1059    | JNB _ j ⇒ d = j
     1060    | JBC _ j ⇒ d = j
     1061    | CJNE _ j ⇒ d = j
     1062    | DJNZ _ j ⇒ d = j
     1063    | _ ⇒ False
     1064    ]
     1065  | Call c ⇒ d = c
     1066  | Jmp j ⇒ d = j
     1067  | _ ⇒ False
     1068  ].
  • src/ASM/Assembly.ma

    r2268 r2316  
    441441*)
    442442definition expand_relative_jump_internal:
    443  ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
     443 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.∀policy:Word → bool.
    444444 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
    445445 list instruction
    446446 ≝
    447   λlookup_labels.λsigma.λlbl.λppc,i.
     447  λlookup_labels.λsigma.λpolicy.λlbl.λppc,i.
    448448   let lookup_address ≝ sigma (lookup_labels lbl) in
    449449   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    450450   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    451    if sj_possible
     451   if sj_possible ∧ ¬(policy ppc)
    452452   then
    453453     let address ≝ RELATIVE disp in
     
    462462
    463463definition expand_relative_jump:
    464   ∀lookup_labels.∀sigma.
     464  ∀lookup_labels.∀sigma.∀policy.
    465465  Word → (*jump_length →*)
    466466  preinstruction Identifier → list instruction ≝
    467467  λlookup_labels: Identifier → Word.
    468468  λsigma:Word → Word.
     469  λpolicy:Word → bool.
    469470  λppc: Word.
    470471  (*λjmp_len: jump_length.*)
     
    472473  (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*)
    473474  match i with
    474   [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?)
    475   | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?)
    476   | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr)
    477   | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?)
    478   | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?)
    479   | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr)
    480   | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr)
    481   | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr)
    482   | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr)
     475  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JC ?)
     476  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNC ?)
     477  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JB ? baddr)
     478  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JZ ?)
     479  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNZ ?)
     480  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JBC ? baddr)
     481  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (JNB ? baddr)
     482  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (CJNE ? addr)
     483  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma policy jmp ppc (DJNZ ? addr)
    483484  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
    484485  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
     
    539540    let address ≝ DATA16 (lookup_datalabels trgt) in
    540541      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
    541   | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
     542  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma policy ppc instr
    542543  | Jmp jmp ⇒
    543544    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     
    754755    @(transitive_lt … (assembly1_lt_128 ?))
    755756    @LT)
    756   @pair_elim #x #y #_ cases x normalize nodelta
     757  @pair_elim #x #y #_ cases x cases (policy ppc) normalize nodelta
    757758  try
    758759   (change with (|flatten ? [assembly1 ?]| < ?)
  • src/ASM/Policy.ma

    r2264 r2316  
    186186  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
    187187    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
    188 #program #n #Heq cases daemon (* XXX *)
     188#program #n #Heq inversion (jump_expansion_internal program n) #x cases x -x
     189 #no_ch #pol cases pol normalize nodelta
     190 [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O
     191   #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by /
     192 | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???);
     193   lapply (refl ? (jump_expansion_internal program (S n)))
     194   whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn
     195   normalize nodelta inversion no_ch #Hno_ch normalize nodelta #Seq >Seq
     196   [ #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
     197     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
     198     normalize nodelta #Teq >Teq @pe_refl
     199   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
     200     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
     201     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*)
     202     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
     203     [ normalize nodelta #HSn #Heq #Seq cases Heq
     204     | -Spol #Spol normalize nodelta cases Sno_ch normalize nodelta #HSn #Heq #Seq
     205       [ @pe_refl
     206       | cases daemon
     207       ]
     208     ]
     209   ]
     210 ]
    189211qed.
    190212
     
    445467          [ lapply (jump_pc_equal program (2*|program|))
    446468            >Feq >Geq normalize nodelta #H @H @Heq
     469          | @Heq
    447470          | cases daemon (* true, but have to add this to properties *)
     471          | cases daemon
    448472          | @(proj2 ?? (proj1 ?? HGp))
    449473          ]
  • 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
  • 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
  • src/ASM/Status.ma

    r2272 r2316  
    10761076  ∀i.
    10771077    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
    1078       instruction_has_label id i →
    1079         occurs_exactly_once ASMTag pseudo_instruction id instr_list.
     1078      (instruction_has_label id i →
     1079        occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
     1080      (is_jump_to i id →
     1081        occurs_exactly_once ASMTag pseudo_instruction id instr_list).
    10801082
    10811083definition construct_datalabels: preamble → ? ≝
Note: See TracChangeset for help on using the changeset viewer.