Changeset 2072


Ignore:
Timestamp:
Jun 14, 2012, 4:03:19 AM (5 years ago)
Author:
sacerdot
Message:

We need to import Jaap's invariants now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2071 r2072  
    804804        let 〈ppc,code〉 ≝ ppc_code in
    805805         ppc = bitvector_of_nat … (|pre|) ∧
     806         nat_of_bitvector … (sigma ppc) = |code| ∧
    806807         ∀ppc'.∀ppc_ok'.
    807808          nat_of_bitvector … ppc' < nat_of_bitvector … ppc →
     
    823824      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
    824825  [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
    825     >EQignore_revcode in Hfold; * #Hfold1 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
     826    >EQignore_revcode in Hfold; * * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
    826827    >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    827828    (* CSC: FALSE, NEEDS ADDITIONAL ASSUMPTION *) cases daemon
    828   | % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
     829  | %
     830    [ % // (*CSC: NEW INVARIANT FOR JAAP!*) cases daemon ]
     831    #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
    829832  | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
    830     * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
     833    * * #IH1 #IH3 #IH2 whd % [%
     834    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
     835    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
    831836    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
    832837    cases (le_to_or_lt_eq … LTppc_ppc)
     
    873878      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
    874879      >IH
    875       [2: (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon
     880      [2: >length_reverse <IH3 (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon
    876881      | @shift_nth_prefix
    877882      |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
Note: See TracChangeset for help on using the changeset viewer.