Changeset 1949 for src/joint


Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
Location:
src/joint
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1908 r1949  
    7474  | extension: ext_step p → joint_step p globals.
    7575
     76axiom EmptyString : String.
     77definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
     78
    7679notation "r ← a1 .op. a2" with precedence 60 for
    7780  @{'op2 $op $r $a1 $a2}.
     
    124127  }.
    125128
     129inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝
     130  | GOTO: label → joint_fin_step p globals
     131  | RETURN: joint_fin_step p globals
     132  | extension_fin : ext_fin_stmt p → joint_fin_step p globals.
     133
    126134inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    127135  | sequential: joint_step p globals → succ p → joint_statement p globals
    128   | GOTO: label → joint_statement p globals
    129   | RETURN: joint_statement p globals
    130   | extension_fin : ext_fin_stmt p → joint_statement p globals.
    131 
    132 coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
    133   extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
    134 
    135 definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
    136   match s with
    137   [ sequential _ _ ⇒ False
    138   | _ ⇒ True
    139   ].
     136  | final: joint_fin_step p globals → joint_statement p globals.
     137
     138coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals.
     139  ∀s : ext_fin_stmt p.joint_fin_step p globals ≝
     140  extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??.
     141
     142coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
     143  ∀s : joint_fin_step p globals.joint_statement p globals ≝
     144  final on _s : joint_fin_step ?? to joint_statement ??.
    140145
    141146record params : Type[1] ≝
     
    187192  ].
    188193
     194definition fin_step_labels ≝
     195  λp,globals.λs : joint_fin_step p globals.
     196  match s with
     197  [ GOTO l ⇒ [ l ]
     198  | RETURN ⇒ [ ]
     199  | extension_fin c ⇒ ext_fin_stmt_labels … c
     200  ].
     201
    189202definition stmt_explicit_labels :
    190203  ∀p,globals.
     
    192205  λp,globals,stmt. match stmt with
    193206  [ sequential c _ ⇒ step_labels … c
    194   | GOTO l ⇒ [ l ]
    195   | RETURN ⇒ [ ]
    196   | extension_fin c ⇒ ext_fin_stmt_labels … c
     207  | final c ⇒ fin_step_labels … c
    197208  ].
    198209
  • src/joint/blocks.ma

    r1908 r1949  
    22include "utilities/bind_new.ma".
    33
    4 inductive block_cont (p : params) (globals : list ident) : Type[0] ≝
    5   | Skip : block_cont p globals
    6   | Final : (Σs.no_seq p globals s) → block_cont p globals
    7   | Cons : joint_step p globals → block_cont p globals → block_cont p globals.
    8  
    9 definition instr_block ≝ λp : params.λglobals.bind_new (localsT p) (block_cont p globals).
    10 unification hint 0 ≔ p, globals;
    11 B ≟ block_cont p globals, R ≟ localsT p
     4definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝
     5  λA,B,C,f,p.f (\fst p) (\snd p).
     6
     7inductive stmt_type : Type[0] ≝
     8  | SEQ : stmt_type
     9  | FIN : stmt_type.
     10
     11definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝
     12  λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ].
     13
     14definition block_cont ≝ λp : params.λglobals,ty.
     15  (list (joint_step p globals)) ×
     16    (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals).
     17
     18definition Skip : ∀p,globals.block_cont p globals SEQ ≝
     19  λp,globals.〈[ ], NOOP …〉.
     20
     21definition instr_block ≝ λp : params.λglobals,ty.
     22  bind_new (localsT p) (block_cont p globals ty).
     23unification hint 0 ≔ p, globals, ty;
     24B ≟ block_cont p globals ty, R ≟ localsT p
    1225(*---------------------------------------*)⊢
    13 instr_block p globals ≡ bind_new R B.
    14 
    15 (* it returns b1 if it is ended by final rather than skip *)
    16 let rec block_cont_append p g (b1 : block_cont p g) (b2 : block_cont p g) on b1 : block_cont p g ≝
    17 match b1 with
    18 [ Skip ⇒ b2
    19 | Cons x b1' ⇒ Cons … x (block_cont_append … b1' b2)
    20 | Final _ ⇒ b1
    21 ].
    22 
    23 interpretation "block contents nil" 'vnil = (Skip ??).
    24 interpretation "block contents cons" 'vcons x b = (Cons ?? x b).
    25 interpretation "block contents append" 'vappend b1 b2 = (block_cont_append ?? b1 b2).
     26instr_block p globals ty ≡ bind_new R B.
     27
     28definition block_cont_append :
     29  ∀p,g,ty.
     30  ∀b1 : block_cont p g SEQ.
     31  ∀b2 : block_cont p g ty.
     32  block_cont p g ty ≝
     33  λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉.
     34
     35definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉.
     36
     37interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b).
     38interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2).
     39
     40definition step_to_block : ∀p : params.∀g.
     41  joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉.
     42
     43definition fin_step_to_block : ∀p : params.∀g.
     44  joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉.
     45
     46coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g.
     47  block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ.
     48
     49coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g.
     50  block_cont p g FIN ≝ fin_step_to_block
     51  on _s : joint_fin_step ?? to block_cont ?? FIN.
    2652
    2753definition block_cons :
    28   ∀p : params.∀globals.joint_step p globals → instr_block p globals → instr_block p globals
    29   ≝ λp,globals,x.m_map … (Cons … x).
     54  ∀p : params.∀globals,ty.
     55  joint_step p globals → instr_block p globals ty → instr_block p globals ty
     56  ≝ λp,globals,ty,x.m_map … (block_cont_cons … x).
    3057
    3158definition block_append :
    32   ∀p : params.∀globals.instr_block p globals → instr_block p globals → instr_block p globals ≝
    33   λp,globals.m_bin_op … (block_cont_append …).
    34 
    35 interpretation "instruction block nil" 'vnil = (bret ?? (Skip ??)).
    36 interpretation "instruction block cons" 'vcons x b = (block_cons ?? x b).
    37 interpretation "instruction block append" 'vappend b1 b2 = (block_append ?? b1 b2).
    38 
    39 let rec block_conts_of_list (p : params) globals (l : list (joint_step p globals)) on l : block_cont p globals ≝
    40   match l with
    41   [ nil ⇒ Skip ??
    42   | cons x l' ⇒ Cons … x (block_conts_of_list ?? l')
    43   ].
    44 definition inst_block_of_list :
    45   ∀p : params.∀globals.list (joint_step p globals) → instr_block p globals ≝
    46   λp,globals,l.return block_conts_of_list … l.
    47 
    48 coercion list_to_inst_block :
    49   ∀p : params.∀globals.∀l : list (joint_step p globals).instr_block p globals ≝
    50   inst_block_of_list on _l : list (joint_step ??) to instr_block ??.
    51 
    52 let rec is_block_instance (p : params) g (b : instr_block p g) (l : list (localsT p)) (b' : block_cont p g) on b : Prop ≝
     59  ∀p : params.∀globals,ty.
     60  instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝
     61  λp,globals,ty.m_bin_op … (block_cont_append …).
     62
     63interpretation "instruction block cons" 'cons x b = (block_cons ??? x b).
     64interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2).
     65
     66let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝
    5367  match b with
    5468  [ bret B ⇒
     
    6175    [ nil ⇒ False
    6276    | cons r l' ⇒
    63       is_block_instance p g (f r) l' b'
     77      is_block_instance p g ty (f r) l' b'
    6478    ]
    6579  ].
    6680
    67 lemma is_block_instance_append : ∀p,globals,b1,b2,l1,l2,b1',b2'.
    68   is_block_instance p globals b1 l1 b1' →
    69   is_block_instance p globals b2 l2 b2' →
    70   is_block_instance p globals (b1 @@ b2) (l1 @ l2) (b1' @@ b2').
    71 #p#globals#b1 elim b1
     81lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'.
     82  is_block_instance p globals SEQ b1 l1 b1' →
     83  is_block_instance p globals ty b2 l2 b2' →
     84  is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2').
     85#p#globals#ty #b1 elim b1
    7286[ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *]
    7387normalize in ⊢ (%→?);
     
    7690  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *]
    7791  normalize in ⊢ (%→?); [2: //] #H2
    78   change with (is_block_instance ?? ('new ?) (r2 :: ?) ?) whd
     92  change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd
    7993  @(IH2 … H2)
    8094]
     
    145159qed.
    146160
    147 let rec block_cont_in_code (p : params) g (c : codeT p g)
    148   (once : bool) src b (dst : option (code_point p))
    149   on b : Prop ≝
    150   match b with
    151   [ Skip ⇒
    152     match dst with
    153     [ Some x ⇒
    154       if once then src ~~>^+ x in c else src ~~>^* x in c
    155     | None ⇒ False
    156     ]
    157   | Final s ⇒
    158     match dst with
    159     [ Some _ ⇒ False
    160     | None ⇒ ∃mid.src ~~>^* mid in c ∧ stmt_at … c mid = Some ? s
    161     ]
    162   | Cons s B' ⇒
    163     ∃mid.src ~~>^* mid in c ∧
     161let rec seq_list_in_code (p : params) g (c : codeT p g)
     162  src l dst on l : Prop ≝
     163  match l with
     164  [ nil ⇒ src = dst
     165  | cons hd tl ⇒
     166    ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧
     167       seq_list_in_code p g c (point_of_succ … src n) tl dst
     168  ].
     169
     170(*
     171definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝
     172  λp,g,b.\fst b @ [\snd b].
     173
     174coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝
     175  seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??).
     176*)
     177
     178definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
     179  code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit → Prop ≝
     180  λp,g.λc : codeT p g.λty,src,b,dst.
     181  ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
     182  match ty
     183  return λx.stmt_type_if ? x ??? →
     184    stmt_type_if ? x ?? → Prop
     185  with
     186  [ SEQ ⇒ λs,dst.
    164187      ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
    165         block_cont_in_code p g c false (point_of_succ … mid n) B' dst
    166    ].
    167    
    168 
    169 notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 56 for
    170   ${default @{'block_in_code $c $b $x $B $y}
    171             @{'block_in_code $c false $x $B $y}
    172   }.
     188         point_of_succ … mid n = dst
     189  | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s)
     190  ] (\snd b) dst.
    173191 
    174 notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    175   @{'block_in_code $c $b $x $B $y}.
     192
     193notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
     194  @{'block_in_code $c $x $B $y}.
     195 
    176196notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    177   @{'block_in_code $c false $x $B $y}.
    178 
    179 interpretation "block cont in code" 'block_in_code c b x B y =
    180   (block_cont_in_code ?? c b x B y).
    181 
    182 lemma tunnel_append_l : ∀p,g.∀c : codeT p g.∀p,x,y,B,z.
    183   x ~~>^* y in c → y ~❨B,p❩~> z in c → x ~❨B,p❩~> z in c.
    184 #p #g #c #b #x #y *
    185 [ * [ #_ *] #z cases b
    186   [ @tunnel_tunnel_plus | @tunnel_trans]
    187 | #s * [2: #z #_ *]
    188 | #s #B' #z]
    189 #H1 * #mid * #H2 #H3 %{mid} %{? H3} @(tunnel_trans … H1 H2)
     197  @{'block_in_code $c $x $B $y}.
     198
     199interpretation "block cont in code" 'block_in_code c x B y =
     200  (block_cont_in_code ?? c ? x B y).
     201
     202lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z.
     203  seq_list_in_code p g c x l1 y →
     204  seq_list_in_code p g c y l2 z →
     205  seq_list_in_code p g c x (l1@l2) z.
     206#p#g#c#x#l1 lapply x -x
     207elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?);
     208[ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G)
     209| #EQ destruct(EQ) //
     210]
     211qed.
     212
     213lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x.
     214  ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z.
     215  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c.
     216#p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta
     217#l1 #s1 #y * #l2 #s2 #z * normalize nodelta
     218#mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3
     219%{mid2} %
     220[ whd in match (〈?,?〉@?);
     221  @(seq_list_in_code_append … H1)
     222  %{n} %{EQ1} >EQ2 assumption
     223| assumption
     224]
    190225qed.
    191226
    192 lemma tunnel_plus_append_l : ∀p,g.∀c : codeT p g.∀b,x,y,B,z.
    193   x ~~>^+ y in c → y ~❨B,b❩~> z in c → x ~❨B,true❩~> z in c.
    194 #p #g #c #b #x #y *
    195 [ * [ #_ *] #z cases b
    196   [ @tunnel_plus_trans | @tunnel_plus_tunnel]
    197 | #s * [2: #z #_ *]
    198 | #s #B' #z]
    199 #H1 * #mid * #H2 #H3 %{mid} %{? H3}
    200 @(tunnel_trans … H2) /2 by tunnel_plus_to_star/
    201 qed.
    202 
    203 lemma block_cont_in_code_plus_to_star : ∀p,g.∀c : codeT p g.∀b,x,B1,y.
    204   x ~❨B1,b❩~> y in c → x ~❨B1❩~> y in c.
    205 #p#g#c#b#x *
    206 [ * [*] #y cases b [ @tunnel_plus_to_star | //]
    207 |*: //
    208 ] qed.
    209 
    210 lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀b1,b2,x,B1,y,B2,z.
    211   x ~❨B1,b1❩~> Some ? y in c → y ~❨B2,b2❩~> z in c → x ~❨B1@@B2,b1∨b2❩~> z in c.
    212 #p#g#c #b1 #b2 #x #B1 lapply x -x lapply b2 -b2 lapply b1 -b1 elim B1
    213 [ * #b2 #x #y #B2 #z
    214   [ @tunnel_plus_append_l | @tunnel_append_l ]
    215 | #s #b1 #b2 #x #y #B2 #z *
    216 | #s #B1' #IH #b1 #b2 #x #y #B2 #dst * #m *
    217   #H1 * #n * #H2 #H3 #H4
    218   %{m} %{H1} %{n} %{H2} @(IH false false … H3)
    219   @(block_cont_in_code_plus_to_star … H4)
    220 ]
    221 qed.
    222 
    223227definition instr_block_in_function :
    224   ∀p,g.∀fn : joint_internal_function g p.bool →
    225     instr_block p g
     228  ∀p,g.∀fn : joint_internal_function g p.∀ty.
     229    instr_block p g ty
    226230    code_point p →
    227     option (code_point p) → Prop ≝
    228  λp,g,fn,b,B,src,dst.
     231    ? → Prop ≝
     232 λp,g,fn,ty,B,src,dst.
    229233 ∃vars,B'.
    230234  All ? (In ? (joint_if_locals … fn)) vars ∧
    231235  is_block_instance … B vars B' ∧
    232   src ~❨B',b❩~> dst in joint_if_code … fn.
    233 
    234 interpretation "instr block in function" 'block_in_code fn b x B y =
    235   (instr_block_in_function ?? fn b B x y).
     236  src ~❨B'❩~> dst in joint_if_code … fn.
     237
     238interpretation "instr block in function" 'block_in_code fn x B y =
     239  (instr_block_in_function ?? fn ? B x y).
    236240
    237241lemma instr_block_in_function_trans :
    238   ∀p,g.∀fn : joint_internal_function p g.∀b1,b2,src,B1,mid,B2,dst.
    239   src ~❨B1,b1❩~> Some ? mid in fn →
    240   mid ~❨B2,b2❩~> dst in fn →
    241   src ~❨B1@@B2,b1∨b2❩~> dst in fn.
    242 #p#g#fn#b1#b2#x#B1#y#B2#z
     242  ∀p,g.∀fn : joint_internal_function g p.∀ty,src.
     243  ∀B1 : instr_block p g SEQ.
     244  ∀mid.∀B2 : instr_block p g ty.∀dst.
     245  src ~❨B1❩~> mid in fn →
     246  mid ~❨B2❩~> dst in fn →
     247  src ~❨B1@B2❩~> dst in fn.
     248#p#g#fn#ty#src#B1#mid#B2#dst
    243249* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
    244250* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
    245 %{(vars1@vars2)} %{(b1 @@ b2)}
    246 /4 by is_block_instance_append, block_cont_in_code_append, All_append, conj/
    247 qed.
     251%{(vars1@vars2)} %{(b1 @ b2)}
     252/4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/
     253qed.
  • src/joint/semantics_blocks.ma

    r1882 r1949  
    22include "joint/semantics_paolo.ma".
    33
    4 (* WARNING: all the following breaks apart if statements are allowed to depend
    5    on flow. Execution of blocks does not update flow information in the state
    6    (e.g. the program counter) until the end *)
    7 
    8 definition goto_no_seq : ∀g.∀p:sem_params.genv g p → label →
    9   state p → Z → res (state_pc p) ≝ λg,p,ge,lbl,st,id.
    10       ! newpc ← pointer_of_label ? p … ge
    11         (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) lbl ;
    12       return mk_state_pc … st newpc. % qed.
    13 
    14 lemma goto_no_seq_to_normal : ∀p : sem_params.∀g,ge.∀st : state_pc p.∀id,lbl.
    15   block_id (pblock (pc p st)) = id →
    16   goto_no_seq g p ge lbl st id = goto g p ge lbl st.
    17 #p #g #ge * #st ** #typ * #r #id
    18 #H inversion H [1,3: #r'] #id'
    19 #EQ1 #EQ2 #EQ3 #o #EQ4 #id'' #lbl #EQ5 destruct
    20 whd in match goto_no_seq;
    21 whd in match goto; normalize nodelta //
    22 qed.
    23 
    24 (* executes a block of instructions, until its end or before if a
    25    function call or a redirection is encountered. If executed until end,
    26    or is a non-tail call is encountered, the next program counter must be
    27    provided *)
    28 let rec eval_block_cont globals (p:sem_params) (ge : genv globals p)
    29   (st : state p) id (b : block_cont p globals) (dst : option cpointer) on b :
    30     IO io_out io_in (trace×(state_pc p)) ≝
     4
     5axiom ExecutingInternalCallInBlock : String.
     6
     7let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
    318  match b with
    32   [ Skip ⇒
    33     ! nxt ← opt_to_res … (msg SuccessorNotProvided) dst ;
    34     return 〈E0, mk_state_pc ? st nxt〉
    35   | Final s ⇒
    36     ! 〈flow, tr, st'〉 ← eval_statement_no_seq … ge st s;
    37     ! st ← eval_stmt_flow_no_seq … ge st' id flow;
    38     return 〈tr, st〉
    39   | Cons hd tl ⇒
    40     ! 〈flow, tr1, st'〉 ← eval_step ?? ge st hd ;
     9  [ nil ⇒ [ ]
     10  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
     11  ].
     12
     13definition step_flow_change_labels :
     14  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
     15    step_flow p g lbls1 → step_flow p g lbls2 ≝
     16  λp,g,lbls1,lbls2,prf,flow.
     17  match flow with
     18  [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)»
     19  | Init id b args dest ⇒ Init … id b args dest
     20  | Proceed ⇒ Proceed ???
     21  ].
     22
     23coercion step_flow_diff_lbls :
     24  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
     25  ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝
     26  step_flow_change_labels on _flow : step_flow ??? to step_flow ???.
     27
     28definition monad_step_flow_times_coerc :
     29  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
     30    monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝
     31    λp,g,lbls1,lbls2,M,A,H,m.
     32    ! 〈flow,a〉 ← m ;
     33    return 〈(flow : step_flow ?? lbls2),a〉. assumption qed.
     34
     35coercion step_flow_monad_times :
     36  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
     37    ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝
     38  monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?).
     39
     40let rec eval_seq_list globals (p:sem_params) (ge : genv globals p)
     41  (st : state p) (b : list (joint_step p globals)) on b :
     42    IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝
     43    match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with
     44    [ nil ⇒ return 〈Proceed ???, st〉
     45    | cons hd tl ⇒
     46      ! 〈flow, st'〉 ← eval_step … ge st hd ;
     47      match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with
     48      [ Proceed ⇒ eval_seq_list globals p ge st' tl
     49      | _ ⇒ return 〈flow, st'〉
     50      ]
     51    ]. /2 by Exists_append_r, Exists_append_l/ qed.
     52
     53definition fin_step_flow_change_labels :
     54  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
     55    fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝
     56  λp,g,lbls1,lbls2,prf,flow.
     57  match flow with
     58  [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)»
     59  | FTailInit id b args ⇒ FTailInit … id b args
     60  | FEnd ⇒ FEnd ???
     61  ].
     62
     63coercion fin_step_flow_diff_lbls :
     64  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
     65  ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝
     66  fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???.
     67
     68definition monad_fin_step_flow_times_coerc :
     69  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
     70    monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝
     71    λp,g,lbls1,lbls2,M,A,H,m.
     72    ! 〈flow,a〉 ← m ;
     73    return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed.
     74
     75coercion fin_step_flow_monad_times :
     76  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
     77    ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝
     78  monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?).
     79
     80definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty.
     81  seq_list_labels … (\fst b) @
     82  match ty return λx.stmt_type_if ? x ??? → ? with
     83  [ SEQ ⇒ step_labels …
     84  | FIN ⇒ fin_step_labels …
     85  ] (\snd b).
     86
     87definition eval_block_cont :
     88  ∀globals.∀p : sem_params.∀ty.genv globals p →
     89  state p → ∀b : block_cont p globals ty.
     90  IO io_out io_in (
     91    (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) ×
     92    (state p)) ≝ λglobals,p,ty,ge,st.
     93  match ty return λx.∀b : block_cont p globals x.
     94    IO io_out io_in (
     95      (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) ×
     96      (state p))
     97  with
     98  [ SEQ ⇒ λb.
     99    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
     100    match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with
     101    [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
     102    | Proceed ⇒ eval_step … ge st' (\snd b)
     103    | Init _ _ _ _ ⇒
     104      Error … (msg ExecutingInternalCallInBlock)
     105    ]
     106  | FIN ⇒ λb.
     107    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
     108    match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with
     109    [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
     110    | Proceed ⇒ eval_fin_step … ge st' (\snd b)
     111    | Init _ _ _ _ ⇒
     112      Error … (msg ExecutingInternalCallInBlock)
     113    ]
     114  ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
     115
     116lemma m_pred
     117
     118lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
     119  ∀f : X → monad M Y.m_pred MP P … m →
     120  ! x ← m ; f x = ! x ← 
     121
     122definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
     123  λp,globals,lbls,A,flp.
     124  match \fst flp with
     125  [ Init _ _ _ _ ⇒ False
     126  | _ ⇒ True
     127  ].
     128
     129definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
     130  λp,globals,lbls,A,flp.
     131  match \fst flp with
     132  [ Proceed ⇒ True
     133  | _ ⇒ False
     134  ].
     135
     136definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
     137λp,globals,ge,s.match s with
     138[ CALL_ID f args dest ⇒
     139  Try
     140    ! b ← find_symbol … ge f ;
     141    ! fd ← find_funct_ptr … ge b ;
     142    match fd with
     143    [ Internal _ ⇒ return False
     144    | External _ ⇒ return True
     145    ]
     146  catch ⇒
     147    True
     148| extension c ⇒
     149  ∀st : state p.
     150  pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
     151| _ ⇒ True
     152].
     153
     154definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].
     155
     156lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
     157  err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
     158#O #I #X #Y * //
     159qed.
     160
     161lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
     162#O #I #X #m elim m // qed.
     163lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
     164#X #m elim m // qed.
     165
     166lemma never_calls_no_init : ∀p,globals,ge,s.
     167  never_calls p globals ge s →
     168  ∀st : state p.
     169  pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
     170#p#g#ge * //
     171[10,12:
     172|*:
     173  #a #b #c try #d try #e try #f try #g
     174  @res_io_pred
     175  @(mp_bind … (λ_.True) … (pred_res_True …))
     176  #st *  try (@mp_return @I)
     177  @(mp_bind … (λ_.True) … (pred_res_True …))
     178  #st * [9: elim st] normalize nodelta try (@mp_return @I)
     179  @(mp_bind … (λ_.True) … (pred_res_True …))
     180  #st *  try (@mp_return @I)
     181  @(mp_bind … (λ_.True) … (pred_res_True …))
     182  #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
     183  @(mp_bind … (λ_.True) … (pred_res_True …))
     184  #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
     185  try (@mp_return @I)
     186  @(mp_bind … (λ_.True) … (pred_res_True …))
     187  #st * @mp_return @I
     188]
     189[ #id #args #dest #H whd in H;
     190  #st change with (! x ← ? ; ?) in match (eval_step ?????);
     191  elim (find_symbol ????) in H ⊢ %; [//]
     192  #b >m_return_bind  >m_return_bind
     193  change with (! x ← ? ; ?) in match (eval_call_block ?????????);
     194  elim (find_funct_ptr ????) [//]
     195  #fd >m_return_bind  >m_return_bind
     196  elim fd #fn normalize nodelta *
     197  @(mp_bind … (λ_.True)) [//]
     198  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
     199  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
     200  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
     201  #st * @mp_return %
     202| #s #H @H
     203]
     204qed.
     205
     206lemma unbranching_truly_sequential : ∀p,globals,ge,s.
     207  unbranching p globals ge s →
     208  ∀st : state p.
     209  pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
     210#p#globals#ge#s * #H #G #st
     211lapply (never_calls_no_init … H st) @m_pred_mp
     212>G * *
     213[ * #lbl * | #id #fd #args #dest ] #st * %
     214qed.
     215
     216lemma seq_list_labels_append : ∀p,globals,b1,b2.
     217  seq_list_labels p globals (b1 @ b2) =
     218  seq_list_labels … b1 @ seq_list_labels … b2.
     219#p #g #b1 elim b1
     220[ //
     221| #hd #tl #IH #b2 whd in ⊢ (??%%);
     222  >associative_append <IH %
     223]
     224qed.
     225
     226lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
     227  eval_seq_list globals p ge st (b1@b2) =
     228  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
     229  match flow with
     230  [ Proceed ⇒
     231    ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
     232    return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
     233  | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
     234  ].
     235[2,3,4:
     236  #lbl #H >seq_list_labels_append
     237  [1,2: @Exists_append_l | @Exists_append_r ] @H ]
     238#globals#p#ge#st#b1 lapply st -st elim b1
     239[ #st #b2 >m_return_bind normalize nodelta
     240  <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
     241  @m_bind_ext_eq **
     242  [ * #lbl #H | #id #fd #args #dest ] #st' %
     243| #hd #tl #IH #st #b2
     244  whd in match (? @ b2);
     245  whd in match (eval_seq_list ?????);
     246  whd in match (eval_seq_list ???? (hd :: tl));
     247  >m_bind_bind
     248  @m_bind_ext_eq
     249  ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
     250  [1,2: @m_return_bind]
     251  >m_bind_bind
     252  >IH >m_bind_bind
     253  @m_bind_ext_eq **
     254  [#lbl | #id #fd #args #dest ] #st' normalize nodelta
     255  >m_return_bind
     256  [1,2: @m_return_bind ]
     257  >m_bind_bind normalize nodelta
     258  @m_bind_ext_eq **
     259  [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
     260]
     261qed.
     262
     263lemma eval_seq_list_unbranching :
     264∀globals,p,ge,st,b.
     265  All ? (unbranching … ge) b →
     266  pred_io … (λ_.True) (truly_sequential …)
     267    (eval_seq_list globals p ge st b).
     268#globals#p#ge#st #b lapply st -st elim b
     269[ #st * %
     270| #hd #tl #IH #st * #hd_ok #tl_ok
     271  @mp_bind
     272  [2: @(unbranching_truly_sequential … hd_ok st) |]
     273  ** [#lbl|#id#fd#args#dest] #st' *
     274  normalize nodelta
     275  @mp_bind [2: @(IH st' tl_ok)|]
     276  ** [#lbl|#id#fd#args#dest] #st'' * %
     277]
     278qed.
     279
     280lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
     281  pred_io O I A Perr P v →
     282  rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
     283#O #I #A #Perr #P #v elim v
     284[ #o #f #IH whd in ⊢ (%→%);
     285  #H %{(refl …)} #i @IH @H
     286|*: /2/
     287]
     288qed.
     289
     290lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
     291  All ? (unbranching … ge) b1 →
     292  eval_seq_list globals p ge st (b1@b2) =
     293  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
     294  ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
     295  return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
     296[2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
     297#globals #p #ge #st #b1 #b2 #H
     298>eval_seq_list_append
     299@mr_bind
     300[2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
     301** [#lbl|#id#fd#args#dest] #st
     302#y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
     303qed.
     304
     305lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
     306  block_cont_labels p globals ty (b1 @ b2) =
     307  block_cont_labels … b1 @ block_cont_labels … b2.
     308#p #g #ty * #l1 #s1 * #l2 #s2
     309whd in match (〈?,?〉@?); whd in ⊢ (??%?);
     310>seq_list_labels_append
     311>associative_append
     312>associative_append
     313>associative_append %
     314qed.
     315
     316lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
     317  ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
     318  eval_block_cont ??? ge st (b1@b2) =
     319  ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
     320  match ty return λx.
     321    block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
     322  [ SEQ ⇒ λb2.
    41323    match flow with
    42     [ Proceed ⇒
    43       ! 〈tr2, st〉 ← eval_block_cont globals p ge st id tl dst ;
    44       return 〈tr1 ⧺ tr2, st〉
    45     | Init id fn args dest ⇒
    46       ! ra ← opt_to_res … (msg SuccessorNotProvided) dst ;
    47       let st' ≝ set_frms … (save_frame … ra dest st) st in
    48       ! st ← do_call ?? ge st' id fn args ;
    49       return 〈tr1, st〉
    50     | Redirect l ⇒
    51       ! st ← goto_no_seq ? p … ge l st id ;
    52       return 〈tr1, st〉
    53     ]
     324    [ Proceed ⇒
     325      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
     326      return 〈?, st''〉
     327    | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
     328    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
     329    ]
     330  | FIN ⇒ λb2.
     331    match flow with
     332    [ Proceed ⇒
     333      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
     334      return 〈?, st''〉
     335    | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
     336    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
     337    ]
     338  ] b2.
     339[3,5: whd in flow'; @flow'
     340  #lbl >block_cont_labels_append @Exists_append_r
     341|2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
     342]
     343#globals#p * whd in match stmt_type_if; normalize nodelta
     344#ge#st * #l1 #s1 * #l2 #s2
     345whd in match (〈?,?〉@?);
     346whd in match eval_block_cont; normalize nodelta
     347>m_bind_bind
     348>eval_seq_list_append
     349>m_bind_bind
     350@m_bind_ext_eq
     351
     352 whd in ⊢ (??%?);
     353    match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
     354    [ SEQ ⇒
     355    | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
     356    ]
     357  | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
    54358  ].
    55  
    56 lemma Eapp_E0 : ∀tr1 : trace.tr1 ⧺ E0 = tr1 ≝ append_nil ….
    57 
    58 (* just like repeat, but without the full_exec infrastructure *)
    59 let rec repeat_eval_state n globals (p:sem_params) (ge : genv globals p)
     359#globals#p#ty#ge#st*#l1#s1*#l2#s2
     360whd in match (〈?,?〉@?);
     361whd in match eval_block_cont; normalize nodelta
     362>m_bind_bind
     363>eval_seq_list_append
     364>m_bind_bind
     365@m_bind_ext_eq
     366** [#l|#id#fd#args#dest] normalize nodelta #st'
     367[1,2:>m_return_bind normalize nodelta
     368  [ >m_return_bind ] % ]
     369change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
     370>m_bind_bind whd in match stmt_type_if;
     371normalize nodelta
     372>m_bind_bind
     373@m_bind_ext_eq
     374**[#l|#id#fd#args#dest] normalize nodelta #st''
     375[1,2: >m_return_bind normalize nodelta % | % ]
     376qed.
     377
     378
     379
     380(* just like repeat, but without the full_exec infrastructure, and it
     381   stops upon a non-proceed flow cmd *)
     382let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
    60383  (st : state_pc p) on n :
    61     IO io_out io_in (trace×(state_pc p)) ≝
     384    IO io_out io_in (bool × (state_pc p)) ≝
    62385match n with
    63 [ O ⇒ return 〈E0, st〉
     386[ O ⇒ return 〈false,st〉
    64387| S k ⇒
    65   ! 〈tr1, st〉 ← eval_state globals p ge st ;
    66   ! 〈tr2, st〉 ← repeat_eval_state k globals p ge st ;
    67   return 〈tr1 ⧺ tr2, st〉
     388  ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
     389  if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
    68390].
    69391
    70 lemma repeat_eval_state_plus : ∀n1,n2,globals, p, ge, st.
    71   repeat_eval_state (n1 + n2) globals p ge st =
    72   ! 〈tr1, st〉 ← repeat_eval_state n1 globals p ge st ;
    73   ! 〈tr2, st〉 ← repeat_eval_state n2 globals p ge st ;
    74   return 〈tr1 ⧺ tr2, st〉.
     392definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
     393λp,g,ty,b.S (|\fst b|).
     394
     395interpretation "block cont size" 'norm b = (block_size ??? b).
     396
     397lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
     398  repeat_eval_state_flag (n1 + n2) globals p ge st =
     399  ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
     400  if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
    75401#n1 elim n1 -n1 [| #n1 #IH]
    76402#n2 #globals #p #ge #st
    77 [ >m_return_bind change with n2 in match (0 + n2);
    78   change with (! x ← ? ; ?) in ⊢ (???%);
    79   <(m_bind_return … (repeat_eval_state ?????)) in ⊢ (??%?);
    80   @m_bind_ext_eq * //
    81 | change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
    82   change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S n1) ????);
     403[ @m_return_bind
     404| change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
     405  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
    83406  >m_bind_bind in ⊢ (???%);
    84   @m_bind_ext_eq * #tr1 #st1
    85   >IH >m_bind_bind in ⊢ (??%?); >m_bind_bind in ⊢ (???%);
    86   @m_bind_ext_eq * #tr2 #st2 >m_return_bind
    87   >m_bind_bind @m_bind_ext_eq * #tr3 #st3 >m_return_bind >Eapp_assoc %
    88 ]
    89 qed.
    90 
    91 lemma repeat_eval_state_one : ∀globals, p, ge, st.
    92   repeat_eval_state 1 globals p ge st = eval_state globals p ge st.
     407  @m_bind_ext_eq ** #st' normalize nodelta
     408  [ % | @IH ]
     409]
     410qed.
     411
     412lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
     413  repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
    93414#globals #p #ge #st
    94 change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????);
    95 <(m_bind_return … (eval_state ????)) in ⊢ (???%);
    96 @m_bind_ext_eq * #tr1 #st1 >m_return_bind >Eapp_E0 %
    97 qed.
    98 
    99 lemma If_true : ∀A.∀b : bool.∀f : b → A.∀g.∀prf' : bool_to_Prop b.If b then with prf do f prf else with prf do g prf = f prf'.
    100 #A * #f #g * normalize % qed.
     415change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
     416<(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
     417@m_bind_ext_eq ** #st %
     418qed.
    101419
    102420lemma eval_tunnel_step :
     
    105423  point_of_pointer ? p … (pc … st) = OK … src →
    106424  src ~~> dst in joint_if_code … fn →
    107   eval_state g p ge st =
    108     OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
     425  eval_state_flag g p ge st =
     426    return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    109427#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
    110 change with (! s ← ? ; ?) in match (eval_state ????);
     428change with (! s ← ? ; ?) in match (eval_state_flag ????);
    111429change with (! fn ← ? ; ?) in match (fetch_statement ?????);
    112430>pc_pt in ⊢ (??%?); >m_return_bind
    113431>fetch_fn in ⊢ (??%?); >m_return_bind
    114432>EQ1 in ⊢ (??%?);  >m_return_bind
    115 >EQ2 in ⊢ (??%?);  >m_return_bind
    116 change with (! st ← ? ; ?) in ⊢ (??%?);
    117 whd in match eval_stmt_flow; normalize nodelta
    118 change with (! ptr ← ? ; ?) in match (goto ?????);
    119 whd in match pointer_of_label; normalize nodelta
     433>EQ2 in ⊢ (??%?);
     434change with (! st ← ? ; ?) in match (eval_statement ?????);
     435whd in match eval_fin_step; normalize nodelta
     436>m_return_bind
     437whd in match eval_fin_step_flow; normalize nodelta
     438change with (! ptr ← ? ; ?) in match (goto ??????);
     439whd in match pointer_of_label_in_block; normalize nodelta
     440whd in match fetch_function in fetch_fn;
     441normalize nodelta in fetch_fn;
    120442>fetch_fn in ⊢ (??%?); >m_return_bind
    121 >EQ2 in ⊢ (??%?); >m_return_bind %
    122 qed.
    123 
     443>EQ2 in ⊢ (??%?); >m_return_bind
     444cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
     445elim (pointer_compat_from_ind … H) %
     446qed.
    124447
    125448lemma fetch_function_from_block_eq :
     
    131454@m_bind_ext_eq // qed.
    132455
     456(*
    133457lemma eval_tunnel :
    134458  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
     
    137461  src ~~>^* dst in joint_if_code … fn →
    138462  ∃n.repeat_eval_state n g p ge st =
    139     OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
     463    return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
    140464#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
    141465lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
     
    153477]
    154478#n' #EQ %{(S n')}
    155 change with (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
     479change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    156480>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    157 >EQ  >m_return_bind %
     481>EQ %
    158482qed.
    159483
     
    164488  src ~~>^+ dst in joint_if_code … fn →
    165489  ∃n.repeat_eval_state (S n) g p ge st =
    166     OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
     490    return set_pc … (pointer_of_point ? p (pc … st) dst) st.
    167491#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
    168492letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
     
    174498]
    175499#n #EQ %{n}
    176 change with (! 〈tr1,st1〉 ← ? ; ?) in match (repeat_eval_state ?????);
     500change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
    177501>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
    178 >EQ  >m_return_bind %
    179 qed.
     502>EQ %
     503qed.
     504*)
    180505
    181506lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
     
    190515qed.
    191516
    192 lemma eval_block_cont_in_code :
     517lemma eval_seq_list_in_code :
    193518  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
    194519  fetch_function … ge (pc … st) = OK … fn →
    195520  point_of_pointer ? p … (pc … st) = OK … src →
     521  All ? (never_calls … ge) B →
     522  seq_list_in_code … (joint_if_code … fn) src B dst →
     523  repeat_eval_state_flag (|B|) g p ge st =
     524   ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
     525   match flow with
     526   [ Redirect l ⇒
     527     ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
     528     return 〈true, st''〉
     529   | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
     530       (* dummy, never happens *)
     531   | Proceed ⇒
     532     let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
     533     return 〈false, mk_state_pc ? st' nxt_ptr〉
     534   ].
     535#p #g #ge #st #fn #src #B lapply src -src
     536lapply st -st elim B [|#hd #tl #IH]
     537#st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
     538[2: #EQ normalize in EQ; <EQ
     539  whd in match (eval_seq_list ???? [ ]);
     540  >m_return_bind normalize nodelta
     541  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
     542|1: * #n * #EQat #H
     543  change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
     544  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
     545  >m_bind_bind
     546  >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
     547  >m_bind_bind >m_bind_bind
     548  lapply (never_calls_no_init … hd_ok st) #hd_ok'
     549  @(mr_bind …
     550    (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
     551  [ lapply hd_ok' elim (eval_step ?????)
     552    [ #o #f #IH'
     553      whd in ⊢ (%→%); #G
     554      %{(refl …)} #i @IH' @G
     555    |*: #v whd in ⊢ (%→%); #H
     556      % [ % ] @H
     557    ]
     558  | ** [#lbl | #id #fd #args #dest ] #st'
     559    #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
     560    whd in match succ_pc; normalize nodelta
     561    >pc_pt >m_return_bind
     562    letin src' ≝ (point_of_succ p src n) in H ⊢ %;
     563    letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
     564    [>m_return_bind whd in match eval_step_flow; normalize nodelta
     565     whd in match (pblock ?);
     566     elim (goto … ge lbl st' ?)
     567     [ #st'' >m_return_bind %
     568     | #e %
     569     ]
     570    | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
     571      [ @fetch_fn
     572      | @point_of_pointer_of_point
     573      ]
     574    ]
     575  ]
     576]
     577qed.
     578
     579definition eval_block_cont_pc :
     580  ∀globals.∀p : sem_params.∀ty.genv globals p →
     581  state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
     582  IO io_out io_in (bool × (state_pc p)) ≝
     583  λglobals,p,ty,ge,st,b,nxt.
     584  ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
     585  match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
     586  [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
     587        (pointer_of_point ? p (pc ? st) nxt) flow
     588  | FIN ⇒ λflow.λ_.
     589    ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
     590    return 〈true, st'〉
     591  ] flow nxt.
     592
     593lemma eval_block_cont_in_code :
     594  ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
     595  fetch_function … ge (pc … st) = OK … fn →
     596  point_of_pointer ? p … (pc … st) = OK … src →
     597  All ? (never_calls … ge) (\fst B) →
    196598  src ~❨B❩~> dst in joint_if_code … fn →
    197   ∃n.repeat_eval_state n g p ge st =
    198     eval_block_cont g p ge st (block_id (pblock (pc … st))) B (! x ← dst; return pointer_of_point … p (pc … st) x).
    199 #p #g #ge #st #fn #src #B lapply src -src
    200 lapply st -st elim B [|#s|#s #B' #IH]
    201 #st #src #dst #fetch_fn #pc_pt
    202 [ cases dst [*] #z @eval_tunnel assumption
     599  repeat_eval_state_flag (|B|) g p ge st =
     600    eval_block_cont_pc g p ty ge st B dst.
     601#p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
     602* #mid * #l_in_code #s_in_code
     603change with (1 + |l|) in match (|?|);
     604>commutative_plus
     605>repeat_eval_state_flag_plus
     606change with (! x ← ? ; ?) in ⊢ (???%);
     607>m_bind_bind
     608>(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
     609>m_bind_bind
     610@m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
     611normalize nodelta
     612[ -s_in_code lapply dst -dst cases ty
     613  whd in match stmt_type_if; normalize nodelta
     614  #dst >m_return_bind
     615  [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
     616  normalize nodelta
     617  whd in match (pblock ?);
     618  elim (goto g p ge lbl st' ?) #x //
     619| %
     620| >m_return_bind normalize nodelta
     621  >repeat_eval_state_flag_one
     622  >m_bind_bind
     623  lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
     624  whd in match stmt_type_if; normalize nodelta
     625  #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
     626  whd in match eval_state_flag; normalize nodelta
     627  letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
     628  letin st_pc' ≝ (mk_state_pc ? st' pc')
     629  >(fetch_statement_eq … ?? s_in_code)
     630  [2,5: @point_of_pointer_of_point
     631  |3,6: @fetch_fn
     632  |*: >m_return_bind
     633    whd in match eval_statement; normalize nodelta
     634    @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
     635    whd in match succ_pc; normalize nodelta
     636    >point_of_pointer_of_point >m_return_bind
     637    >pointer_of_point_of_pointer [2: @refl |*:]
     638    [ >point_of_pointer_of_point >n_is_dst %
     639    | %
     640    ]
     641  ]
     642]
     643qed.
     644     cases dst [*] #z @eval_tunnel assumption
    203645| cases dst [2: #z *]]
    204646* #mid * #tunn [#H | * #n * #H #G ]
  • src/joint/semantics_paolo.ma

    r1882 r1949  
    6363
    6464axiom BadProgramCounter : String.
     65
     66definition function_of_block :
     67 ∀pars : params.
     68 ∀globals.
     69  genv globals pars →
     70  block →
     71  res (joint_internal_function … pars) ≝
     72  λpars,blobals,ge,b.
     73  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     74  match def with
     75  [ Internal def' ⇒ OK … def'
     76  | External _ ⇒ Error … [MSG BadProgramCounter]].
     77 
    6578(* this can replace graph_fetch function and lin_fetch_function *)
    6679definition fetch_function:
     
    7083  cpointer →
    7184  res (joint_internal_function … pars) ≝
    72  λpars,globals,ge,p.
    73   let b ≝ pblock p in
    74   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    75   match def with
    76   [ Internal def' ⇒ OK … def'
    77   | External _ ⇒ Error … [MSG BadProgramCounter]].
    78 
    79 inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
    80   | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
    81   | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
    82   | Proceed  : step_flow p globals. (* go to implicit successor *)
    83 
    84 inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
    85   | SRedirect : label → stmt_flow p globals
    86   | SProceed : succ p → stmt_flow p globals
    87   | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
    88   | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
    89   | SEnd  : stmt_flow p globals. (* end flow *)
    90 
     85 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
     86
     87inductive step_flow (p : params) (globals : list ident) (labels : list label) : Type[0] ≝
     88  | Redirect : (Σl.In ? labels l) → step_flow p globals labels (* used for goto-like flow alteration *)
     89  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals labels (* call a function with given id, then proceed *)
     90  | Proceed  : step_flow p globals labels. (* go to implicit successor *)
     91
     92inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
     93  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
     94  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
     95  | FEnd  : fin_step_flow p globals labels. (* end flow *)
    9196
    9297record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
     
    164169   serialization and on whether the call is a tail one. *)
    165170definition eval_call_block:
    166  ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
     171 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.∀lbls.
    167172  genv globals p → state p' → block → call_args p → call_dest p →
    168     IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝
    169  λglobals,p,p',ge,st,b,args,dest.
     173    IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
     174 λglobals,p,p',lbls,ge,st,b,args,dest.
    170175  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    171176    match fd with
    172177    [ Internal fn ⇒
    173       return 〈Init … (block_id b) fn args dest, E0, st〉
     178      return 〈Init … (block_id b) fn args dest, st〉
    174179    | External fn ⇒
    175180      ! params ← fetch_external_args … p' fn st : IO ???;
     
    181186      let vs ≝ [mk_val ? evres] in
    182187      ! st ← set_result … p' vs st : IO ???;
    183       return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     188      return 〈Proceed ???, st〉
    184189      ].
    185190
     
    218223  return 〈st'', pr〉.
    219224
    220 definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
    221   match flow with
    222   [ SProceed _ ⇒ False
    223   | SInit _ _ _ _ _ ⇒ False
    224   | _ ⇒ True
    225   ].
    226 
    227225(* parameters that need full params to have type of functions,
    228226   but are still independent of serialization *)
     
    231229  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    232230  (* change of pc must be left to *_flow execution *)
    233   ; exec_extended: ∀globals.genv globals pp → ext_step pp →
     231  ; exec_extended: ∀globals.genv globals pp → ∀s : ext_step pp.
    234232      state msu_pars →
    235       IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
    236   ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
     233      IO io_out io_in ((step_flow pp globals (ext_step_labels … s))× (state msu_pars))
     234  ; exec_fin_extended: ∀globals.genv globals pp → ∀s : ext_fin_stmt pp.
    237235      state msu_pars →
    238       IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
     236      IO io_out io_in ((fin_step_flow pp globals (ext_fin_stmt_labels … s))×(state msu_pars))
    239237  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    240238  }.
     
    305303  ! fn ← fetch_function … ge ptr ;
    306304  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     305 
     306definition pointer_of_label_in_block : ∀p : params.∀ msp : more_sem_params p.∀globals.
     307  genv globals p → block → label → res cpointer ≝
     308  λp,msp,globals,ge,b,lbl.
     309  ! fn ← function_of_block … ge b ;
     310  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     311            (point_of_label … (joint_if_code … fn) lbl) ;
     312  return (mk_pointer Code (mk_block Code (block_id b)) ? (offset_of_point p msp pt) : Σp.?). // qed.
    307313
    308314definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    309315  genv globals p → cpointer → label → res cpointer ≝
    310   λp,msp,globals,ge,ptr,lbl.
    311   ! fn ← fetch_function … ge ptr ;
    312   ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    313             (point_of_label … (joint_if_code … fn) lbl) ;
    314   return pointer_of_point ? msp ptr pt.
     316  λp,msp,globals,ge,ptr.
     317  pointer_of_label_in_block p msp globals ge (pblock ptr).
    315318
    316319definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     
    332335
    333336definition goto: ∀globals. ∀p:sem_params.
    334   genv globals p → label → state_pc p → res (state_pc p) ≝
    335  λglobals,p,ge,l,st.
    336   ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
    337   return set_pc … newpc st.
     337  genv globals p → label → state p → block → res (state_pc p) ≝
     338 λglobals,p,ge,l,st,b.
     339  ! newpc ← pointer_of_label_in_block ? p … ge b l ;
     340  return mk_state_pc ? st newpc.
    338341
    339342(*
     
    342345*)
    343346
    344 definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
    345  λp,l,st.
    346  ! nw ← succ_pc ? p … (pc ? st) l ;
    347  return set_pc … nw st.
     347definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
     348 λp,l,st,pc.
     349 ! newpc ← succ_pc ? p … pc l ;
     350 return mk_state_pc … st newpc.
    348351
    349352axiom MissingSymbol : String.
     
    355358definition eval_step :
    356359 ∀globals.∀p:sem_params. genv globals p → state p →
    357   joint_step p globals →
    358   IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
     360  ∀s:joint_step p globals.
     361  IO io_out io_in ((step_flow p globals (step_labels … s))×(state p)) ≝
    359362 λglobals,p,ge,st,seq.
    360   match seq with
     363  match seq return λx.IO ?? ((step_flow ?? (step_labels … x) × ?)) with
    361364  [ extension c ⇒
    362365    exec_extended … ge c st
    363366  | COST_LABEL cl ⇒
    364     return 〈Proceed ??, Echarge cl, st〉
     367    return 〈Proceed ???, st〉
    365368  | COMMENT c ⇒
    366     return 〈Proceed ??, E0, st〉
     369    return 〈Proceed ???, st〉
    367370  | LOAD dst addrl addrh ⇒
    368371    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    371374    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    372375    ! st ← acca_store p … dst v st ;
    373     return 〈Proceed ??, E0, st〉
     376    return 〈Proceed ???, st〉
    374377  | STORE addrl addrh src ⇒
    375378    ! vaddrh ← dph_arg_retrieve … st addrh;
     
    378381    ! v ← acca_arg_retrieve … st src;
    379382    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    380     return 〈Proceed ??, E0, set_m … m' st〉
     383    return 〈Proceed ???, set_m … m' st〉
    381384  | COND src ltrue ⇒
    382385    ! v ← acca_retrieve … st src;
    383386    ! b ← bool_of_beval v;
    384387    if b then
    385       return 〈Redirect ?? ltrue, E0, st〉
     388      return 〈Redirect ??? ltrue, st〉
    386389    else
    387       return 〈Proceed ??, E0, st〉
     390      return 〈Proceed ???, st〉
    388391  | ADDRESS ident prf ldest hdest ⇒
    389392    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
     
    391394    ! st' ← dpl_store … ldest laddr st;
    392395    ! st'' ← dph_store … hdest haddr st';
    393     return 〈Proceed ??, E0, st''〉
     396    return 〈Proceed ???, st''〉
    394397  | OP1 op dacc_a sacc_a ⇒
    395398    ! v ← acca_retrieve … st sacc_a;
     
    397400    let v' ≝ BVByte (op1 eval op v) in
    398401    ! st ← acca_store … dacc_a v' st;
    399     return 〈Proceed ??, E0, st〉
     402    return 〈Proceed ???, st〉
    400403  | OP2 op dacc_a sacc_a src ⇒
    401404    ! v1 ← acca_arg_retrieve … st sacc_a;
     
    409412    ! st' ← acca_store … dacc_a v' st;
    410413      let st'' ≝ set_carry … carry st' in
    411     return 〈Proceed ??, E0, st''〉
     414    return 〈Proceed ???, st''〉
    412415  | CLEAR_CARRY ⇒
    413416    let st' ≝ set_carry … BVfalse st in
    414     return 〈Proceed ??, E0, st'〉
     417    return 〈Proceed ???, st'〉
    415418  | SET_CARRY ⇒
    416419    let st' ≝ set_carry … BVtrue st in
    417     return 〈Proceed ??, E0, st'〉
     420    return 〈Proceed ???, st'〉
    418421  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    419422    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     
    426429    ! st' ← acca_store … dacc_a_reg v1' st;
    427430    ! st'' ← accb_store … dacc_b_reg v2' st';
    428     return 〈Proceed ??, E0, st''〉
     431    return 〈Proceed ???, st''〉
    429432  | POP dst ⇒
    430433    ! 〈st',v〉 ← pop p st;
    431434    ! st'' ← acca_store p p dst v st';
    432     return 〈Proceed ??, E0, st''〉
     435    return 〈Proceed ???, st''〉
    433436  | PUSH src ⇒
    434437    ! v ← acca_arg_retrieve … st src;
    435438    ! st ← push … st v;
    436     return 〈Proceed ??, E0, st〉
     439    return 〈Proceed ???, st〉
    437440  | MOVE dst_src ⇒
    438441    ! st ← pair_reg_move … st dst_src ;
    439     return 〈Proceed ??, E0, st〉
     442    return 〈Proceed ???, st〉
    440443  | CALL_ID id args dest ⇒
    441444    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     
    445448  | (* TODO: to prove *)
    446449    elim daemon
     450  | %1 %
    447451  ] qed.
    448452
    449 definition eval_step_flow :
    450  ∀globals.∀p:sem_params.step_flow p globals →
    451   succ p → stmt_flow p globals ≝
    452  λglobals,p,cmd,nxt.
    453  match cmd with
    454  [ Redirect l ⇒ SRedirect … l
    455  | Init id fn args dest ⇒ SInit … id fn args dest nxt
    456  | Proceed ⇒ SProceed … nxt
    457  ].
    458 
    459 definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
    460   state p → joint_statement … p globals →
    461   IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
     453definition eval_fin_step : ∀globals: list ident.∀p:sem_params. genv globals p →
     454  state p → ∀s : joint_fin_step … p globals.
     455  IO io_out io_in ((fin_step_flow p globals (fin_step_labels … s))×(state p)) ≝
    462456 λglobals,p,ge,st,s.
    463   match s with
    464     [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉
    465     | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
    466     | sequential seq l ⇒
    467       ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
    468       return 〈eval_step_flow … flow l, tr, st〉
    469     | extension_fin c ⇒
    470       ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
    471       return 〈pi1 … flow, tr, st〉
    472     ].
    473 
    474 definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
    475   state p → (Σs : joint_statement … p globals.no_seq … s) →
    476   IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
    477  λglobals,p,ge,st,s_sig.
    478   match s_sig with
    479   [ mk_Sig s s_prf ⇒
    480     match s return λx.no_seq p globals x → ? with
    481     [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉
    482     | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
    483     | sequential seq l ⇒ Ⓧ
    484     | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
    485     ] s_prf
    486   ]. % qed.
    487 
    488 let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
    489   (v2 : IO O I B) on v1 : Prop ≝
    490   match v1 with
    491   [ Value x ⇒
    492     match v2 with
    493     [ Value y ⇒
    494       P x y
    495     | _ ⇒ False
    496     ]
    497   | Wrong _ ⇒
    498     match v2 with
    499     [ Wrong _ ⇒ True
    500     | _ ⇒ False
    501     ]
    502   | Interact o1 f1 ⇒
    503     match v2 with
    504     [ Interact o2 f2 ⇒
    505       ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
    506     | _ ⇒ False
    507     ]
    508   ]. <prf @i qed.
    509 
    510 definition IORel ≝ λO,I.
    511   mk_MonadRel (IOMonad O I) (IOMonad O I)
    512     (rel_io O I) ???.
    513 [//
    514 |#X #Y #Z #W #relin #relout #m elim m
    515   [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
    516     #f1 #f2 #G' whd %{(refl …)} #i
    517     @(IH … (G i) f1 f2 G')
    518   | #v * [#o #f * | #v' | #e *]
    519     #Pvv' #f #g #H normalize @H @Pvv'
    520   | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
    521   ]
    522 | #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
    523   [1,4,7: #o' #f' [2,3: *]
    524     normalize * #prf destruct(prf) normalize #G
    525     % [%] normalize #i @IH @G
    526   |2,5,8: #v' [1,3: *]
    527     @H
    528   |*: #e' [1,2: *] //
    529   ]
    530 ]
    531 qed.
    532 
    533 lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
    534   reflexive ? (m_rel ?? (IORel O I) ?? rel).
    535 #O #I #X #rel #H #m elim m
    536 [ #o #f #IH whd %[%] #i normalize @IH
    537 | #v @H
    538 | #e %
    539 ]
    540 qed.
    541 
    542 lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
    543   (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
    544   ∀m,n,o.
    545   m_rel ?? (IORel O I) … rel1 m n →
    546   m_rel ?? (IORel O I) … rel2 n o →
    547   m_rel ?? (IORel O I) … rel3 m o.
    548 #O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
    549 [ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
    550   normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
    551 | #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
    552   @H
    553 | #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
    554 ]
    555 qed.
    556 
    557 lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
    558   ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
    559   ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
    560                   m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
    561 #M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
    562 @(mr_bind … H) @G qed.
    563 
    564 lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
    565   m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
    566 #M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
    567 qed.
    568 
    569 lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
    570   pi1 ?? s1 = s2 →
    571   m_rel ?? (IORel ??) ??
    572     (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
    573       \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
    574     (eval_statement_no_seq globals p ge st s1)
    575     (eval_statement globals p ge st s2).
    576 #globals #p #ge #st * * [#s #n | #lbl || #c ]*
    577 #s2 #EQ destruct(EQ)
    578 whd in match eval_statement;
    579 whd in match eval_statement_no_seq;
    580 normalize nodelta
    581 [1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
    582 <(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
    583 @(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
    584 #x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
    585 qed.
     457  match s return λx.IO ?? ((fin_step_flow ?? (fin_step_labels … x)) × ?) with
     458    [ GOTO l ⇒ return 〈FRedirect ??? l, st〉
     459    | RETURN ⇒ return 〈FEnd ???, st〉
     460    | extension_fin c ⇒ exec_fin_extended … ge c st
     461    ]. %1 % qed.
     462
    586463
    587464definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
     
    598475    return mk_state_pc ? st' pc. % qed.
    599476
    600 definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
    601   state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
    602   λglobals,p,ge,st,flow.
    603   match flow with
    604   [ SRedirect l ⇒ goto … ge l st
    605   | SProceed nxt ⇒ next ? nxt st
    606   | SInit id fn args dest nxt ⇒
    607     ! ra ← succ_pc ? p … (pc … st) nxt ;
    608     let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
    609     do_call ?? ge st' id fn args
    610   | STailInit id fn args ⇒
     477(* The pointer provided is the one to the *next* instruction.
     478   The boolean tells wether a flow changement has occurred (i.e.
     479   a non Proceed cmd was issued). Used in linking block evaluation
     480   with regular one *)
     481definition eval_step_flow :
     482 ∀globals.∀p:sem_params.∀lbls.genv globals p →
     483  state p → cpointer → step_flow p globals lbls →
     484    res (bool × (state_pc p)) ≝
     485 λglobals,p,lbls,ge,st,nxt,cmd.
     486 match cmd with
     487  [ Redirect l ⇒
     488    ! st ← goto … ge l st (pblock nxt) ; return 〈true, st〉
     489  | Init id fn args dest ⇒
     490    let st' ≝ set_frms … (save_frame … nxt dest st) st in
     491    ! st ← do_call ?? ge st' id fn args ;
     492    return 〈true, st〉
     493  | Proceed ⇒
     494    return 〈false, mk_state_pc ? st nxt〉
     495  ].
     496
     497definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀lbls. genv globals p →
     498  state p → block → fin_step_flow p globals lbls → res (state_pc p) ≝
     499  λglobals,p,lbls,ge,st,b,cmd.
     500  match cmd with
     501  [ FRedirect l ⇒ goto … ge l st b
     502  | FTailInit id fn args ⇒
    611503    do_call … ge st id fn args
    612   | SEnd ⇒
    613     ! 〈st,ra〉 ← fetch_ra … st ;
    614     ! st' ← pop_frame … ge st;
    615     return mk_state_pc ? st' ra
     504  | FEnd ⇒
     505    ! 〈st',ra〉 ← fetch_ra … st ;
     506    ! st'' ← pop_frame … ge st;
     507    return mk_state_pc ? st'' ra
    616508  ].
    617509
    618 definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
    619   state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
    620     IO io_out io_in (state_pc p) ≝
    621   λglobals,p,ge,st,id,flow_sig.
    622   match flow_sig with
    623   [ mk_Sig flow prf ⇒
    624     match flow return λx.flow_no_seq p globals x → ? with
    625     [ SRedirect l ⇒ λ_.
    626       ! newpc ← pointer_of_label ? p … ge
    627         (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
    628       return mk_state_pc … st newpc
    629     | STailInit id fn args ⇒ λ_.
    630       do_call … ge st id fn args
    631     | SEnd ⇒ λ_.
    632       ! 〈st,ra〉 ← fetch_ra … st ;
    633       ! st' ← pop_frame … ge st;
    634       return mk_state_pc ? st' ra
    635     | _ ⇒ Ⓧ
    636     ] prf
    637   ]. % qed.
    638 
    639 lemma pointer_of_label_eq_with_id :
    640 ∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
    641   block_id (pblock ptr1) = block_id (pblock ptr2) →
    642   pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
    643 #g #p #ge
    644 ** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
    645 ** #ty2 * #r2 #id2 #H2 inversion H2
    646 [1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
    647 qed.
    648 
    649 
    650 lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
    651   ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
    652   pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
    653     (eval_stmt_flow_no_seq g p ge st id s1) =
    654     (eval_stmt_flow g p ge st s2).
    655 #g#p#ge#st#id'
    656 **[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
    657 #s2 #EQ #EQ' destruct(EQ)
    658 whd in match eval_stmt_flow_no_seq; normalize nodelta
    659 whd in match eval_stmt_flow; normalize nodelta
    660 [2,3: %]
    661 whd in match goto; normalize nodelta
    662 whd in match set_pc; normalize nodelta
    663 >pointer_of_label_eq_with_id [% | >EQ' % |]
    664 qed.
    665 
    666 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
    667   state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
     510definition eval_statement :
     511 ∀globals.∀p:sem_params.genv globals p →
     512  state_pc p → joint_statement p globals →
     513    IO io_out io_in (bool × (state_pc p)) ≝
     514 λglobals,p,ge,st,stmt.
     515 match stmt with
     516 [ sequential s nxt ⇒
     517   ! 〈flow, st'〉 ← eval_step … ge st s ;
     518   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
     519   eval_step_flow … ge st' nxtptr flow
     520 | final s ⇒
     521   ! 〈flow, st'〉 ← eval_fin_step … ge st s ;
     522   ! st ← eval_fin_step_flow … ge st' (pblock … (pc … st)) flow ;
     523   return 〈true, st〉
     524 ].
     525
     526definition eval_state_flag : ∀globals: list ident.∀p:sem_params. genv globals p →
     527  state_pc p → IO io_out io_in (bool × (state_pc p)) ≝
    668528  λglobals,p,ge,st.
    669529  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
    670   ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
    671   let st ≝ set_no_pc … st_npc st in
    672   ! st ← eval_stmt_flow … ge st flow;
    673   return 〈tr, st〉.
    674 
     530  eval_statement … ge st s.
     531
     532definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
     533  state_pc p → IO io_out io_in (state_pc p) ≝
     534  λglobals,p,ge,st.
     535  ! 〈flag,st'〉 ← eval_state_flag … ge st ;
     536  return st'.
     537
     538(* Paolo: what if in an intermediate language main finishes with an external
     539  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
     540  not static... *)
    675541definition is_final: ∀globals:list ident. ∀p: sem_params.
    676542  genv globals p → cpointer → state_pc p → option int ≝
     
    678544  do s ← fetch_statement ? p … ge (pc … st);
    679545  match s with
    680    [ RETURN ⇒
     546  [ final s' ⇒
     547    match s' with
     548    [ RETURN ⇒
    681549      do 〈st,ra〉 ← fetch_ra … st;
    682550      if eq_pointer ra exit then
     
    685553      else
    686554       Error ? [ ]
    687    | _ ⇒ Error ? [ ]]).
     555   | _ ⇒ Error ? [ ]
     556   ]
     557 | _ ⇒ Error ? [ ]
     558 ]).
    688559 
    689560record evaluation_parameters : Type[1] ≝
     
    694565 }.
    695566
     567(* Paolo: with structured traces, eval need not emit labels. However, this
     568  changes trans_system. For now, just putting a dummy thing for
     569  the transition. *)
    696570definition joint_exec: trans_system io_out io_in ≝
    697571  mk_trans_system … evaluation_parameters (λG. state_pc G)
    698572   (λG.is_final (globals G) G (genv2 G) (exit G))
    699    (λG.eval_state (globals G) G (genv2 G)).
     573   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
    700574
    701575definition make_global :
Note: See TracChangeset for help on using the changeset viewer.