Changeset 2292


Ignore:
Timestamp:
Aug 2, 2012, 6:40:15 PM (7 years ago)
Author:
campbell
Message:

More RTLabs invariants.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2289 r2292  
    365365  statement_typed te s → statement_typed (〈r,t〉::te) s.
    366366#tw #r #t *
    367 [ 3: #t' #r #cst #l #H %2 @H
    368 | 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
    369 | 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
     367[ 1,2: //
     368| #t' #r #cst #l #H %2 @H
     369| #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     370| #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
    370371| 6,7: #t' #r1 #r2 #l * /3/
    371 | *: //
     372| #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ]
     373| #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ]
     374| #r' #l1 #l2 * #t' #E /3/
     375| //
    372376] qed.
    373377
     
    571575| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
    572576| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
     577| #l % [2: @(pi2 ?? r) | skip ]
    573578| @(π1 (π1 Env))
    574579| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
     
    793798| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
    794799| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
     800| #l % try @conj
     801  [ @(pi2 ?? fnr)
     802  | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
     803  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
     804    [ #Env @I
     805    | * #retid #retty * #Env #moo %{retty} /2/
     806    ]
     807  ]
     808| #l %
     809  [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
     810  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
     811    [ #Env @I
     812    | * #retid #retty * #Env #moo %{retty} /2/
     813    ]
     814  ]
    795815| @(π1 (π1 (si_vars … (π1 Env))))
    796816| #l #H cases (Exists_append … H)
     
    804824  ]
    805825| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
     826| #l whd % [2: @(pi2 ?? r) | skip ]
    806827| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    807828| @(pi2 … (pf_entry …))
  • src/RTLabs/syntax.ma

    r2288 r2292  
    3737| St_load t' addr dst _ ⇒ env_has e dst t' ∧ env_has e addr ASTptr
    3838| St_store t' addr src _ ⇒ env_has e src t' ∧ env_has e addr ASTptr
     39| St_call_id id args dst _ ⇒ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
     40| St_call_ptr fnptr args dst _ ⇒ env_has e fnptr ASTptr ∧ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
     41| St_cond r _ _ ⇒ ∃t. env_has e r t
    3942| _ ⇒ True
    4043].
  • src/utilities/lists.ma

    r1949 r2292  
    7676[ * [ // | #h #t #_ * ]
    7777| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
     78] qed.
     79
     80lemma All2_left : ∀A,B,P,la,lb.
     81  All2 A B P la lb → All A (λa.∃b.P a b) la.
     82#A #B #P #la elim la
     83[ //
     84| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hdb} // | /2/ ]
     85] qed.
     86
     87lemma All2_right : ∀A,B,P,la,lb.
     88  All2 A B P la lb → All B (λb.∃a.P a b) lb.
     89#A #B #P #la elim la
     90[ * // #h #t *
     91| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ]
    7892] qed.
    7993
Note: See TracChangeset for help on using the changeset viewer.