Changeset 3371 for src/joint


Ignore:
Timestamp:
Jun 26, 2013, 2:22:28 PM (6 years ago)
Author:
piccolo
Message:

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationHelper.ma

    r3154 r3371  
    181181* #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin
    182182cases(bind_new_bind_new_instantiates' … Hregs
    183   (bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
    184        EQfetch Rst1st2 …)))
    185 [2: % assumption
    186 |4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
    187 |3:
     183  ((bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
     184       EQfetch Rst1st2 …) ? )))
     185[3: % assumption
     186|5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
     187|4:
     188|2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
    188189]
    189190#st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel
     
    332333    #H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1
    333334    cases(bind_new_bind_new_instantiates' … Hregs
    334     (bind_new_bind_new_instantiates' ?????? Hdata
     335    ((bind_new_bind_new_instantiates' ?????? Hdata
    335336     (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 …
    336        EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption]
     337       EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1)) ?))
     338    [3: % assumption
     339    |2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
     340    ]
    337341    #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl
    338342    * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H)
    339     -H #st2' * #EQst2' #fin_sem_rel
     343    -H [2: @sym_eq
     344           @(bind_new_bind_new_instantiates' … Hregs1 (pi2 ?? (init ? fn1)))]
     345    #st2' * #EQst2' #fin_sem_rel
    340346|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %
    341347|
     
    366372  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
    367373  >point_of_pc_of_point >EQmid % ]
    368 cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     374cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
    369375#nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1)
    370376* #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_
     
    582588]
    583589#EQ destruct(EQ) #n_costed
    584 lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
    585 [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
    586       #H cases(H EQfetch) -H |*:]
     590lapply(b_graph_transform_program_fetch_internal_function … goodR (pc_block (pc … st1)) f fn)
     591@eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H
     592cases(H (proj1 … (fetch_statement_inv … EQfetch))) -H
    587593#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    588 #EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
    589 *** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
     594#EQt_fn1 #Hinit * #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #H
     595lapply(H ?? (proj2 … (fetch_statement_inv … EQfetch))) -H normalize nodelta
     596 whd in ⊢ (% → ?);
     597*** #blp #blm #bls * @if_elim
    590598[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
    591       whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
    592       #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
    593       >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
    594       whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
    595       <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
     599      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ <ABS
     600      cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
    596601]
    597602#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
    598603#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
    599604* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    600 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    601                (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
    602 [2,4: % assumption]
     605cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
     606               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)) ?))
     607[2,5: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
     608      @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
     609|3,6: % assumption
     610]
    603611#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    604612cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
    605613normalize nodelta
    606 #Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
     614#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v' #_
    607615[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
    608616     (last_pop … st2))}
     
    775783#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
    776784>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
    777 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
    778                (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    779                [2: % assumption]
     785cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
     786               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)) ? ))
     787[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
     788    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
     789|3: % assumption
     790]
    780791#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
    781792%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
     
    10641075cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
    10651076<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
    1066 cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit
     1077cases(bind_new_bind_new_instantiates' … Hregs ((bind_new_bind_new_instantiates' … Hinit
    10671078 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
    1068    Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
     1079   Rst1st2 t_fn EQt_fn)) ? ))
     1080[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
     1081    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn))) ] 
     1082#EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
    10691083** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
    10701084[ * #sem_rel #EQt_next
     
    13471361#id' * #args' * #dest' #EQinstr
    13481362cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
    1349   (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
     1363  ((bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
    13501364 (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize …
    1351    EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr)
     1365   EQst1_no_pc'' … Rst1st2 … EQt_fn1)) ?) … EQpc' EQt_call EQinstr)
     1366[2: @sym_eq
     1367    @(bind_new_bind_new_instantiates' …
     1368        (bind_instantiates_to_instantiate … EQdata) (pi2 ?? (init ? fn))) ]
    13521369#st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after
    13531370#Hprologue
     
    13631380%{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
    13641381   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
    1365 cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) -Hprologue #st2' * #EQst2'
    1366 #fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
     1382cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue)
     1383[2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata1 (pi2 ?? (init ? fn1)))] 
     1384-Hprologue #st2' * #EQst2'
     1385#fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
    13671386#nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta
    13681387>(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %]
  • src/joint/StatusSimulationUtils.ma

    r3262 r3371  
    256256  return 〈f,t_fn〉 →
    257257  bind_new_P' ??
    258      (λregs1.λdata.bind_new_P' ??
     258     (λregs1.λdata.
     259     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    259260      (λregs2.λblp.
    260261       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
     
    292293     return 〈f,t_fn〉 →
    293294    bind_new_P' ??
    294      (λregs1.λdata.bind_new_P' ??
     295     (λregs1.λdata.
     296      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    295297     (λregs2.λblp.(\snd blp) = [ ] ∧
    296298        ∀mid.
     
    342344  bind_new_P' ??
    343345     (λregs1.λdata.
    344       bind_new_P' ??
     346      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    345347      (λregs2.λblp.
    346348       \snd blp = (RETURN …) ∧
     
    426428  bind_new_P' ??
    427429    (λregs1.λdata.
    428      bind_new_P' ??
     430     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    429431      (λregs2.λblp.
    430432        ∀pc',t_fn,id',arg',dest',nxt1.
     
    448450       bind_new_P' ??
    449451         (λregs11.λdata1.
    450           ∃st2'.
     452          init_regs bl = new_regs … data1 → ∃st2'.
    451453           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    452454           (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
     
    481483  bind_new_P' ??
    482484     (λregs1.λdata.
    483       bind_new_P' ??
     485      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    484486      (λregs2.λblp.
    485487        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     
    523525   bind_new_P' ??
    524526    (λregs1.λdata.
    525      bind_new_P' ??
     527     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
    526528      (λregs2.λblp.
    527529       ∃ has_tail',id',arg'.
     
    537539       bind_new_P' ??
    538540         (λregs11.λdata1.
    539           ∃st2'.
     541          init_regs bl = new_regs … data1 → ∃st2'.
    540542           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    541543           (added_prologue … data1) (increment_stack_usage P_out ssize_f1 st2_after) =
     
    782784lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
    783785@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    784 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
     786#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
    785787lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
    786788[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
     
    984986lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn)
    985987@eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
    986 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
     988#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
    987989lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
    988990-EQfetch cases stmt in EQstmt H;
  • src/joint/lineariseProof.ma

    r2808 r3371  
    1818include "joint/semanticsUtils.ma".
    1919include "common/ExtraMonads.ma".
    20 (*
    21 !!!SPOSTATO IN extraGlobalenvs.ma!!!!
    22 
    23 include alias "common/PositiveMap.ma".
    24 
    25 lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
    26 id < (nextfunction ? ge) →
    27 lookup_opt … id (functions ? ge) = None ? →
    28 lookup_opt … id (functions … (add_functs F ge l)) = None ?.
    29 #F #ge #l #id whd in match add_functs; normalize nodelta
    30 elim l -l [ #_ normalize //]
    31 * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
    32 >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
    33 #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
    34 | cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
    35 [elim tl [normalize //]
    36 #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
    37 #H2 lapply(transitive_le … H H2) @lt_to_not_eq
    38 qed.
    39 
    40 lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
    41 lookup_opt … id (functions ? (\fst gem)) = None ? →
    42 lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?.
    43 #F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
    44 ** #x1 #x2 #x3 #tl whd in match add_globals;
    45 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
    46 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
    47 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
    48 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption
    49 qed.
    50 
    51  
    52 lemma globalenv_no_minus_one :
    53  ∀F,V,i,p.
    54   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
    55 #F #V #i #p
    56 whd in match find_funct_ptr; normalize nodelta
    57 whd in match globalenv;
    58 whd in match globalenv_allocmem; normalize nodelta
    59 @add_globals_functions_miss @add_functs_functions_miss normalize //
    60 qed.
    61 *)
    62 
    63 (* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!!
    64 
    65 lemma fetch_internal_function_no_minus_one :
    66   ∀F,V,i,p,bl.
    67   block_id (pi1 … bl) = -1 →
    68   fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    69     bl = Error … [MSG BadFunction].
    70  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
    71  whd in match fetch_internal_function;
    72   whd in match fetch_function; normalize nodelta
    73   >globalenv_no_minus_one
    74   cases (symbol_for_block ???) normalize //
    75 qed.
    76 
    77 *)
    78 
    79 (*spostato in ExtraMonads.ma
    80 
    81 lemma bind_option_inversion_star:
    82   ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
    83   (∀x.f = Some … x → g x = Some … y → P) →
    84   (! x ← f ; g x = Some … y) → P.
    85 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
    86 
    87 interpretation "option bind inversion" 'bind_inversion =
    88   (bind_option_inversion_star ???????).
    89 
    90 lemma bind_inversion_star : ∀X,Y.∀P : Prop.
    91 ∀m : res X.∀f : X → res Y.∀v : Y.
    92 (∀x. m = return x → f x = return v → P) →
    93 ! x ← m ; f x = return v → P.
    94 #X #Y #P #m #f #v #H #G
    95 elim (bind_inversion ????? G) #x * @H qed.
    96 
    97 interpretation "res bind inversion" 'bind_inversion =
    98   (bind_inversion_star ???????).
    99 
    100 lemma IO_bind_inversion:
    101   ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    102   (∀x.f = return x → g x = return y → P) →
    103   (! x ← f ; g x = return y) → P.
    104 #O #I #A #B #P #f #g #y cases f normalize
    105 [ #o #f #_ #H destruct
    106 | #a #G #H @(G ? (refl …) H)
    107 | #e #_ #H destruct
    108 ] qed.
    109 
    110 interpretation "IO bind inversion" 'bind_inversion =
    111   (IO_bind_inversion ?????????).
    112 
    113 record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
    114   { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop)
    115   ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf))
    116   ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n.
    117       m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) →
    118                   m_frel ?? Q G (m_bind … m f) (m_bind … n g)
    119   ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
    120   }.
    121 
    122 *)
    123 
    124 (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    125   λO,I.mk_MonadFunctRel ??
    126   (λX,Y,F,m,n.∀x.m = return x → n = return F x)
    127   ???.
    128 [ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    129 | #X #Y #Z #W #F #G *
    130   [ #o #f | #u | #e ] #n #H #f #g #K #x
    131   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    132   >(H ? (refl …)) @K @EQ
    133 | #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H %
    134 ]
    135 qed.*)
    136 
    137 (* spostato in ExtraMonads.ma
    138 definition res_preserve : MonadFunctRel Res Res ≝
    139   mk_MonadFunctRel ??
    140   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    141   ???.
    142 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    143 | #X #Y #Z #W #P #Q #F #G *
    144   [ #u | #e ] #n #H #f #g #K #x
    145   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    146   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    147 | #X #Y #P #F #G #H #u #v #K #x #EQ
    148   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    149 ]
    150 qed.
    151 
    152 definition opt_preserve : MonadFunctRel Option Option ≝
    153   mk_MonadFunctRel ??
    154   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    155   ???.
    156 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    157 | #X #Y #Z #W #P #Q #F #G *
    158   [ | #u ] #n #H #f #g #K #x
    159   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    160   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    161 | #X #Y #P #F #G #H #u #v #K #x #EQ
    162   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    163 ]
    164 qed.
    165 
    166 definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    167   λO,I.mk_MonadFunctRel ??
    168   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    169   ???.
    170 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    171 | #X #Y #Z #W #P #Q #F #G *
    172   [ #o #f | #u | #e ] #n #H #f #g #K #x
    173   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    174   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    175 | #X #Y #P #F #G #H #u #v #K #x #EQ
    176   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    177 ]
    178 qed.
    179 
    180 definition preserving ≝
    181   λM1,M2.λFR : MonadFunctRel M1 M2.
    182   λX,Y,A,B : Type[0].
    183   λP : X → Prop.
    184   λQ : A → Prop.
    185   λF : ∀x : X.P x → Y.
    186   λG : ∀a : A.Q a → B.
    187   λf : X → M1 A.
    188   λg : Y → M2 B.
    189   ∀x,prf.
    190   FR … G
    191     (f x) (g (F x prf)).
    192 
    193 definition preserving2 ≝
    194   λM1,M2.λFR : MonadFunctRel M1 M2.
    195   λX,Y,Z,W,A,B : Type[0].
    196   λP : X → Prop.
    197   λQ : Y → Prop.
    198   λR : A → Prop.
    199   λF : ∀x : X.P x → Z.
    200   λG : ∀y : Y.Q y → W.
    201   λH : ∀a : A.R a → B.
    202   λf : X → Y → M1 A.
    203   λg : Z → W → M2 B.
    204   ∀x,y,prf1,prf2.
    205   FR … H
    206     (f x y) (g (F x prf1) (G y prf2)).
    207 *)
     20
     21check mk_sem_graph_params
    20822
    20923definition graph_prog_params ≝
    210 λp,p',prog,stack_sizes.
    211 mk_prog_params (mk_sem_graph_params p p') prog stack_sizes.
     24λp,p',pre_main,prog,stack_sizes.
     25mk_prog_params (mk_sem_graph_params p p' pre_main) prog stack_sizes.
     26
     27check mk_sem_graph_params
    21228
    21329definition graph_abstract_status:
    214  ∀p:unserialized_params.
     30 ∀p:uns_params.
    21531  (∀F.sem_unserialized_params p F) →
     32   (∀prog : joint_program (mk_graph_params p).
     33    joint_closed_internal_function (mk_graph_params p) (prog_names … prog)) →
    21634    ∀prog : joint_program (mk_graph_params p).
    21735  (ident → option ℕ) →
    21836     abstract_status
    219  ≝
    220  λp,p',prog,stack_sizes.
    221  joint_abstract_status (graph_prog_params ? p' prog stack_sizes).
     37 ≝ 
     38 λp,p',pre_main,prog,stack_sizes.
     39 joint_abstract_status (graph_prog_params ? p' pre_main prog stack_sizes).
    22240
    22341definition lin_prog_params ≝
    224 λp,p',prog,stack_sizes.
    225 mk_prog_params (mk_sem_lin_params p p') prog stack_sizes.
     42λp,p',pre_main,prog,stack_sizes.
     43mk_prog_params (mk_sem_lin_params p p' pre_main) prog stack_sizes.
    22644
    22745definition lin_abstract_status:
    228  ∀p:unserialized_params.
     46 ∀p:uns_params.
    22947  (∀F.sem_unserialized_params p F) →
     48  (∀prog : joint_program (mk_lin_params p).
     49    joint_closed_internal_function (mk_lin_params p) (prog_names … prog)) →
    23050    ∀prog : joint_program (mk_lin_params p).
    23151  (ident → option ℕ) →
    23252     abstract_status
    23353 ≝
    234  λp,p',prog,stack_sizes.
    235  joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
     54 λp,p',pre_main,prog,stack_sizes.
     55 joint_abstract_status (lin_prog_params ? p' pre_main prog stack_sizes).
    23656
    23757(*
Note: See TracChangeset for help on using the changeset viewer.