Changeset 2230 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jul 23, 2012, 10:35:43 AM (7 years ago)
Author:
sacerdot
Message:

Glue proof maximally simplified or sort of.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2229 r2230  
    653653   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
    654654   #lbl #ins % ]
     655  lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) >bitvector_of_nat_inverse_nat_of_bitvector
     656  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
     657  * #pc #jl #Hl normalize nodelta
     658  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
     659  * #Spc #Sjl #SHL lapply SHL
     660  <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
     661  #SHl normalize nodelta #Hcompact
    655662  @conj
    656   [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
    657     >bitvector_of_nat_inverse_nat_of_bitvector
    658     inversion (lookup_opt ????) normalize nodelta
    659     [ #Hl #abs cases abs
    660     | * #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
    661       >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
    662       inversion (lookup_opt ????) normalize nodelta
    663       [ #_ #abs cases abs
    664       | * #Spc #Sjl #SHl normalize nodelta #Hcompact
    665         >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
    666         >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    667         >add_bitvector_of_nat_plus >Hcompact % ]]
     663  [ >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉)
     664    >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
     665    >add_bitvector_of_nat_plus >Hcompact %
    668666  | (* Basic proof scheme:
    669667       - ppc < |snd program|, hence our instruction is in the program
     
    676674    elim (le_to_or_lt_eq … Hfpol4) #Hfpc
    677675    [ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2
    678       lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
    679       >bitvector_of_nat_inverse_nat_of_bitvector
    680       inversion (lookup_opt ????) normalize nodelta
    681       [ #_ #abs cases abs
    682       | * #pc #jl #Hl normalize nodelta
    683         inversion (lookup_opt ????) normalize nodelta
    684         [ #_ #abs cases abs
    685         | * #Spc #Sjl #SHl normalize nodelta #Hcompact       
    686           >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    687           >nat_of_bitvector_bitvector_of_nat_inverse
    688           [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    689               >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
    690               #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ]
    691           lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
    692           >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) >Hcompact #X @X ]]
     676      >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
     677      >nat_of_bitvector_bitvector_of_nat_inverse
     678      [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     679          >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
     680          #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @H ]
     681      lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     682      >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >Hcompact #X @X
    693683    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
    694684       * until the end of the program *)
    695685      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 ?)))
    696       [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
    697         >bitvector_of_nat_inverse_nat_of_bitvector
    698         lapply (refl ? (lookup_opt … ppc fpol))
    699         cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
    700         [ #_ normalize nodelta #abs cases abs
    701         | #x cases x -x #pc #jl #EQ normalize nodelta
    702           lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
    703           cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
    704           [ #_ normalize nodelta #abs cases abs
    705           | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hc
    706             >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta
    707             >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
    708             >nat_of_bitvector_bitvector_of_nat_inverse
    709             [2: <Hfpc >Hfpol2 @Hpc ]
    710             elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
    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'
     686      [ >bitvector_of_nat_inverse_nat_of_bitvector
     687        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta
     688        >nat_of_bitvector_bitvector_of_nat_inverse
     689        [2: <Hfpc >Hfpol2 @Hpc ]
     690        elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
     691        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc
     692        [ %1 >Hcompact in HSpc; #X @X
     693        | %2 @conj
     694          [2: >Hcompact in HSpc; #X @X
     695          | #ppc' #ppc_ok' #Hppc'
    716696                (* S ppc < ppc' < |\snd program| *)
    717697                (* lookup S ppc = 2^16 *)
     
    728708                    #Hpcompact
    729709                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
    730                     >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >HSpc #Hle1
     710                    >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
    731711                    lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
    732712                    <Hfpol2 >Hfpc #Hle2
     
    735715                    >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
    736716                    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')
    737                     >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >HSpc #Hle1
     717                    >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
    738718                    lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
    739719                    <Hfpol2 >Hfpc #Hle2
     
    747727                  ]
    748728                ]
    749               ]
    750             ]
    751729          ]
    752730        ]
    753731      | >bitvector_of_nat_inverse_nat_of_bitvector
    754         <Hfpol2 >Hfpc
    755         cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc
     732        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc
     733        %1 >Hpc
    756734        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
    757735        <plus_O_n whd in match instruction_size; normalize nodelta
    758         lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?))
    759         [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %);
    760           #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
    761           #Hli >Hli
    762           lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
    763           [5: >Hass / by /
    764           ]
    765         ]
     736        inversion (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?)
     737        #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
     738        #Hli >Hli
     739        lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
     740        [5: >Hass / by / ]
    766741      ]
    767742    ]
Note: See TracChangeset for help on using the changeset viewer.