Changeset 2228 for src/ASM


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

Further proof reduction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2225 r2228  
    647647[ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
    648648  #x #y #Hx normalize nodelta >Hx / by refl/
    649 | #ppc #ppc_ok normalize nodelta @conj
     649| #ppc #ppc_ok normalize nodelta
     650  >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
     651       \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉))
     652  [2: whd in match fetch_pseudo_instruction; normalize nodelta
     653   >(nth_safe_nth … 〈None ?, Comment []〉)
     654   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     655   #lbl #ins % ]
     656  @conj
    650657  [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok)
    651658    >bitvector_of_nat_inverse_nat_of_bitvector
    652     lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
    653     [ #Hl normalize nodelta #abs cases abs
    654     | #x cases x -x #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
     659    inversion (lookup_opt ????) normalize nodelta
     660    [ #Hl #abs cases abs
     661    | * #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
    655662      >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
    656       lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol))
    657       cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %);
    658       [ #Hl normalize nodelta #abs cases abs
    659       | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact
     663      inversion (lookup_opt ????) normalize nodelta
     664      [ #_ #abs cases abs
     665      | * #Spc #Sjl #SHl normalize nodelta #Hcompact
    660666        >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
    661667        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    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 // ]]
     668        >add_bitvector_of_nat_plus >Hcompact % ]]
    665669  | (* Basic proof scheme:
    666670       - ppc < |snd program|, hence our instruction is in the program
     
    675679      lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
    676680      >bitvector_of_nat_inverse_nat_of_bitvector
    677       lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
    678       [ normalize nodelta #_ #abs cases abs
    679       | #x cases x -x #pc #jl #EQ normalize nodelta
    680         lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
    681         cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
    682         [ normalize nodelta #_ #abs cases abs
    683         | #x cases x -x #Spc #Sjl #SEQ normalize nodelta       
    684           #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     681      inversion (lookup_opt ????) normalize nodelta
     682      [ #_ #abs cases abs
     683      | * #pc #jl #Hl normalize nodelta
     684        inversion (lookup_opt ????) normalize nodelta
     685        [ #_ #abs cases abs
     686        | * #Spc #Sjl #SHl normalize nodelta #Hcompact       
     687          >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
    685688          >nat_of_bitvector_bitvector_of_nat_inverse
    686689          [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
    687               >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     690              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
    688691              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H ]
    689692          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 // ]]
     693          >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) >Hcompact #X @X ]]
    694694    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
    695695       * until the end of the program *)
     
    712712            [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
    713713              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1
    714               >Hc in HSpc;
    715               whd in match create_label_map;
    716               whd in match fetch_pseudo_instruction; normalize nodelta
    717               >(nth_safe_nth … 〈None ?, Comment []〉)
    718               cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
    719               #lbl #ins normalize nodelta #X @X
     714              >Hc in HSpc; #X @X
    720715            | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
    721716              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
    722               [ #ppc' #ppc_ok' #Hppc'
     717              [2: >Hc in Hspc; #X @X
     718              | #ppc' #ppc_ok' #Hppc'
    723719                (* S ppc < ppc' < |\snd program| *)
    724720                (* lookup S ppc = 2^16 *)
     
    727723                lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok')
    728724                >bitvector_of_nat_inverse_nat_of_bitvector
    729                 lapply (refl ? (lookup_opt … ppc' fpol))
    730                 cases (lookup_opt … ppc' fpol) in ⊢ (???% → %);
    731                 [ normalize nodelta #_ #abs cases abs
    732                 | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta
    733                   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol))
    734                   cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %);
    735                   [ normalize nodelta #_ #abs cases abs
    736                   | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta
     725                inversion (lookup_opt ????) normalize nodelta
     726                [ #_ #abs cases abs
     727                | * #xpc #xjl #XEQ normalize nodelta
     728                  inversion (lookup_opt ????) normalize nodelta
     729                  [ #_ #abs cases abs
     730                  | * #Sxpc #Sxjl #SXEQ normalize nodelta
    737731                    #Hpcompact
    738732                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
     
    756750                  ]
    757751                ]
    758               | >Hc in Hspc;
    759                 whd in match create_label_map;
    760                 whd in match fetch_pseudo_instruction; normalize nodelta
    761                 >(nth_safe_nth … 〈None ?, Comment []〉)
    762                 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
    763                  #lbl #ins normalize nodelta
    764                 whd in match instruction_size;
    765                 whd in match assembly_1_pseudoinstruction;
    766                 whd in match expand_pseudo_instruction; normalize nodelta
    767                 <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
    768                 >add_commutative #SEQ cases ins
    769                 [2,3,6: #x [3: #y] normalize nodelta #H @H
    770                 |4,5: #x normalize nodelta
    771                   >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    772                   >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
    773                   cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
    774                   #lpc #ljl normalize nodelta #H @H
    775                 |1: #pi normalize nodelta #X @X
    776                 ]
    777752              ]
    778753            ]
Note: See TracChangeset for help on using the changeset viewer.