Changeset 2189


Ignore:
Timestamp:
Jul 17, 2012, 1:03:37 AM (5 years ago)
Author:
sacerdot
Message:

Proof very close to completion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2188 r2189  
    977977      | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction
    978978        >IH3c try % assumption ]
    979 (*        cut (ppc ≠ zero …)
    980         [% #EQppc_zero @(absurd … IH3b) >IH2' [ @not_eq_O_S ] assumption ] #Not_eq_ppc_zero
    981         cut (bitvector_of_nat ? (S (pred (nat_of_bitvector … ppc))) = ppc)
    982         [ inversion (nat_of_bitvector … ppc)
    983           [2: #p #_ #H normalize in match (pred ?);
    984               lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector
    985               #H' <H' %
    986           | #H @⊥
    987             lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector
    988             #H' @(absurd ?? Not_eq_ppc_zero) >H' % ]] #EQppc lapply ppc_ok; <EQppc #S_pred_ppc_ok
    989         cases (sigma_pol_ok2 (bitvector_of_nat 16 (pred (nat_of_bitvector 16 ppc))) ?)
    990         [2: @(transitive_lt … ppc_ok) >nat_of_bitvector_bitvector_of_nat_inverse
    991             [2: cases daemon (*CSC: True *) | cases daemon (*CSC: True*) ]
    992         | #Sigma_pol1 *
    993           [ cases daemon (*??????????*)
    994           | * #Sigma_pol2 #Sigma_pol3 lapply (Sigma_pol2 … S_pred_ppc_ok ?)
    995             [ cases daemon (*CSC: True *) ]
    996             whd in ⊢ (% → ?); <eq_create_label_cost_map #H >H % ]]]*)
    997     | %(* >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
    998        #abs >abs in sigma_pol4; *
    999        [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
    1000        | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
    1001          >nat_of_bitvector_bitvector_of_nat_inverse // ]*)
     979    | % (*CSC: Stupid proof of True, drop fake invariant *)
    1002980    | >length_append >length_reverse
    1003981      cases IH3 -IH3
     
    10321010          >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]]
    10331011  | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2
    1034     #EQpc_delta2 #eq_fetch_pseudo_instruction *
    1035     [2: #eq_S_prefix_bound
    1036       cut (instr_list = prefix @ [〈label,pi〉 ]) [ cases daemon (*CSC: easy *) ] #EQinstr_list
    1037       @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
    1038       @pair_elim #len #assembledi #eq_assembly_1_pseudoinstruction %
    1039       [
    1040       |
    1041       ]
    1042     | #LTppc_ppc
    1043       cases (le_to_or_lt_eq … LTppc_ppc)
    1044       [2: #S_S_eq normalize nodelta in S_S_eq;
    1045           (*CSC: TRUE, NEEDS SOME WORK *)
    1046           cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' >prf
    1047           >IH1 #LTppc lapply LTppc
    1048           >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
    1049           >fetch_pseudo_instruction_append
    1050           [3: @le_S_S @le_O_n
    1051           |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
    1052           |4: <prf <p_refl in instr_list_ok; #H @H ]
    1053           #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
    1054           [ >length_reverse >length_append >length_reverse // ]
    1055           #j #LTj >nat_of_bitvector_add
    1056           >nat_of_bitvector_bitvector_of_nat_inverse
    1057           [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
    1058           |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
    1059           >reverse_append >reverse_reverse
    1060           cases IH3 -IH3
    1061           [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
    1062           | cases daemon (*CSC: ?????????? *) ]
    1063       | #LTppc''
    1064         cut (nat_of_bitvector … ppc' < |instr_list|)
    1065         [ normalize nodelta in LTppc'';
    1066           @(transitive_le … (nat_of_bitvector … ppc))
    1067           [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse //
    1068           | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
    1069             [ >commutative_plus #H @H
    1070             | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
    1071               @(transitive_le … instr_list_ok)
    1072               >IH1 >nat_of_bitvector_bitvector_of_nat_inverse [2: assumption ]
    1073               >prf >length_append >length_append <plus_n_Sm @le_S_S normalize
    1074               cases daemon (*CSC: ????
    1075              
    1076                >prf >length_append @le_S_S >(commutative_plus (|prefix|))
    1077               >length_append >nat_of_bitvector_bitvector_of_nat_inverse
    1078               [2: <p_refl in instr_list_ok; >prf >length_append #H
    1079                   @(transitive_le … H) //
    1080               | @le_S_S //*) ]]]]
    1081       #X lapply (IH4 ppc' X)
     1012    #EQpc_delta2 #eq_fetch_pseudo_instruction #OR_lt_eq
     1013    cut (ppc' = ppc ∨ ppc' ≠ ppc) [cases daemon (*CSC: True*)] *
     1014    [ #EQppc' >EQppc' in LTppc'; -ppc' >prf
     1015      >IH1 #LTppc lapply LTppc
     1016      >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
     1017      >fetch_pseudo_instruction_append
     1018      [3: @le_S_S @le_O_n
     1019      |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
     1020      |4: <prf <p_refl in instr_list_ok; #H @H ]
     1021      #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
     1022      [ >length_reverse >length_append >length_reverse // ]
     1023      #j #LTj >nat_of_bitvector_add
     1024      >nat_of_bitvector_bitvector_of_nat_inverse
     1025      [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
     1026      |3: @(lt_to_le_to_lt … (nat_of_bitvector … (sigma ppc) + pc_delta))
     1027          [ >EQpc_delta @monotonic_lt_plus_r assumption
     1028          | cases sigma_pol4
     1029            [ #H @(transitive_le … H) %2 %
     1030            | * #_ #EQ >EQ % ]]]
     1031      >reverse_append >reverse_reverse
     1032      cases IH3 -IH3
     1033      [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
     1034      | * * #IH3a #IH3b #IH3c >IH3a @⊥
     1035        cut (|program| = 0)
     1036        [ <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction @IH3c // ] #EQprogram
     1037        @(absurd ?? (not_le_Sn_O j)) <EQprogram assumption ]
     1038    | #NEQppc'
     1039      lapply (IH4 … LTppc')
    10821040      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    10831041      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
     
    10911049        [2: >length_reverse (*CSC: ?????????? <IH3 (*CSC: USE MONOTONICITY *)*) cases daemon
    10921050        | @shift_nth_prefix ]]]]]
    1093 (*        |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
    1094            [ >commutative_plus %
    1095            | >commutative_plus >IH1 whd in ⊢ (?%?);
    1096              @(transitive_le … (S (|instr_list|)))
    1097              [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
    1098              | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
    1099                [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    1100 *)
    1101 cases daemon
    11021051qed.
    11031052
Note: See TracChangeset for help on using the changeset viewer.