Ignore:
Timestamp:
Jul 17, 2012, 3:23:51 PM (8 years ago)
Author:
sacerdot
Message:

Main lemmas all closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2195 r2197  
    241241           (nat_of_bitvector …
    242242            (add … (sigma ppc) (bitvector_of_nat … j))))))
    243     [1: #j #H <load_code_memory_ok
    244         [ @assembly_ok
    245         | cut (0=|assembled'| → False)
    246           [ #abs <abs in assembly_ok4; >EQlen #abs'
    247             @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY
    248           cases assembly_ok3 -assembly_ok3
    249           [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ]
    250           #EQlen_assembled' <EQlen_assembled'
    251           cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok
    252           cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
    253           whd in match instruction_size; normalize nodelta
    254           >create_label_cost_refl
    255           >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
    256           [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
    257           [2: * #EQ1 #EQ2
    258               @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
    259               [1: @lt_to_lt_nat_of_bitvector_add try assumption
    260                   cases daemon (* XXX: two cases to prove, both true *)
    261               |2: cases daemon (* XXX: use monotonicity of sigma *)
    262               ]
    263           ]
    264           cases (le_to_or_lt_eq … instr_list_ok)
    265           [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
    266               assumption ]
    267           #instr_list_ok' #NO_OVERFLOW
    268           @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
    269           [ @lt_to_lt_nat_of_bitvector_add
    270             [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
    271               / by /
    272             | <EQlen assumption
    273             | assumption
    274             ]
    275           | <EQlen <OK
    276             cases (monotone_sigma ???? sigma_policy_witness
    277              (add … ppc (bitvector_of_nat … 1))
    278              (bitvector_of_nat … (|instr_list|)) ??) try assumption
    279             [ #H @H
    280             |3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse
    281                 try % assumption
    282             |4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    283                 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
    284                 @(transitive_le … instr_list_ok') @le_S_S assumption
    285             | #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
     243    [1: #j #H cases (assembly_ok … H) #K -assembly_ok #assembly_ok <load_code_memory_ok
     244        [ @assembly_ok | skip ]
    286245    |2:
    287246      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
Note: See TracChangeset for help on using the changeset viewer.