Changeset 2225 for src


Ignore:
Timestamp:
Jul 20, 2012, 6:15:40 PM (8 years ago)
Author:
sacerdot
Message:

Minor and major improvements everywhere, shortened proofs.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Policy.ma

    r2211 r2225  
    2727          | Some op ⇒ λp2.if no_ch
    2828            then pi1 ?? (jump_expansion_internal program m)
    29             else pi1 ?? (jump_expansion_step program labels «op,?»)
     29            else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?»)
    3030          ] (refl … z)
    3131  ] (refl … n).
    32 [ normalize nodelta cases (jump_expansion_start program (create_label_map program))
     32[5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) //
     33| normalize nodelta cases (jump_expansion_start program (create_label_map program))
    3334  #x cases x -x
    34   [ #H / by I/
     35  [ #H %
    3536  | #sigma normalize nodelta #H @conj [ @conj
    3637    [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
    … …  
    4041    ]
    4142  ]
    42 | / by I/
     43| %
    4344| cases no_ch in p1; #p1
    4445  [ @(pi2 ?? (jump_expansion_internal program m))
    45   | cases (jump_expansion_step program (create_label_map program) «op,?»)
     46  | cases (jump_expansion_step ???)
    4647    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
    47     [ #_ / by I/
     48    [ #_ %
    4849    | #j2 #H2 @conj [ @conj
    4950      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    … …  
    99100
    100101lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
    101 #program whd #x whd cases x
    102 [ //
    103 | #y @pe_int_refl
    104 ]
     102#program whd #x whd cases x try % #y @pe_int_refl
    105103qed.
    106104
    … …  
    108106#program whd #x #y #Hxy whd cases y in Hxy;
    109107[ cases x
    110   [ //
     108  [ #_ %
    111109  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
    112110  ]
    … …  
    171169     [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ))))
    172170       / by /
    173      | #HN normalize nodelta cases (jump_expansion_step program (create_label_map program) «Npol,?»)     
     171     | #HN normalize nodelta cases (jump_expansion_step ???)     
    174172       #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o
    175173       [ normalize nodelta #_ #H destruct (H)
    … …  
    181179   ]
    182180 ]
    183 qed.
    184        
     181qed.     
    185182
    186183lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    … …  
    189186  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
    190187    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
    191 #program #n #Heq
    192 cases daemon (* XXX *)
     188#program #n #Heq cases daemon (* XXX *)
    193189qed.
    194190
    … …  
    259255    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    260256    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    261     sigma_compact_unsafe program (create_label_map program) p ∧
     257    sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧
    262258    \fst p ≤ 2^16.
    263259  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    264   match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with
     260  match \snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy)) with
    265261  [ None   ⇒ True
    266262  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
    267263  ].
     264[2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) // ]
    268265#program #policy #l elim l -l;
    269266[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
    270267| #h #t #Hind #Hp #acc
    271   lapply (refl ? (jump_expansion_step program (create_label_map program) policy))
    272   cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
     268  inversion (jump_expansion_step ???) #pi1 cases pi1 -pi1 #c #r cases r
    273269  [ / by I/
    274270  | #x normalize nodelta #Hx #Hjeq
    … …  
    331327    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    332328    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    333     sigma_compact_unsafe program (create_label_map program) p ∧
     329    sigma_compact_unsafe program (pi1 … (create_label_map program)) p ∧
    334330    \fst p ≤ 2^16.
    335   match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
     331  match (\snd (pi1 ?? (jump_expansion_step program (pi1 … (create_label_map program)) policy))) with
    336332  [ None ⇒ True
    337333  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
    338 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
    339 cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
     334[2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]
     335#program #policy inversion (jump_expansion_step ???)
    340336#p cases p -p #ch #pol normalize nodelta cases pol
    341337[ / by I/
    … …  
    421417          (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
    422418          (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉)))
    423           (sigma_compact program (create_label_map program) pol))
     419          (sigma_compact program (pi1 … (create_label_map program)) pol))
    424420          (\fst pol ≤ 2^16)
    425421      ].
    … …  
    429425   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
    430426[ #Hex cases Hex -Hex #k #Hk
    431   lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
    432   cases (jump_expansion_internal ? (S (2*|program|))) in ⊢ (???% → %);
     427  inversion (jump_expansion_internal ??)
    433428  #x cases x -x #Gno_ch #Go cases Go normalize nodelta
    434429  [ #H #Heq / by I/
    … …  
    447442        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
    448443        ]
    449         | @(equal_compact_unsafe_compact ?? Fp)
     444        | @(equal_compact_unsafe_compact ? Fp)
    450445          [ lapply (jump_pc_equal program (2*|program|))
    451446            >Feq >Geq normalize nodelta #H @H @Heq
    … …  
    546541        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
    547542        ]
    548         | @(equal_compact_unsafe_compact ?? Fp)
     543        | @(equal_compact_unsafe_compact ? Fp)
    549544          [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
    550545            #H @H #i #Hi
    551             cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     546            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    552547            [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
    553548              >Feq in Geq; normalize nodelta cases Fno_ch
    554549              [ normalize nodelta #Heq
    555550                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
    556               | normalize nodelta cases (jump_expansion_step program (create_label_map program) «Fp,?»)
     551              | normalize nodelta cases (jump_expansion_step ???)
    557552                #x cases x -x #stch #sto normalize nodelta cases sto
    558553                [ normalize nodelta #_ #X destruct (X)
    … …  
    560555                   <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
    561556                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
    562                    lapply (Hfull i Hi Hj)
     557                   lapply (Hfull i Hi ?) [>Hj %]
    563558                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    564559                   #fp #fj #Hfj >Hfj normalize nodelta
    … …  
    570565                 ]
    571566               ]
    572              | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi Hj)
    573                 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
     567             | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2:>Hj %]
     568                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2:>Hj] %
    574569              ]
    575570            | cases daemon (* true, but have to add to properties in some way *)
    … …  
    630625 
    631626(* The glue between Policy and Assembly. *)
    632 (*CSC: modified to really use the specification in Assembly.ma.*)
    633627definition jump_expansion':
    634628∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    … …  
    642636  [ None ⇒ λp.None ?
    643637  | Some x ⇒ λp.Some ?
    644       «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     638      «〈(λppc.let pc ≝ \fst (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in
    645639          bitvector_of_nat 16 pc),
    646          (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     640         (λppc.let jl ≝ \snd (bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉) in
    647641          jmpeqb jl long_jump)〉,?»
    648642  ] (refl ? f).
    … …  
    666660        >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
    667661        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    668         >add_bitvector_of_nat_plus >Hcompact whd in match instruction_size;
    669         normalize nodelta whd in match assembly_1_pseudoinstruction;
    670         normalize nodelta whd in match expand_pseudo_instruction;
    671         normalize nodelta whd in match fetch_pseudo_instruction;
    672         normalize nodelta
    673         lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
    674         cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
    675         #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
    676         >Hli normalize nodelta cases instr
    677         [2,3,6: #x [3: #y] normalize nodelta %
    678         |4,5: #x normalize nodelta
    679           >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
    680           whd in match create_label_map; normalize nodelta
    681           >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    682           cases (bvt_lookup … (bitvector_of_nat ?
    683            (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    684           #lpc #ljl normalize nodelta @refl
    685         |1: #pi cases pi
    686           [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    687             [1,2,3,6,7,24,25: #x #y
    688             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    689             normalize nodelta %
    690           |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
    691             whd in match expand_relative_jump; normalize nodelta
    692             whd in match expand_relative_jump_internal; normalize nodelta
    693             >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
    694             whd in match create_label_map; normalize nodelta
    695             >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    696             cases (bvt_lookup … (bitvector_of_nat ?
    697              (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    698             #lpc #ljl normalize nodelta %
    699           ]
    700         ]
    701       ]
    702     ]
     662        >add_bitvector_of_nat_plus >Hcompact @eq_f @eq_f @eq_f
     663        whd in match (fetch_pseudo_instruction ???); >nth_safe_nth
     664        [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]]
    703665  | (* Basic proof scheme:
    704666       - ppc < |snd program|, hence our instruction is in the program
    … …  
    719681        cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
    720682        [ normalize nodelta #_ #abs cases abs
    721         | #x cases x -x #Spc #Sjl #SEQ normalize nodelta whd in match instruction_size;
    722           normalize nodelta whd in match assembly_1_pseudoinstruction;
    723           normalize nodelta whd in match expand_pseudo_instruction;
    724           normalize nodelta whd in match fetch_pseudo_instruction;
    725           normalize nodelta
    726           lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
    727           cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
    728           #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
    729           >Hli normalize nodelta cases instr
    730           [2,3,6: #x [3: #y] normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    731             normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
    732             [1,3,5: <H
    733               lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    734               >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
    735             |2,4,6: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     683        | #x cases x -x #Spc #Sjl #SEQ normalize nodelta       
     684          #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     685          >nat_of_bitvector_bitvector_of_nat_inverse
     686          [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    736687              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    737               #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
    738             ]
    739           |4,5: #x normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    740             normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
    741             [1,3: <add_bitvector_of_nat_Sm in SEQ;
    742               >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
    743               >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
    744               cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    745               #lpc #ljl normalize nodelta #H <H
    746               lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    747               <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
    748               >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
    749             |2,4: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    750               >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    751               #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
    752             ]
    753           |1: #pi cases pi
    754             [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    755               [1,2,3,6,7,24,25: #x #y
    756               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    757               normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    758               normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
    759               [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    760                 <H lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    761                 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
    762               |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    763                 lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    764                 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    765                 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
    766               ]
    767             |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x]
    768               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    769               normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
    770               [1,3,5,7,9,11,13,15,17: <add_bitvector_of_nat_Sm in SEQ;
    771                 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
    772                 whd in match expand_relative_jump; normalize nodelta
    773                 whd in match expand_relative_jump_internal; normalize nodelta
    774                 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
    775                 cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    776                 #lpc #ljl normalize nodelta #H <H
    777                 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    778                 <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
    779                 >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
    780               |2,4,6,8,10,12,14,16,18:
    781                 lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    782                 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    783                 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
    784               ]
    785             ]
    786           ]
    787         ]
    788       ]
     688              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H ]
     689          lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     690          >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >H -H #H @(transitive_le … H)
     691          cut (∀x,y. x=y → x ≤ y) [ #x #y * %] #eq_to_leq @eq_to_leq @eq_f @eq_f
     692          whd in match (fetch_pseudo_instruction ???); >nth_safe_nth
     693          [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]]
    789694    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
    790695       * until the end of the program *)
    … …  
    812717              >(nth_safe_nth … 〈None ?, Comment []〉)
    813718              cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
    814               #lbl #ins normalize nodelta
    815               whd in match instruction_size;
    816               whd in match assembly_1_pseudoinstruction;
    817               whd in match expand_pseudo_instruction; normalize nodelta
    818               <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
    819               >add_commutative #SEQ cases ins
    820               [2,3,6: #x [3: #y] normalize nodelta #H @H
    821               |4,5: #x normalize nodelta
    822                 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    823                 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
    824                 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    825                 #lpc #ljl normalize nodelta #H @H
    826               |1: #pi cases pi
    827                 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    828                   [1,2,3,6,7,24,25: #x #y
    829                   |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    830                   normalize nodelta #H @H
    831                 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
    832                   whd in match expand_relative_jump;
    833                   whd in match expand_relative_jump_internal; normalize nodelta
    834                   >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    835                   >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
    836                   cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    837                   #lpc #ljl normalize nodelta #H @H
    838                 ]
    839               ]
     719              #lbl #ins normalize nodelta #X @X
    840720            | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
    841721              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
    … …  
    873753                    normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
    874754                    cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
    875                     #lbl #ins normalize nodelta
    876                     whd in match instruction_size;
    877                     whd in match assembly_1_pseudoinstruction;
    878                     whd in match expand_pseudo_instruction; normalize nodelta
    879                     <add_bitvector_of_nat_Sm in SXEQ; >bitvector_of_nat_inverse_nat_of_bitvector
    880                     >add_commutative #SXEQ cases ins
    881                     [2,3,6: #x [3: #y] normalize nodelta #H @(sym_eq ??? H)
    882                     |4,5: #x normalize nodelta
    883                       >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
    884                       >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
    885                       cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    886                       #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
    887                     |1: #pi cases pi
    888                       [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    889                         [1,2,3,6,7,24,25: #x #y
    890                         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
    891                           #H @(sym_eq ??? H)
    892                       |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
    893                         whd in match expand_relative_jump;
    894                         whd in match expand_relative_jump_internal; normalize nodelta
    895                         >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
    896                         >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
    897                         cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    898                         #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
    899                       ]
    900                     ]
     755                    #lbl #ins normalize nodelta #X @sym_eq @X
    901756                  ]
    902757                ]
    … …  
    918773                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    919774                  #lpc #ljl normalize nodelta #H @H
    920                 |1: #pi cases pi
    921                   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    922                     [1,2,3,6,7,24,25: #x #y
    923                     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
    924                     #H @H
    925                   |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
    926                     whd in match expand_relative_jump;
    927                     whd in match expand_relative_jump_internal; normalize nodelta
    928                     >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    929                     >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
    930                     cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    931                     #lpc #ljl normalize nodelta #H @H
    932                   ]
     775                |1: #pi normalize nodelta #X @X
    933776                ]
    934777              ]

  • src/ASM/PolicyFront.ma

    r2222 r2225  
    2222  λx:preinstruction Identifier.
    2323  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
     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
    3434  ].
    3535
    … …  
    3838  match instr with
    3939  [ Instruction i ⇒ is_jump' i
    40   | _             ⇒ False
     40  | _             ⇒ false
    4141  ].
    4242   
    … …  
    4545  match instr with
    4646  [ Instruction i   ⇒ is_jump' i
    47   | Call _ ⇒ True
    48   | Jmp _ ⇒ True
    49   | _ ⇒ False
     47  | Call _ ⇒ true
     48  | Jmp _ ⇒ true
     49  | _ ⇒ false
    5050  ].
    5151
    … …  
    5353  λinstr:pseudo_instruction.
    5454  match instr with
    55   [ Call _ ⇒ True
    56   | _ ⇒ False
     55  [ Call _ ⇒ true
     56  | _ ⇒ false
    5757  ].
    5858 
    … …  
    258258   match j with
    259259   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
    260       ¬is_call instr
     260       bool_to_Prop (¬is_call instr)
    261261   | absolute_jump ⇒  \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧
    262262       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    263        ¬is_relative_jump instr
     263       bool_to_Prop (¬is_relative_jump instr)
    264264   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    265265       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
    … …  
    360360  then short_jump
    361361  else select_call_length labels old_sigma inc_sigma added ppc lbl.
    362  
     362
     363definition destination_of: preinstruction Identifier → option Identifier ≝
     364  λi.
     365  match i with
     366  [ JC j     ⇒ Some ? j
     367  | JNC j    ⇒ Some ? j
     368  | JZ j     ⇒ Some ? j
     369  | JNZ j    ⇒ Some ? j
     370  | JB _ j   ⇒ Some ? j
     371  | JBC _ j  ⇒ Some ? j
     372  | JNB _ j  ⇒ Some ? j
     373  | CJNE _ j ⇒ Some ? j
     374  | DJNZ _ j ⇒ Some ? j
     375  | _        ⇒ None ?
     376  ].
     377
    363378definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
    364379  ℕ → ℕ → preinstruction Identifier → option jump_length ≝
    365380  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
    366   match i with
    367   [ JC j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    368   | JNC j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    369   | JZ j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    370   | JNZ j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    371   | JB _ j   ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    372   | JBC _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    373   | JNB _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    374   | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    375   | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    376   | _        ⇒ None ?
    377   ].
    378 
    379 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
    380 #i cases i
    381 [#id cases id
    382  [1,2,3,6,7,33,34:
    383   #x #y %2 whd in match (is_jump ?); /2 by nmk/
    384  |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
    385   #x %2 whd in match (is_jump ?); /2 by nmk/
    386  |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
    387  |9,10,14,15: #x %1 / by I/
    388  |11,12,13,16,17: #x #y %1 / by I/
    389  ]
    390 |2,3: #x %2 /2 by nmk/
    391 |4,5: #x %1 / by I/
    392 |6: #x #y %2 /2 by nmk/
    393 ]
    394 qed.
     381  match destination_of i with
     382  [ Some j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     383  | None       ⇒ None ?
     384  ].
    395385
    396386(* The first step of the jump expansion: everything to short. *)
    … …  
    599589 #a #b #i cases i
    600590 [1: #pi cases pi
    601    [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    602      try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H
    603    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)
    604      try (#abs normalize in abs; destruct (abs) @I)
    605      cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)
    606      try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)
    607      cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
    608      try ( #abs normalize in abs; destruct (abs) @I)
    609      @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)
    610    ]
     591   try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H
     592   cases a in EQ; cases b #EQ try %
     593   try (normalize in EQ; destruct(EQ) @False)
     594   try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False)
     595   lapply EQ -EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
     596   try (#EQ normalize in EQ; destruct(EQ) @False)
     597   @(subaddressing_mode_elim … a1) #w
     598   #EQ normalize in EQ; destruct(EQ)
    611599  |2,3,6: #x [3: #y] #H cases H
    612   |4,5: #id #_ cases a cases b
    613     [2,3,4,6,11,12,13,15: normalize #H destruct (H)
    614     |1,5,7,8,9,10,14,16,17,18: #H / by refl/
    615     ]
    616   ]
     600  |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H)
     601 ]
    617602qed.
    618603
    … …  
    623608 |4,5: #id #_ cases a cases b / by le_n/
    624609 |1: #pi cases pi
    625    [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    626      try (#x #y #H) try (#x #H) try (#H) cases H
    627    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    628      #_ cases a cases b
    629      [1,4,5,6,7,8,9: / by le_n/
    630      |10,13,14,15,16,17,18: / by le_n/
    631      |19,22,23,24,25,26,27: / by le_n/
    632      |28,31,32,33,34,35,36: / by le_n/
    633      |37,40,41,42,43,44,45: / by le_n/
    634      |46,47,48,49,50,51,52,53,54: / by le_n/
    635      |55,56,57,58,59,60,61,62,63: / by le_n/
    636      |64,65,66,67,68,69,70,71,72: / by le_n/
    637      |73,74,75,76,77,78,79,80,81: / by le_n/
    638      ]
    639      try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n)
    640      cases x * #ad   
    641      try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n)
    642      #z @(subaddressing_mode_elim … z) #w normalize / by /
    643    ]
     610    try (#x #y #H) try (#x #H) try (#H) cases H
     611    -H cases a cases b @leb_true_to_le try %
     612    try (@(subaddressing_mode_elim … x) #w % @False)
     613    cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     614    @(subaddressing_mode_elim … a1) #w %
    644615 ]
    645616qed.
    … …  
    701672              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    702673              cases (get_index' bool 2 0 flags) normalize nodelta
    703               [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     674              [3,4: #H cases (proj2 ?? H)
    704675              |1,2: cases (eq_bv 9 upper ?)
    705676                [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
    … …  
    761732              ]
    762733            ]
    763           |1: #pi cases pi
    764             [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    765               [1,2,3,6,7,24,25: #x #y
    766               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    767               normalize nodelta #H #Heq @refl
    768             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
    769               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    770               #Hj #Heq lapply (Hj x (refl ? x)) -Hj
     734          |1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
     735              [#A #B * / by refl/] #fst_foo
     736              cut (∀x.
     737                    instruction_has_label x (\snd  (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) →
     738               lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     739              [#x #Heq cases (create_label_map program) #clm #Hclm
     740               @le_S_to_le @(proj2 ?? (Hclm x ?))
     741               @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
     742               [ >nat_of_bitvector_bitvector_of_nat_inverse
     743                 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     744               | whd in match fetch_pseudo_instruction; normalize nodelta
     745                 >nth_safe_nth
     746                 [ >nat_of_bitvector_bitvector_of_nat_inverse
     747                   [ @pair_elim // ]
     748                   @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ]
     749                 | assumption ]] #lookup_in_program
     750              -H #pi cases pi
     751              try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try %
     752              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H;
     753              #Hj lapply (Hj x (refl ? x)) -Hj
    771754              whd in match expand_relative_jump; normalize nodelta
    772755              whd in match expand_relative_jump_internal; normalize nodelta
    … …  
    776759              <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
    777760              [1,4,7,10,13,16,19,22,25:
    778                 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
    779                 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
    780                 #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2
     761                >fst_foo @pair_elim #sj_possible #disp #H #H2
    781762                @(pair_replace ?????????? (eq_to_jmeq … H))
    782                 [1,3,5,7,9,11,13,15,17:
    783                   cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    784                   [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
    785                     @le_S_to_le @(proj2 ?? (Hclm x ?))
    786                     @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    787                     [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
    788                       [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    789                     |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
    790                       >nth_safe_nth
    791                       [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
    792                         [1,3,5,7,9,11,13,15,17: >Heq %]
    793                         @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    794                       ]
    795                     ]
    796                     >Heq / by /
    797                   ]
    798                   #X >(le_to_leb_true … X) @refl
    799                 ]
     763                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
     764                  try % >Heq % ]
    800765                >(proj1 ?? H2) try (@refl) normalize nodelta
    801766                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
    … …  
    803768                  @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
    804769                ]
    805               |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/
     770              |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs
    806771              ]
    807               cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
    808               [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
    809               #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
     772              * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
    810773              @(pair_replace ?????????? (eq_to_jmeq … H))
    811                 [1,3,5,7,9,11,13,15,17:
    812                   cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    813                   [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
    814                     @le_S_to_le @(proj2 ?? (Hclm x ?))
    815                     @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    816                     [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
    817                       [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    818                     |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
    819                       >nth_safe_nth
    820                       [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
    821                         [1,3,5,7,9,11,13,15,17: >Heq %]
    822                         @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    823                       ]
    824                     ]
    825                     >Heq / by /
    826                   ]
    827                   #X >(le_to_leb_true … X) @refl
    828                 ]
     774                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
     775                  try % >Heq % ]
    829776                #H2 >H2 try (@refl) normalize nodelta
    830777                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
    … …  
    832779                  [1,2: %] whd in match (map ????); whd in match (flatten ??);
    833780                  whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
    834                   >length_append >length_append @eq_f2 %
    835                 ]
    836               ]
    837             ]
    838           ]
    839         ]
    840       ]
     781                  >length_append >length_append %]]]]]
    841782qed.
    842783
    … …  
    845786 #i cases i
    846787 [2,3,6: #x [3: #y] #Hj #j1 #j2 %
    847  |4,5: #x #Hi cases Hi #abs @⊥ @abs @I
    848  |1: #pi cases pi
    849    [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    850      [1,2,3,6,7,24,25: #x #y
    851      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    852      #Hj #j1 #j2 %
    853    |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
    854      #Hi cases Hi #abs @⊥ @abs @I
    855    ]
    856  ]
    857 qed.
     788 |4,5: #x #Hi cases Hi
     789 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
     790     try % cases Hj ]
     791qed.

  • src/ASM/PolicyStep.ma

    r2220 r2225  
    44include alias "basics/logic.ma".
    55
     6lemma not_is_jump_to_destination_of_Nome:
     7 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None ….
     8 * try (#x #y #H) try (#y #H) try #H cases H %
     9qed.
     10
    611lemma jump_expansion_step1:
    7  ∀program : Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l.
    8  ∀prefix,x,tl. pi1 … program=prefix@[x]@tl →
     12 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
    913 ∀labels: label_map.
    1014 ∀old_sigma : ppc_pc_map.
    … …  
    3842   = policy.
    3943  not_jump_default (prefix@[〈label,instr〉]) policy.
    40  #program #prefix #x #tl #prf #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
    41  #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 
     44 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
     45 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
    4246 #i >append_length <commutative_plus #Hi normalize in Hi;
    4347 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    … …  
    4650     [ >(nth_append_first ? i prefix ?? Hi)
    4751       @(Hpolicy i Hi)
    48      | @bitvector_of_nat_abs
    49        [ @(transitive_lt ??? Hi) ]
    50        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    51          @le_plus_n_r
    52        | @lt_to_not_eq @Hi
    53        ]
     52     | @bitvector_of_nat_abs try assumption
     53       [ @(transitive_lt ??? Hi) assumption ]
     54       @lt_to_not_eq @Hi
    5455     ]
    55    | @bitvector_of_nat_abs
    56      [ @(transitive_lt ??? Hi) @le_S_to_le ]
    57      [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
    58        <plus_n_Sm @le_S_S @le_plus_n_r
    59      | @lt_to_not_eq @le_S @Hi
    60      ]
     56   | @bitvector_of_nat_abs try assumption
     57     [ @(transitive_lt ??? Hi) assumption ]
     58     @lt_to_not_eq @le_S @Hi
    6159   ]
    6260 | <Heq2 >Hi >lookup_insert_miss
    6361   [ >lookup_insert_hit cases instr in Heq1;
    6462     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    65      |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
    66        [1,3: <minus_n_n whd in match (nth ????); %
    67        |2,4: @le_n
    68        ]
    69      |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
    70        [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    71          [1,2,3,6,7,24,25: #x #y
    72          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
    73          <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    74        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
    75          #_ #H @⊥ cases H #H2 @H2 %
    76        ]
    77      ]
    78    | @bitvector_of_nat_abs
    79      [ @le_S_to_le ]
    80      [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
    81        >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    82      | @lt_to_not_eq @le_n
    83      ]
    84    ]
    85  ]
     63     |4,5: #x normalize nodelta #Heq1 >nth_append_second try %
     64           <minus_n_n #abs cases abs
     65     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     66         #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
     67         >not_is_jump_to_destination_of_Nome in H; normalize nodelta // ]         
     68   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
    8669qed.
     70
     71lemma jump_expansion_step2:
     72 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
     73 ∀labels : label_map.
     74 ∀old_sigma : ppc_pc_map.
     75 ∀inc_pc : ℕ.
     76 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
     77 ∀Hpolicy1 :
     78  \fst  (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O.
     79 ∀Hpolicy2:
     80   inc_pc =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
     81 ∀policy : ppc_pc_map.
     82 ∀new_length : jump_length.
     83 ∀isize : ℕ.
     84 ∀Heq2 :
     85  〈inc_pc+isize,
     86   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     87   〈inc_pc+isize,
     88   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     89               (\snd  old_sigma) 〈O,short_jump〉)〉
     90   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     91    〈inc_pc,new_length〉 inc_sigma)〉
     92   = policy.
     93 \fst  (lookup … (bitvector_of_nat … O) (\snd  policy) 〈O,short_jump〉) = O.
     94 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc
     95 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2
     96 <Heq2 >lookup_insert_miss
     97 [ cases (decidable_eq_nat 0 (|prefix|))
     98   [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1
     99   | #Hneq >lookup_insert_miss
     100     [ @Hpolicy1
     101     | @bitvector_of_nat_abs try assumption @lt_O_S ]]
     102 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ]
     103qed.
     104
     105(*
     106lemma jump_expansion_step3:
     107(*
     108 program :
     109  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
     110 labels :
     111  (Σlm:label_map
     112   .(∀l:identifier ASMTag
     113     .occurs_exactly_once ASMTag pseudo_instruction l program
     114      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
     115       =address_of_word_labels_code_mem program l))*)
     116 ∀old_sigma :
     117   Σpolicy:ppc_pc_map
     118   .True(*not_jump_default program policy
     119    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     120                 〈O,short_jump〉)
     121     =O
     122    ∧\fst  policy
     123     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
     124                  (\snd  policy) 〈O,short_jump〉)
     125    ∧sigma_compact_unsafe program labels policy
     126    ∧\fst  policy≤ 2 \sup 16*).
     127 ∀prefix : list (option Identifier×pseudo_instruction). (*
     128 x : (option Identifier×pseudo_instruction)
     129 tl : (list (option Identifier×pseudo_instruction))
     130 prf : (program=prefix@[x]@tl)
     131 acc :
     132  (Σx0:ℕ×ppc_pc_map
     133   .(let 〈added,policy〉 ≝x0 in 
     134     not_jump_default prefix policy
     135     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     136                  〈O,short_jump〉)
     137      =O
     138     ∧\fst  policy
     139      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     140                   (\snd  policy) 〈O,short_jump〉)
     141     ∧jump_increase prefix old_sigma policy
     142     ∧sigma_compact_unsafe prefix labels policy
     143     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     144     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     145     ∧out_of_program_none prefix policy
     146     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     147                  (\snd  policy) 〈O,short_jump〉)
     148      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     149                   (\snd  old_sigma) 〈O,short_jump〉)
     150       +added
     151     ∧sigma_safe prefix labels added old_sigma policy))
     152 inc_added : ℕ
     153 inc_pc_sigma : ppc_pc_map
     154 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     155 ∀label : option Identifier.
     156 ∀instr : pseudo_instruction.(*
     157 p1 : (x≃〈label,instr〉)
     158 add_instr ≝
     159  match instr
     160   in pseudo_instruction
     161   return λ_:pseudo_instruction.(option jump_length)
     162   with 
     163  [Instruction (i:(preinstruction Identifier))⇒
     164   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     165   (|prefix|) i
     166  |Comment (_:String)⇒None jump_length
     167  |Cost (_:costlabel)⇒None jump_length
     168  |Jmp (j:Identifier)⇒
     169   Some jump_length
     170   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     171  |Call (c:Identifier)⇒
     172   Some jump_length
     173   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     174  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     175 inc_pc : ℕ
     176 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
     177 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
     178 old_pc : ℕ
     179 old_length : jump_length
     180 Holdeq :
     181  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     182   〈O,short_jump〉
     183   =〈old_pc,old_length〉)
     184 Hpolicy :
     185  (not_jump_default prefix 〈inc_pc,inc_sigma〉
     186   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     187                〈O,short_jump〉)
     188    =O
     189   ∧inc_pc
     190    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     191                 〈O,short_jump〉)
     192   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     193   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
     194   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     195   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     196   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
     197   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     198                〈O,short_jump〉)
     199    =old_pc+inc_added
     200   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
     201 added : ℕ*)
     202 ∀policy : ppc_pc_map.
     203 (*new_length : jump_length
     204 isize : ℕ
     205 Heq1 :
     206  (match 
     207   match instr
     208    in pseudo_instruction
     209    return λ_:pseudo_instruction.(option jump_length)
     210    with 
     211   [Instruction (i:(preinstruction Identifier))⇒
     212    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     213    (|prefix|) i
     214   |Comment (_:String)⇒None jump_length
     215   |Cost (_:costlabel)⇒None jump_length
     216   |Jmp (j:Identifier)⇒
     217    Some jump_length
     218    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     219   |Call (c:Identifier)⇒
     220    Some jump_length
     221    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     222   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     223    in option
     224    return λ_0:(option jump_length).(jump_length×ℕ)
     225    with 
     226   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     227   |Some (pl:jump_length)⇒
     228    〈max_length old_length pl,
     229    instruction_size_jmplen (max_length old_length pl) instr〉]
     230   =〈new_length,isize〉)
     231 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
     232 prefix_ok : (|prefix|< 2 \sup 16 )
     233 Heq2a :
     234  (match 
     235   match instr
     236    in pseudo_instruction
     237    return λ_0:pseudo_instruction.(option jump_length)
     238    with 
     239   [Instruction (i:(preinstruction Identifier))⇒
     240    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     241    (|prefix|) i
     242   |Comment (_0:String)⇒None jump_length
     243   |Cost (_0:costlabel)⇒None jump_length
     244   |Jmp (j:Identifier)⇒
     245    Some jump_length
     246    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     247   |Call (c:Identifier)⇒
     248    Some jump_length
     249    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     250   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
     251    in option
     252    return λ_0:(option jump_length).ℕ
     253    with 
     254   [None⇒inc_added
     255   |Some (x0:jump_length)⇒
     256    inc_added+(isize-instruction_size_jmplen old_length instr)]
     257   =added)
     258 Heq2b :
     259  (〈inc_pc+isize,
     260   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     261   〈inc_pc+isize,
     262   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     263               (\snd  old_sigma) 〈O,short_jump〉)〉
     264   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     265    〈inc_pc,new_length〉 inc_sigma)〉
     266   =policy)*)
     267 jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
     268 #old_sigma #prefix #label #instr #policy
     269    #i >append_length >commutative_plus #Hi normalize in Hi;
     270    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     271    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     272      [ (* USE[pass]: jump_increase *)
     273        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
     274        <(proj2 ?? (pair_destruct ?????? Heq2))
     275        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     276        [ >lookup_insert_miss
     277          [ @pair_elim #pc #j #EQ2 #X @X
     278          | @bitvector_of_nat_abs
     279            [ @(transitive_lt ??? Hi) ]
     280            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     281              @le_S_S @le_plus_n_r
     282            | @lt_to_not_eq @Hi
     283            ]
     284          ]
     285        | @bitvector_of_nat_abs
     286          [ @(transitive_lt ??? Hi) @le_S_to_le ]
     287          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     288            >append_length @le_S_S <plus_n_Sm @le_plus_n_r
     289          | @lt_to_not_eq @le_S @Hi
     290          ]
     291        ]
     292      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
     293        >lookup_insert_miss
     294        [ >lookup_insert_hit cases (dec_is_jump instr)
     295          [ cases instr in Heq1; normalize nodelta
     296            [ #pi cases pi
     297              [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     298                [1,2,3,6,7,24,25: #x #y
     299                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
     300              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     301                whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
     302                #_ <(proj1 ?? (pair_destruct ?????? Heq1))
     303                @jmpleq_max_length
     304              ]
     305            |2,3,6: #x [3: #y] #_ #Hj cases Hj
     306            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     307            ]
     308          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
     309            [ #pi cases pi
     310              [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     311                [1,2,3,6,7,24,25: #x #y
     312                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     313                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
     314                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     315                (* USE: not_jump_default (from old_sigma) *)
     316                lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
     317                [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
     318                  >prf >nth_append_second
     319                  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
     320                    <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     321                  |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
     322                    @le_n
     323                  ]
     324                |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
     325                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     326                |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
     327                  >Holdeq #EQ2 >EQ2 %2 @refl
     328                ]
     329              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     330                #_ #_ #abs @⊥ @(absurd ? I abs)
     331              ]
     332            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     333              (* USE: not_jump_default (from old_sigma) *)
     334              lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
     335              [1,4,7: >prf >nth_append_second
     336                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     337                |2,4,6: @le_n
     338                ]
     339              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     340              |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl
     341              ]
     342            |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs)
     343            ]
     344          ]
     345        | @bitvector_of_nat_abs
     346          [ @le_S_to_le ]
     347          [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf
     348            >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     349          | @lt_to_not_eq @le_n
     350          ]
     351        ]
     352      ]
     353    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     354      normalize nodelta
     355      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
     356      #a #b normalize nodelta %2 @refl
     357    ]
     358  ]
     359qed.*)
    87360
    88361(* One step in the search for a jump expansion fixpoint. *)
    … …  
    190463  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    191464    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    192     cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     465    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    193466    [ #Hj
    194467      (* USE: policy_increase (from fold) *)
    195468      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
    196       lapply (Habs i Hi Hj)
     469      lapply (Habs i Hi ?) [ >Hj %]
    197470      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
    198471      #opc #oj
    … …  
    204477    | #Hnj
    205478      (* USE: not_jump_default (from fold and old_sigma) *)
    206       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)
    207       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
    208       @refl
     479      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
     480      [2: >Hnj %]
     481      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
     482      >Hnj %
    209483    ]
    210484  | #abs >abs in Hsig; #Hsig
    … …  
    232506  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
    233507  #Heq1 #Heq2
    234   @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     508 cut (S (|prefix|) < 2^16)
     509 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
     510   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
     511 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
     512 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
     513  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    235514  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    236515   * commented out for full proofs, but this needs a lot of memory and time *)
    237516  [ (* not_jump_default *)
    238     cases (pair_destruct ?????? Heq2) -Heq2 #_ #Heq2
    239     @(jump_expansion_step1 … prf … Heq1 Heq2)
     517    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
    240518    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    241519  | (* 0 ↦ 0 *)
    242     <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    243     [ cases (decidable_eq_nat 0 (|prefix|))
    244       [ #Heq <Heq >lookup_insert_hit
    245         (* USE: inc_pc = fst policy *)
    246         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    247         <Heq
    248         (* USE[pass]: 0 ↦ 0 *)
    249         @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    250       | #Hneq >lookup_insert_miss
    251         [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    252         | @bitvector_of_nat_abs
    253           [3: @Hneq]
    254         ]
    255       ]
    256     | @bitvector_of_nat_abs
    257       [3: @lt_to_not_eq @lt_O_S ]
    258     ]
    259     [1,3: @lt_O_S
    260     |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    261       [2: <plus_n_Sm @le_S_S]
    262       @le_plus_n_r
    263     ]
    264   ]
    265   | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
    266     >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    267   ]
    268   | (* jump_increase *) (* cases daemon *)
    269     #i >append_length >commutative_plus #Hi normalize in Hi;
    270     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    271     [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    272       [ (* USE[pass]: jump_increase *)
    273         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
    274         <(proj2 ?? (pair_destruct ?????? Heq2))
    275         @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    276         [ >lookup_insert_miss
    277           [ @pair_elim #pc #j #EQ2 #X @X
    278           | @bitvector_of_nat_abs
    279             [ @(transitive_lt ??? Hi) ]
    280             [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    281               @le_S_S @le_plus_n_r
    282             | @lt_to_not_eq @Hi
    283             ]
    284           ]
    285         | @bitvector_of_nat_abs
    286           [ @(transitive_lt ??? Hi) @le_S_to_le ]
    287           [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    288             >append_length @le_S_S <plus_n_Sm @le_plus_n_r
    289           | @lt_to_not_eq @le_S @Hi
    290           ]
    291         ]
    292       | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
    293         >lookup_insert_miss
    294         [ >lookup_insert_hit cases (dec_is_jump instr)
    295           [ cases instr in Heq1; normalize nodelta
    296             [ #pi cases pi
    297               [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    298                 [1,2,3,6,7,24,25: #x #y
    299                 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
    300               |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    301                 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
    302                 #_ <(proj1 ?? (pair_destruct ?????? Heq1))
    303                 @jmpleq_max_length
    304               ]
    305             |2,3,6: #x [3: #y] #_ #Hj cases Hj
    306             |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    307             ]
    308           | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
    309             [ #pi cases pi
    310               [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    311                 [1,2,3,6,7,24,25: #x #y
    312                 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    313                 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    314                 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    315                 (* USE: not_jump_default (from old_sigma) *)
    316                 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    317                 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    318                   >prf >nth_append_second
    319                   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    320                     <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    321                   |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    322                     @le_n
    323                   ]
    324                 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    325                   >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    326                 |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    327                   >Holdeq #EQ2 >EQ2 %2 @refl
    328                 ]
    329               |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    330                 #_ #_ #abs @⊥ @(absurd ? I abs)
    331               ]
    332             |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    333               (* USE: not_jump_default (from old_sigma) *)
    334               lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    335               [1,4,7: >prf >nth_append_second
    336                 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    337                 |2,4,6: @le_n
    338                 ]
    339               |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    340               |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl
    341               ]
    342             |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs)
    343             ]
    344           ]
    345         | @bitvector_of_nat_abs
    346           [ @le_S_to_le ]
    347           [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf
    348             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    349           | @lt_to_not_eq @le_n
    350           ]
    351         ]
    352       ]
    353     | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    354       normalize nodelta
    355       cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
    356       #a #b normalize nodelta %2 @refl
    357     ]
    358   ]
    359   | (* sigma_compact_unsafe *)
     520    @(jump_expansion_step2 … Heq2b) try assumption
     521    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
     522    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
     523  | (* inc_pc = fst of policy *)
     524    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
     525  | (* jump_increase *)
     526    cases daemon (*XXX*)
     527  | (* sigma_compact_unsafe *) cases daemon (*
    360528    #i >append_length <commutative_plus #Hi normalize in Hi;
    361529    <(proj2 ?? (pair_destruct ?????? Heq2))
    … …  
    461629      ]
    462630    ]
    463   ]
    464   | (* policy_jump_equal → added = 0 *)
     631  ] *)
     632  | (* policy_jump_equal → added = 0 *) cases daemon (*
    465633    <(proj2 ?? (pair_destruct ?????? Heq2))
    466634    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
    … …  
    530698      ]
    531699    ]
    532   ]
     700  ] *)
    533701  | (* added = 0 → policy_pc_equal *) cases daemon
    534702    (* USE[pass]: added = 0 → policy_pc_equal *)
    … …  
    831999      ]
    8321000    ] *)
    833   ]
    8341001  | (* out_of_program_none *) cases daemon
    8351002    (* #i #Hi2 >append_length <commutative_plus @conj
    … …  
    8701037      ]
    8711038    ] *)
    872   ]
    8731039  | (* lookup p = lookup old_sigma + added *) cases daemon
    8741040    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
    … …  
    10031169      ]
    10041170    ] *)
    1005   ]
    10061171  | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
    10071172    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    … …  
    10241189                    [1,4,7: *)
    10251190                 
    1026   ]        
    1027 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     1191  ]       
     1192| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    10281193  [ #i cases i
    10291194    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    10301195    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    10311196    ]
     1197  | >lookup_insert_hit @refl
    10321198  | >lookup_insert_hit @refl
    1033   ]
    1034   | >lookup_insert_hit @refl
    1035   ]
    10361199  | #i #Hi <(le_n_O_to_eq … Hi)
    10371200    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
    10381201    #a #b normalize nodelta %2 @refl
    1039   ]
    10401202  | #i cases i
    10411203    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    10421204    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    10431205    ]
    1044   ]
    10451206  | #_ %
    1046   ]
    10471207  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
    10481208    (* USE: 0 ↦ 0 (from old_sigma) *)
    10491209    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
    1050   ]
    10511210  | #i cases i
    10521211    [ #Hi2 @conj
    … …  
    10661225      ]
    10671226    ]
    1068   ]
    10691227  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
    10701228    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
    1071   ]
    10721229  | #i cases i
    10731230    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    … …  
    10771234]
    10781235qed.
    1079 
Note: See TracChangeset for help on using the changeset viewer.