Changeset 2197


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

Main lemmas all closed.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2194 r2197  
    917917          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    918918         |assembledi| ≤ |assembled| ∧
    919          ∀j:nat. ∀H: j < |assembledi|. K.
     919         ∀j:nat. ∀H: j < |assembledi|. K.
    920920          nth_safe ? j assembledi H =
    921921           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
     
    951951            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
    952952           |assembledi| ≤ |reverse … code| ∧
    953            ∀j:nat. ∀H: j < |assembledi|. K.
     953           ∀j:nat. ∀H: j < |assembledi|. K.
    954954            nth_safe ? j assembledi H =
    955955             nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K)
     
    10711071      >reverse_append >reverse_reverse
    10721072      cases IH3 -IH3
    1073       [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
     1073      [ #IH3 >IH3 <(length_reverse … code) %
     1074        [ >length_append @monotonic_lt_plus_r assumption
     1075        | @nth_safe_prepend ]
    10741076      | * * #IH3a #IH3b #IH3c >IH3a @⊥
    10751077        cut (|program| = 0)
     
    11121114        >(fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction)
    11131115        @(transitive_le … IH6) //
    1114       | #j #LTj >reverse_append >reverse_reverse #K
    1115         >IH
    1116         [ @shift_nth_prefix
    1117         | >length_reverse
    1118           @(lt_to_le_to_lt …
    1119             (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat … (|assembledi'|)))))
    1120           [ @lt_to_lt_nat_of_bitvector_add try assumption
    1121             [ cases daemon (*CSC: True*)
    1122             | cases daemon (*CSC: True*)
    1123             ]
    1124           | cases IH3 -IH3
    1125             [ #eq_code <eq_code
    1126               @(transitive_le … (nat_of_bitvector … (sigma (add …  ppc' (bitvector_of_nat … 1)))))
    1127               [ cases daemon (*CSC: True*)
    1128               | cases (monotone_sigma … sigma_pol_ok … (add … ppc' (bitvector_of_nat … 1)) ppc ??)
    1129                 try assumption
    1130                 [ #X @X
    1131                 | cases daemon (*CSC: False, sigma ppc = zero! *)
    1132                 | @(transitive_le … ppc_ok) %2 %
    1133                 | cases daemon (*CSC: True*)
    1134                 ]]
    1135             | * * #_ #relevant #_ >relevant
    1136               @(transitive_le … (S ?) … (lt_nat_of_bitvector …)) [%2 % | skip]]]
    1137         ]]]]]
     1116      | #j #LTj >reverse_append >reverse_reverse cases (IH … LTj) -IH #K #IH %
     1117        [ >length_append @(lt_to_le_to_lt … K) //
     1118        | >IH @shift_nth_prefix ]]]]]
    11381119qed.
    11391120
  • 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.