Changeset 2147


Ignore:
Timestamp:
Jul 3, 2012, 3:53:32 AM (5 years ago)
Author:
sacerdot
Message:

Theorem closed (up to one more lemma on overflow), but new proof obligation
for the assembly function.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2146 r2147  
    730730         let 〈len,assembledi〉 ≝
    731731          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     732         |assembledi| ≤ |assembled| ∧
    732733         ∀j:nat. ∀H: j < |assembledi|. ∀K.
    733734          nth_safe ? j assembledi H =
  • src/ASM/AssemblyProof.ma

    r2146 r2147  
    448448  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
    449449  >eq_fetch_pseudo_instruction
    450   change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
     450  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<|assembledi|.?) → ?)
    451451  >eq_assembly_1_pseudoinstruction
    452   whd in ⊢ (% → ?); #assembly_ok
     452  whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
    453453  %
    454454  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
     
    472472    [1: #j #H <load_code_memory_ok
    473473        [ @assembly_ok
    474         | cases assembly_ok3 -assembly_ok3
     474        | cut (0=|assembled'| → False)
     475          [ #abs <abs in assembly_ok4; >EQlen #abs'
     476            @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY
     477          cases assembly_ok3 -assembly_ok3
    475478          [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ]
    476479          #EQlen_assembled' <EQlen_assembled'
     
    483486          [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
    484487              <add_bitvector_of_nat_Sm >add_commutative
    485               >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
    486               whd in ⊢ (??%? → ?); #EQlen_assembled'
    487               cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ]
     488              >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 assumption ]
    488489          cases (le_to_or_lt_eq … instr_list_ok)
    489490          [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
    490               whd in ⊢ (??%? → ?); #EQlen_assembled'
    491               cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ]             
    492           ]
     491              assumption ]
    493492          #instr_list_ok' #NO_OVERFLOW
    494493          @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
     
    509508                >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
    510509                @(transitive_le … instr_list_ok') @le_S_S assumption
    511             | * #EQ1 @⊥ >EQ1 in EQlen_assembled';
    512                 whd in ⊢ (??%? → ?); #EQlen_assembled'
    513                 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *)
    514             ]
    515           ]
    516 (* OLD CODE          [ #assembly_ok1'
    517             cut (nat_of_bitvector 16 (sigma ppc)+|assembled|≤|assembled'|)
    518             [ cases sigma_policy_witness #_ >EQprogram #sigma_ok
    519               cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
    520               whd in match instruction_size; normalize nodelta
    521               >create_label_cost_refl
    522               >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
    523               [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
    524               [ #JAP1
    525                 cut (nat_of_bitvector … (sigma ppc) + len < 2^16)
    526                 [cases daemon (*CSC: provable, needs lemma*)] #LT1
    527                 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len)
    528                 [2: @(le_to_lt_to_lt … LT1) / by / ]
    529                 cases assembly_ok3
    530                 [2: * #_ #abs @⊥ @(absurd … abs (lt_to_not_eq … assembly_ok1')) ]
    531                 #EQ_sigma_instr_list <EQ_sigma_instr_list
    532                 <nat_of_bitvector_add
    533                 [2: >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    534                     @(transitive_le … LT1) @le_S_S / by / ]
    535                 <OK XXX
    536                
    537                  XXX cases daemon (*CSC: ???*)
    538                 | -assembly_ok3 #assembly_ok3
    539                   <assembly_ok3             
    540                 (*CSC: we have to go by cases here!*)
    541                 <nat_of_bitvector_add
    542                 [2: cases daemon ] (*CSC: end of wrong part*)
    543  
    544               |
    545               ]
    546              
    547              
    548                #JAP1
    549               <(nat_of_bitvector_bitvector_of_nat_inverse 16 len)
    550               [2: cases daemon ]
    551               cases assembly_ok3
    552               [2: * #_ #EQ2 cases daemon (*CSC: ???*)
    553               | -assembly_ok3 #assembly_ok3
    554                 <assembly_ok3             
    555               (*CSC: we have to go by cases here!*)
    556               <nat_of_bitvector_add
    557               [2: cases daemon ] (*CSC: end of wrong part*)
    558            
    559            
    560              cases assembly_ok3
    561               [2: * #_ #EQ2 cases daemon (*CSC: ???*)
    562               | -assembly_ok3 #assembly_ok3
    563                 <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok
    564                 cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
    565                 whd in match instruction_size; normalize nodelta
    566                 >create_label_cost_refl
    567                 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
    568                 [>eq_assembly_1_pseudoinstruction |2: skip] #OK #_ <EQlen
    569                 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len)
    570                 [2: cases daemon ]
    571                 <nat_of_bitvector_add
    572                 [2: cases daemon ]
    573                 <OK @(monotone_sigma2 … sigma_policy_witness) >EQprogram
    574                 cases daemon (*CSC: ???*)
    575               ]
    576             | #LE2
    577               cut (|assembled| < 2^16)
    578                [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction) / by /] #LTassembled
    579               cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
    580               [ >nat_of_bitvector_add
    581                 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    582                 @(le_to_lt_to_lt … LE2 assembly_ok1')
    583               | #LE @(lt_to_le_to_lt … LE)
    584                 @lt_to_lt_nat_of_bitvector_add
    585                 [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
    586                   / by /
    587                 | @(le_to_lt_to_lt ???? assembly_ok1') @LE2
    588                 | assumption
    589                 ]
    590               ]
    591             ]
    592           | #assembly_ok1' >assembly_ok1' / by /
    593           ]*)
     510            | * #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
    594511    |2:
    595512      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
     
    604521           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
    605522           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
    606            >add_associative % ]]
    607   ]]
     523           >add_associative % ]]]]
    608524qed.
    609525
Note: See TracChangeset for help on using the changeset viewer.