Changeset 2229 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jul 20, 2012, 9:38:04 PM (7 years ago)
Author:
sacerdot
Message:

More cleaning up, ready for more aggressive factorization.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2228 r2229  
    643643normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
    644644lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
    645 #fpc #fpol #Hfpol
     645#fpc #fpol #Hfpol cases Hfpol ** #Hfpol1 #Hfpol2 #Hfpol3 #Hfpol4
    646646@conj
    647 [ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
    648   #x #y #Hx normalize nodelta >Hx / by refl/
     647[ >Hfpol1 %
    649648| #ppc #ppc_ok normalize nodelta
    650649  >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
     
    655654   #lbl #ins % ]
    656655  @conj
    657   [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok)
     656  [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
    658657    >bitvector_of_nat_inverse_nat_of_bitvector
    659658    inversion (lookup_opt ????) normalize nodelta
     
    675674         through the next non-zero instruction)
    676675    *)
    677     elim (le_to_or_lt_eq … (proj2 ?? Hfpol)) #Hfpc
    678     [ %1 @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol)))
    679       lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
     676    elim (le_to_or_lt_eq … Hfpol4) #Hfpc
     677    [ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2
     678      lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
    680679      >bitvector_of_nat_inverse_nat_of_bitvector
    681680      inversion (lookup_opt ????) normalize nodelta
     
    689688          [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    690689              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
    691               #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H ]
     690              #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ]
    692691          lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    693692          >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) >Hcompact #X @X ]]
     
    695694       * until the end of the program *)
    696695      elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
    697       [ lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
     696      [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
    698697        >bitvector_of_nat_inverse_nat_of_bitvector
    699698        lapply (refl ? (lookup_opt … ppc fpol))
     
    708707            >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
    709708            >nat_of_bitvector_bitvector_of_nat_inverse
    710             [2: <Hfpc >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @Hpc ]
     709            [2: <Hfpc >Hfpol2 @Hpc ]
    711710            elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
    712             [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
    713               >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1
    714               >Hc in HSpc; #X @X
    715             | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
    716               >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
    717               [2: >Hc in Hspc; #X @X
    718               | #ppc' #ppc_ok' #Hppc'
     711            <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc
     712            [ %1 >Hc in HSpc; #X @X
     713            | %2 @conj
     714              [2: >Hc in HSpc; #X @X
     715              | #ppc' #ppc_ok' #Hppc'
    719716                (* S ppc < ppc' < |\snd program| *)
    720717                (* lookup S ppc = 2^16 *)
    721718                (* lookup |\snd program| = 2^16 *)
    722719                (* lookup ppc' = 2^16 → instruction size = 0 *)
    723                 lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok')
     720                lapply (Hfpol3 (nat_of_bitvector ? ppc') ppc_ok')
    724721                >bitvector_of_nat_inverse_nat_of_bitvector
    725722                inversion (lookup_opt ????) normalize nodelta
     
    731728                    #Hpcompact
    732729                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
    733                     >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
     730                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >HSpc #Hle1
    734731                    lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
    735                     <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
     732                    <Hfpol2 >Hfpc #Hle2
    736733                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
    737734                    >bitvector_of_nat_inverse_nat_of_bitvector
    738735                    >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
    739736                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
    740                     >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
     737                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >HSpc #Hle1
    741738                    lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
    742                     <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
     739                    <Hfpol2 >Hfpc #Hle2
    743740                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
    744741                    >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
     
    755752        ]
    756753      | >bitvector_of_nat_inverse_nat_of_bitvector
    757         <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     754        <Hfpol2 >Hfpc
    758755        cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc
    759756        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
Note: See TracChangeset for help on using the changeset viewer.