Changeset 2156


Ignore:
Timestamp:
Jul 6, 2012, 11:30:52 AM (5 years ago)
Author:
sacerdot
Message:

One more invariant, one less daemon.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2154 r2156  
    775775         ppc = bitvector_of_nat … (|pre|) ∧
    776776         |code| ≤ 2^16 ∧
     777         (|code| = 2^16 → |pre| = |instr_list|) ∧
    777778         (nat_of_bitvector … (sigma ppc) = |code| ∨
    778779          sigma ppc = zero … ∧ |code| = 2^16) ∧
     
    798799  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    799800    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
    800     cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold3 #Hfold2 whd
     801    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 #Hfold2 whd
    801802    <eq_create_label_cost_map whd %
    802803    [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
     
    808809      | #Hfold5 %2 <Hfold1 assumption ]]
    809810  | * #sigma_pol_ok1 #_ #instr_list_ok %
    810     [ % % // >sigma_pol_ok1 % ]
     811    [ % % [%] // [#abs change with (0=S ?) in abs; destruct(abs) | >sigma_pol_ok1 % ]]
    811812    #ppc' #ppc_ok' #abs @⊥ cases abs
    812813     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
     
    814815  | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
    815816    #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
    816     * * #IH1 #IH2 *
    817     [2: #H @⊥ cases daemon (*CSC: impossible case, using Jaaps's ? *)]
     817    * * * #IH1 #IH2 #IH4 *
     818    [2: * #_ #H @⊥ lapply (IH4 H) >prf >length_append
     819        >(plus_n_O (|prefix|)) in ⊢ (??%? → ?); #X
     820        lapply (injective_plus_r … X) >length_append normalize #abs' destruct(abs')]
    818821    #IH3 #IH5
    819822    cut (|prefix| < |instr_list|)
     
    835838    lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta
    836839    cut (pc_delta < 2^16)
    837     [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok
    838     % [ % [% ] ]
     840    [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok check fst_eq
     841    cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
     842    [ whd in match instruction_size; normalize nodelta
     843      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
     844    #EQpc_delta2
     845    % [ % [% [% ] ] ]
    839846    [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
    840847    | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*)
     848    | lapply (sigma_pol_ok2 … ppc_ok) * #sigma_pol_ok3
     849      <eq_fetch_pseudo_instruction <eq_create_label_cost_map #sigma_pol4
     850       >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta >EQpc_delta2
     851       #abs >abs in sigma_pol4; *
     852       [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
     853       | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
     854         >nat_of_bitvector_bitvector_of_nat_inverse // ]
    841855    | cases (sigma_pol_ok2 … ppc_ok)
    842856      whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction
Note: See TracChangeset for help on using the changeset viewer.