Changeset 2225 for src/ASM/Policy.ma


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

Minor and major improvements everywhere, shortened proofs.

File:
1 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              ]
Note: See TracChangeset for help on using the changeset viewer.