Changeset 2153 for src/ASM


Ignore:
Timestamp:
Jul 4, 2012, 3:38:52 PM (7 years ago)
Author:
boender
Message:
  • updated the proof some more
File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Policy.ma

    r2152 r2153  
    3535  | #sigma normalize nodelta #H @conj [ @conj
    3636    [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
    37     | (* #Ht destruct (Ht) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
     37    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    3838    ]
    3939    | @(proj2 ?? H)
    … …  
    4848    | #j2 #H2 @conj [ @conj
    4949      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    50       | (*#Ht @(equal_compact_unsafe_compact ?? op)
    51         [ @(proj2 ?? (proj1 ?? H2)) @Ht
    52         | cases daemon (* add sigma_safe to properties *)
    53         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
    54         ]*)
    55         @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     50      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
    5651      ]
    5752      | @(proj2 ?? H2)
    … …  
    6863qed.
    6964
     65 
    7066lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program).
    7167#program whd #x whd #n #Hn
    … …  
    153149]
    154150qed.
     151
     152lemma jump_pc_equal: ∀program.∀n.
     153  match \snd (jump_expansion_internal program n) with
     154  [ None   ⇒ True
     155  | Some p1 ⇒ match \snd (jump_expansion_internal program (S n)) with
     156    [ None ⇒ True
     157    | Some p2 ⇒ sigma_jump_equal program p1 p2 → sigma_pc_equal program p1 p2
     158    ]
     159  ].
     160 #program #n lapply (refl ? (jump_expansion_internal program n))
     161 cases (jump_expansion_internal program n) in ⊢ (???% → %); #x cases x -x
     162 #Nno_ch #No cases No
     163 [ normalize nodelta #HN #NEQ @I
     164 | #Npol normalize nodelta #HN #NEQ lapply (refl ? (jump_expansion_internal program (S n)))
     165   cases (jump_expansion_internal program (S n)) in ⊢ (???% → %); #x cases x -x
     166   #Sno_ch #So cases So
     167   [ normalize nodelta #HS #SEQ @I
     168   | #Spol normalize nodelta #HS #SEQ #Hj
     169     whd in match (jump_expansion_internal program (S n)) in SEQ; (*80s*)
     170     >NEQ in SEQ; normalize nodelta cases Nno_ch in HN;
     171     [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ))))
     172       / by /
     173     | #HN normalize nodelta cases (jump_expansion_step program (create_label_map program) «Npol,?»)     
     174       #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o
     175       [ normalize nodelta #_ #H destruct (H)
     176       | #Stno_p normalize nodelta #HSt #STeq
     177         <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? STeq)))) in Hj; #Hj
     178         @(proj2 ?? (proj1 ?? HSt)) @(proj2 ?? (proj1 ?? (proj1 ?? HSt))) @Hj
     179       ]
     180     ]
     181   ]
     182 ]
     183qed.
     184       
    155185
    156186lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    … …  
    413443        @conj
    414444        [ @(equal_compact_unsafe_compact ?? Fp)
    415           [ cases daemon
     445          [ lapply (jump_pc_equal program (2*|program|))
     446            >Feq >Geq normalize nodelta #H @H @Heq
    416447          | cases daemon
    417448          | @(proj2 ?? (proj1 ?? HGp))
    … …  
    487518                  normalize nodelta #Hpe
    488519                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
    489                   [ cases daemon (* reorder *)
     520                  [ @HXp
    490521                  | lapply (Hfa x Hx) >Xeq >Seq
    491522                    lapply (measure_special program «Xp,?»)
    492                     [ cases daemon (* reorder *)
     523                    [ @HXp
    493524                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
    494525                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
    … …  
    517548        ]
    518549      ]
    519     | #Hfull
    520       whd in match (jump_expansion_internal program (S (2*|program|))); (*65s*)
    521       >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq
    522       normalize nodelta
    523       [ @conj
    524         [ cases daemon (* XXX *)
    525         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
    526         ]
    527       | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto
    528         [ #_ / by I/
    529         | -sto #stp normalize nodelta #Hstp @conj
    530           [ @(equal_compact_unsafe_compact ?? Fp)
    531             [ @(proj2 ?? (proj1 ?? Hstp)) @(proj2 ?? (proj1 ?? (proj1 ?? Hstp)))
    532               #i #Hi
    533               cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    534               [ #Hj
    535                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) i (le_S_to_le … Hi))
    536                 lapply (Hfull i Hi Hj)
    537                 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    538                 #fp #fj #Hfj >Hfj normalize nodelta
    539                 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
    540                 #stp #stj cases stj normalize nodelta
    541                 [1,2: #H cases H #H2 cases H2 destruct (H2)
    542                 |3: #_ @refl
    543                 ]
    544               | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i Hi Hj)
     550    | #Hfull lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
     551      cases (jump_expansion_internal program (S (2*|program|))) in ⊢ (???% → %);
     552      #z cases z -z #Gch #Go cases Go normalize nodelta
     553      [ #HGp #Geq @I
     554      | -Go #Gp normalize nodelta #HGp #Geq @conj
     555        [ @(equal_compact_unsafe_compact ?? Fp)
     556          [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
     557            #H @H #i #Hi
     558            cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     559            [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
     560              >Feq in Geq; normalize nodelta cases Fno_ch
     561              [ normalize nodelta #Heq
     562                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
     563              | normalize nodelta cases (jump_expansion_step program (create_label_map program) «Fp,?»)
     564                #x cases x -x #stch #sto normalize nodelta cases sto
     565                [ normalize nodelta #_ #X destruct (X)
     566                | -sto #stp normalize nodelta #Hst #Heq
     567                   <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
     568                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
     569                   lapply (Hfull i Hi Hj)
     570                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
     571                   #fp #fj #Hfj >Hfj normalize nodelta
     572                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
     573                   #stp #stj cases stj normalize nodelta
     574                   [1,2: #H cases H #H2 cases H2 destruct (H2)
     575                   |3: #_ @refl
     576                   ]
     577                 ]
     578               ]
     579             | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi Hj)
    545580                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
    546581              ]
    547             | cases daemon 
    548             | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))
     582            | cases daemon
     583            | @(proj2 ?? (proj1 ?? HGp))
    549584            ]
    550           | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))
     585          | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
    551586          ]
    552587        ]
    553588      ]
    554589    ]
    555   ]
    556 | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
    557   #x cases x -x #nch #npol normalize nodelta #Hnpol
    558   #x cases x -x #Sch #Spol normalize nodelta #HSpol
    559   cases npol in Hnpol; cases Spol in HSpol;
    560   [ #Hnpol #HSpol %1 //
    561   |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
    562     #H destruct (H)
    563   |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
    564       cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
    565       #x1 #x2
    566       cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
    567       #y1 #y2 normalize nodelta
    568       @dec_eq_jump_length
    569   ]
    570 ]
     590  | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
     591    #x cases x -x #nch #npol normalize nodelta #Hnpol
     592    #x cases x -x #Sch #Spol normalize nodelta #HSpol
     593    cases npol in Hnpol; cases Spol in HSpol;
     594    [ #Hnpol #HSpol %1 //
     595    |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
     596      #H destruct (H)
     597    |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
     598        cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     599        #x1 #x2
     600        cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     601        #y1 #y2 normalize nodelta
     602        @dec_eq_jump_length
     603    ]
     604  ]
    571605qed.
    572606
Note: See TracChangeset for help on using the changeset viewer.