Changeset 1626 for src


Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

Location:
src
Files:
1 added
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1612 r1626  
    8282.
    8383
    84 definition var_types ≝ identifier_map SymbolTag var_type.
     84definition var_types ≝ identifier_map SymbolTag (var_type × type).
    8585
    8686axiom UndeclaredIdentifier : String.
     
    8989λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
    9090
    91 definition local_id : var_types → ident → Prop ≝
    92 λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
     91(* Assert that an identifier is a local variable with the given typ. *)
     92definition local_id : var_types → ident → typ → Prop ≝
     93λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False | _ ⇒ t = typ_of_type (\snd vt) ] | _ ⇒ False ].
    9394
    9495(* Note that the semantics allows locals to shadow globals.
     
    105106].
    106107
    107 definition characterise_vars : list (ident×region) → function → var_types × nat ≝
     108definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝
    108109λglobals, f.
    109   let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
     110  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
    110111  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
    111112  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
     
    115116                           then 〈Stack stack_high,stack_high + sizeof ty〉
    116117                           else 〈Local, stack_high〉 in
    117       〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
     118      〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
    118119  〈m,stacksize〉.
    119120
    120 lemma local_id_add_global : ∀vars,id,r,id'.
    121   local_id (add ?? vars id (Global r)) id' → local_id vars id'.
    122 #var #id #r #id'
     121lemma local_id_add_global : ∀vars,id,r,t,id',t'.
     122  local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'.
     123#var #id #r #t #id' #t'
    123124whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
    124125cases (identifier_eq ? id id')
     
    127128] qed.
    128129
    129 lemma local_id_add_miss : ∀vars,id,t,id'.
    130   id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
    131 #vars #id #t #id' #NE
     130lemma local_id_add_miss : ∀vars,id,vt,id',t'.
     131  id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'.
     132#vars #id #vt #id' #t' #NE
    132133whd in ⊢ (% → %);
    133134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
     
    138139lemma characterise_vars_all : ∀l,f,vars,n.
    139140  characterise_vars l f = 〈vars,n〉 →
    140   ∀i. local_id vars i
    141       Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
     141  ∀i,t. local_id vars i t
     142        Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f).
    142143#globals #f
    143144whd in ⊢ (∀_.∀_.??%? → ?);
    144145elim (fn_params f @ fn_vars f)
    145 [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
     146[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind
    146147  elim globals in H;
    147148  [ normalize //
    148   | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
     149  | * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H)
    149150  ]
    150 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
     151| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t
     152
     153  #H >(contract_pair var_types nat ?) in E;
     154  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     155  cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     156  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     157
    151158  cases (identifier_eq ? id i)
    152   [ #E' <E' #H % @refl
    153   | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
    154     whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    155     cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    156     #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    157     @(IH m0 n0)
     159  [ 1,3: #E' >E' in EQ2:%; #EQ2 % %
     160    [ 1,3: @refl
     161    | *: destruct (EQ2) change with (add ?????) in H:(?%??);
     162      whd in H; whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]); >lookup_add_hit in H;
     163      whd in ⊢ (% → ?); #E'' >E'' @refl
     164    ]
     165  | *: #NE %2 @(IH m0 n0)
    158166    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
    159167    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
     
    446454  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
    447455  | Evar id ⇒
    448       do c as E ← lookup' vars id;
     456      do 〈c,t〉 as E ← lookup' vars id;
    449457      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
    450458      [ Global r ⇒ λ_.
     
    460468          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    461469          ]
    462       | Local ⇒ λE. OK ? «Id ? id, ?»
     470      | Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
    463471      ] E
    464472  | Ederef e1 ⇒
     
    572580  match ed with
    573581  [ Evar id ⇒
    574       do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
     582      do 〈c,t〉 ← lookup' vars id;
    575583      match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
    576584      [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭
     
    599607].
    600608whd try @I
    601 [ >E @I
     609[ >E whd @refl
    602610| >(E ? (refl ??)) @refl
    603611| 3,4: @pi2
     
    615623
    616624inductive destination (vars:var_types) : Type[0] ≝
    617 | IdDest : ∀id:ident. local_id vars id → destination vars
     625| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    618626| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    619627
     
    629637        match ed1 with
    630638        [ Evar id ⇒
    631             do c as E ← lookup' vars id;
     639            do 〈c,t〉 as E ← lookup' vars id;
    632640            match c return λx.? → ? with
    633             [ Local ⇒ λE. OK ? (IdDest vars id ?)
     641            [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    634642            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
    635643            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
     
    640648        ]
    641649    ].
    642 whd // >E @I
     650whd // >E @refl
    643651qed.
    644652
     
    686694do dest ← translate_dest vars e1 (typeof e2);
    687695match dest with
    688 [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
     696[ IdDest id ty p ⇒
     697    do e2' ← type_should_eq (typeof e2) ty ? e2';
     698    OK ? «St_assign ? id e2', ?»
    689699| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
    690700].
     
    712722record tmpgen : Type[0] ≝ {
    713723  tmp_universe : universe SymbolTag;
    714   tmp_env : list (ident × typ)
     724  tmp_env : list (ident × type)
    715725}.
    716726
    717 definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝
    718 λc,g.
     727definition alloc_tmp : type → tmpgen → ident × tmpgen ≝
     728λty,g.
    719729  let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
    720   〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.
     730  〈tmp, mk_tmpgen u (〈tmp, ty〉::(tmp_env g))〉.
    721731
    722732lemma lookup_label_hit : ∀lbls,l,l'.
     
    728738definition add_tmps : var_types → tmpgen → var_types ≝
    729739λvs,g.
    730   foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g).
     740  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs (tmp_env g).
    731741
    732742definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝
    733743λvars,u1,u2.
    734   ∀id. local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id.
     744  ∀id,ty. local_id (add_tmps vars u1) id ty → local_id (add_tmps vars u2) id ty.
    735745
    736746lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q.
    737747  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
     748cases daemon (* XXX freshness
    738749#tmp #g #g' #vars #q
    739750whd in ⊢ (???% → ?); #E
     
    744755[ >E >lookup_add_hit @I
    745756| cases E #NE >lookup_add_miss [ @H | /2/
    746 ] qed.
     757] *) qed.
    747758
    748759definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
     
    763774qed.
    764775
    765 lemma local_id_add_local_oblivious : ∀vars,id,id'.
    766   local_id vars id → local_id (add ?? vars id' Local) id.
    767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     776(* XXX Not true without fresh id' XXX
     777lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'.
     778  local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty.
     779#vars #id #ty #id' #ty' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    768780cases (identifier_eq ? id id')
    769781[ #E >E >lookup_add_hit @I
    770782| #NE >lookup_add_miss [ @H | /2/
    771783] qed.
    772 
    773 lemma local_id_add_tmps_oblivious : ∀vars,id,u.
    774   local_id vars id → local_id (add_tmps vars u) id.
     784*)
     785
     786(* XXX freshness XXX *)
     787axiom local_id_add_tmps_oblivious : ∀vars,id,ty,u.
     788  local_id vars id ty → local_id (add_tmps vars u) id ty.
     789(*
    775790#vars #id * #u #l #H elim l
    776791[ //
    777792| * #id' #ty #tl @local_id_add_local_oblivious
    778793] qed.
     794*)
    779795
    780796lemma add_tmps_oblivious : ∀vars,lbls,s,u.
     
    784800#s' * #H1 #H2 %
    785801[ @(stmt_vars_mp … H1)
    786   #id @local_id_add_tmps_oblivious
     802  #id #t @local_id_add_tmps_oblivious
    787803| @H2
    788804] qed.
    789805
    790 lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars.
    791   〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    792 #tmp #u #q #u0 #vars
     806lemma local_id_fresh_tmp : ∀tmp,u,ty,u0,vars.
     807  〈tmp,u〉 = alloc_tmp ty u0 → local_id (add_tmps vars u) tmp (typ_of_type ty).
     808#tmp #u #ty #u0 #vars
    793809whd in ⊢ (???% → ?); #E
    794810destruct
    795 whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
    796 @I
     811whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
     812@refl
    797813qed.
    798814
     
    812828        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    813829        match dest with
    814         [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»
     830        [ IdDest id ty p ⇒ OK ? «〈St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?»
    815831        | MemDest r q e1' ⇒
    816             let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in
    817             OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»
     832            let 〈tmp, u〉 as Etmp ≝ alloc_tmp (typeof e1) u in
     833            OK ? «〈St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?»
    818834        ]
    819835    ]
     
    891907try @I
    892908try (#l #H @(match H in False with [ ]))
    893 try (#id #H @H)
     909try (#id #ty #H @H)
    894910[ @add_tmps_oblivious @(pi2 ?? s')
    895911| @local_id_add_tmps_oblivious @p
    896912]
    897 try (@sub_pi2 #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
    898 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
     913try (@sub_pi2 #x @expr_vars_mp #i #ty @local_id_add_tmps_oblivious)
     914[ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @local_id_add_tmps_oblivious
    899915| 2,4: @(local_id_fresh_tmp … Etmp)
    900916| @(alloc_tmp_preserves … Etmp)
     
    907923    %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
    908924  ]
    909 | 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L
     925| 10,14: cases H2 #_ #TP2 #id #ty #L @TP2 cases H1 #_ #TP1 @TP1 @L
    910926| 15,18: @(π1 (π1 H1))
    911927| 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
     
    913929| 17,20: @(π2 H1)
    914930(* Sfor *)
    915 | @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ]
     931| @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @(π2 H2) @H | @H5 ]
    916932| @(π1 (π1 H3))
    917 | @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ]
     933| @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @H | @H5 ]
    918934| #l #H cases (Exists_append … H)
    919935  [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
     
    926942    ]
    927943  ]
    928 | #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
     944| #id #ty #H @(π2 H3) @(π2 H2) @(π2 H1) @H
    929945(* Slabel *)
    930946| %{l} @E
     
    948964  let 〈id,ty〉 ≝ it in
    949965   do «s,u, Is» ← su;
    950   do t as E ← lookup' vars id;
     966  do 〈t,ty'〉 as E ← lookup' vars id;
    951967  match t return λx.? → ? with
    952968  [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
     
    957973      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    958974      ];
    959       OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?»
     975      OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s, u〉, ?»
    960976  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    961977  ] E) (OK ? s) params.
    962978try @conj try @conj try @conj try @conj try @conj try @conj
    963979try @I
    964 [ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I
     980[ @(expr_vars_mp … (λid,ty. local_id_add_tmps_oblivious vars id ty u)) whd >E @refl
    965981| @(π1 (π1 Is))
    966982| @(π2 (π1 Is))
     
    10301046qed.
    10311047
    1032 lemma local_id_split : ∀vars,tmpgen,i.
    1033   local_id (add_tmps vars tmpgen) i
    1034   local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
    1035 #vars #tmpgen #i
    1036 whd in ⊢ (?%? → ?);
     1048lemma local_id_split : ∀vars,tmpgen,i,t.
     1049  local_id (add_tmps vars tmpgen) i t
     1050  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env tmpgen).
     1051#vars #tmpgen #i #t
     1052whd in ⊢ (?%?? → ?);
    10371053elim (tmp_env tmpgen)
    10381054[ #H %1 @H
    10391055| * #id #ty #tl #IH
    10401056  cases (identifier_eq ? i id)
    1041   [ #E >E #H %2 whd %1 @refl
     1057  [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ]
    10421058  | #NE #H cases (IH ?)
    10431059    [ #H' %1 @H'
     
    10571073] qed.
    10581074
    1059 definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
     1075definition translate_function : universe SymbolTag → list (ident×region×type) → function → res internal_function ≝
    10601076λtmpuniverse, globals, f.
    10611077  do «lbls, Ilbls» ← build_label_env (fn_body f);
     
    10671083    (opttyp_of_type (fn_return f))
    10681084    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    1069     ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
     1085    ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env tmp @ fn_vars f)))
    10701086    stacksize
    10711087    s ?).
     
    10741090#s1 * #H1 #H2 %
    10751091[ @(stmt_vars_mp … H1)
    1076   #i #H
     1092  #i #t #H
    10771093  cases (local_id_split … H)
    1078   [ #H' @Exists_squeeze >map_append
    1079     @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H'
     1094  [ #H' >map_append
     1095    @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H'
    10801096                | skip
    1081                 | * #id #ty #E1 <E1 @refl
     1097                | * #id #ty * #E1 #E2 <E1 <E2 @refl
    10821098                ]
    1083   | #EX @Exists_append_r @Exists_append_l @EX
     1099  | #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
    10841100  ]
    10851101| @(stmt_labels_mp … H2)
     
    10901106] qed.
    10911107
    1092 definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
     1108definition translate_fundef : universe SymbolTag → list (ident×region×type) → clight_fundef → res (fundef internal_function) ≝
    10931109λtmpuniverse,globals,f.
    10941110match f with
     
    11051121λp.
    11061122  let tmpuniverse ≝ universe_for_program p in
    1107   let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    1108   let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
     1123  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
     1124  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
    11091125  let globals ≝ fun_globals @ var_globals in
    11101126  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
  • src/Cminor/initialisation.ma

    r1610 r1626  
    2121(* None of the additional code introduces locals or labels. *)
    2222definition stmt_inv : stmt → Prop ≝
    23   stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     23  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s).
    2424 
    2525discriminator option.
     
    9797[ % [ % // |
    9898  @(stmt_P_mp … H) #s * #V #L %
    99   [ @(stmt_vars_mp … V) #i *
     99  [ @(stmt_vars_mp … V) #i #t *
    100100  | @(stmt_labels_mp … L) #l *
    101101  ]
  • src/Cminor/semantics.ma

    r1605 r1626  
    1212
    1313definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
    14   stmt_P (λs.stmt_vars (present ?? en) s ∧
     14  stmt_P (λs.stmt_vars (λid,ty. present ?? en id) s ∧
    1515             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.
    1616
     
    2323#s * #H1 #H2 %
    2424[ @(stmt_vars_mp … H1)
    25   #l #H @update_still_present @H
     25  #l #ty #H @update_still_present @H
    2626| @H2
    2727] qed.
     
    5353inductive stack : Type[0] ≝
    5454| SStop : stack
    55 | Scall : ∀dest:option ident. ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some id ⇒ present ?? en id] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
     55| Scall : ∀dest:option (ident×typ). ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty)] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
    5656
    5757inductive state : Type[0] ≝
     
    9292axiom FailedLoad : String.
    9393
    94 let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (present ?? en)) (sp:block) (m:mem) on e : res (trace × val) ≝
    95 match e return λt,e.expr_vars t e (present ?? en) → res (trace × val) with
     94let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝
     95match e return λt,e.expr_vars t e (λid,ty. present ?? en id) → res (trace × val) with
    9696[ Id _ i ⇒ λEnv.
    9797    let r ≝ lookup_present ?? en i ? in
     
    383383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
    384384                   [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
    385                    | Some id ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en id dstP v) ? ? m sp k ? st'〉
     385                   | Some idty ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
    386386                   ] dstP
    387387        ]
     
    414414  @(stmt_P_mp … (f_inv f))
    415415  #s * #V #L %
    416   [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
     416  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
    417417    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
    418       * #id' #ty * #E1 #H <E1 @H
     418      * #id' #ty * #E1 destruct #H @H
    419419    | *: #H cases (Exists_All … H (init_locals_env … en …))
    420       * #id' #ty * #E1 #H <E1 @H
     420      * #id' #ty * #E1 destruct #H @H
    421421    ]
    422422  | 2,4: @L
  • src/Cminor/syntax.ma

    r1605 r1626  
    1616
    1717(* Assert a predicate on every variable or parameter identifier. *)
    18 let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
     18let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
    1919match e with
    20 [ Id _ i ⇒ P i
     20[ Id t i ⇒ P i t
    2121| Cst _ _ ⇒ True
    2222| Op1 _ _ _ e ⇒ expr_vars ? e P
     
    2828
    2929lemma expr_vars_mp : ∀t,e,P,Q.
    30   (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
     30  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
    3131#t0 #e elim e normalize /3/
    3232[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     
    4242| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
    4343(* ident for returned value, expression to identify fn, args. *)
    44 | St_call : option ident → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     44| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4545| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4646| St_seq : stmt → stmt → stmt
     
    7676
    7777(* Assert a predicate on every variable or parameter identifier. *)
    78 definition stmt_vars : (ident → Prop) → stmt → Prop ≝
     78definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
    7979λP,s.
    8080match s with
    81 [ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     81[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
    8282| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    83 | St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     83| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8484| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8585| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
     
    107107] qed.
    108108
    109 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
     109lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
    110110#P #Q #H #s elim s normalize
    111111[ //
     
    146146; f_stacksize : nat
    147147; f_body      : stmt
    148 ; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
     148     (* Ensure that variables appear in the params and vars list with the
     149        correct typ; and that all goto labels used are declared. *)
     150; f_inv       : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧
    149151                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
    150152}.
  • src/Cminor/toRTLabs.ma

    r1611 r1626  
    1 include "basics/lists/list.ma".
     1include "utilities/lists.ma".
    22include "common/Globalenvs.ma".
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
    55
    6 definition env ≝ identifier_map SymbolTag register.
     6definition env ≝ identifier_map SymbolTag (register × typ).
    77definition label_env ≝ identifier_map Label label.
    88definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
     
    1212   let 〈rs,en,gen〉 ≝ rsengen in
    1313   let 〈r,gen'〉 ≝ fresh … gen in
    14      〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
    15 
     14     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
     15(*
    1616lemma populates_env : ∀l,e,u,l',e',u'.
    1717  populate_env e u l = 〈l',e',u'〉 →
     
    4949  #i #H @lookup_add_oblivious @(IH … E0) @H
    5050] qed.
    51 
     51*)
    5252definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
    5353λen,gen. foldr ??
     
    9292] qed.
    9393
    94 definition lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
     94definition Env_has : env → ident → typ → Prop ≝
     95λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
     96
     97lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
     98#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
     99[ * | * #r #t' #E % #E' destruct ]
     100qed.
     101
     102definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
     103/2/ qed.
    95104definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
    96105
     
    107116
    108117definition partially_closed : label_env → graph statement → Prop ≝
    109  λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.
     118 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
    110119
    111120(* I'd use a single parametrised definition along with internal_function, but
    112121   it's a pain without implicit parameters. *)
    113 record partial_fn (lenv:label_env) : Type[0] ≝
     122record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
    114123{ pf_labgen    : universe LabelTag
    115124; pf_reggen    : universe RegisterTag
    116 ; pf_result    : option (register × typ)
    117125; pf_params    : list (register × typ)
    118126; pf_locals    : list (register × typ)
     127; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
     128; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
    119129; pf_stacksize : nat
    120130; pf_graph     : graph statement
    121131; pf_closed    : partially_closed lenv pf_graph
     132; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
    122133; pf_entry     : Σl:label. present ?? pf_graph l
    123134; pf_exit      : Σl:label. present ?? pf_graph l
    124135}.
    125136
    126 inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
    127 | fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.
    128 
    129 lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
    130   fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
    131 #le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.
    132 
    133 lemma fn_graph_included_refl : ∀label_env,f.
    134   fn_graph_included label_env f f.
    135 #le #f % #l #H @H qed.
    136 
    137 lemma fn_graph_included_sig : ∀label_env,f,f0.
    138   ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
    139   fn_graph_included label_env f f0 →
    140   fn_graph_included label_env f f'.
    141 #le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
    142 qed.
    143 
    144 lemma add_statement_inv : ∀le,l,s.∀f.
    145   labels_present (pf_graph le f) s →
    146   partially_closed le (add … (pf_graph ? f) l s).
    147 #le #l #s #f #p
     137definition fn_env_has ≝
     138  λle,env,f. env_has (pf_locals le env f @ pf_params le env f).
     139
     140record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
     141{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
     142; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
     143}.
     144
     145lemma fn_con_trans : ∀le,env,f1,f2,f3.
     146  fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
     147#le #env #f1 #f2 #f3 #H1 #H2 %
     148[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
     149| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
     150] qed.
     151
     152lemma fn_con_refl : ∀label_env,env,f.
     153  fn_contains label_env env f f.
     154#le #env #f % #l // qed.
     155
     156lemma fn_con_sig : ∀label_env,env,f,f0.
     157  ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.
     158  fn_contains label_env env f f0 →
     159  fn_contains label_env env f f'.
     160#le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
     161qed.
     162
     163lemma add_statement_inv : ∀le,env,l,s.∀f.
     164  labels_present (pf_graph le env f) s →
     165  partially_closed le (add … (pf_graph … f) l s).
     166#le #env #l #s #f #p
    148167#l' #s' #H cases (identifier_eq … l l')
    149168[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    150169  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
    151 | #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     170| #NE @(labels_P_mp … (pf_closed f l' s' ?))
    152171  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    153172  | >lookup_add_miss in H; /2/
     
    155174] qed.
    156175
     176definition statement_typed_in ≝
     177λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s.
     178
     179lemma forall_nodes_add : ∀A,P,l,a,g.
     180  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
     181#A #P #l #a #g #ALL #NEW
     182#l' #a'
     183cases (identifier_eq … l' l)
     184[ #E destruct >lookup_add_hit #E destruct @NEW
     185| #ne >lookup_add_miss /2/
     186] qed.
     187
    157188(* Add a statement to the graph, *without* updating the entry label. *)
    158 definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
    159 λle,l,s,f,p.
    160   mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
    161                 (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    162                 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
    163                 «pf_entry ? f, ?» «pf_exit ? f, ?».
     189definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
     190  labels_present (pf_graph … f) s →
     191  statement_typed_in le env f s →
     192  Σf':partial_fn le env. fn_contains … f f' ≝
     193λle,env,l,s,f,p,tp.
     194  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
     195                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     196                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
     197                «pf_entry … f, ?» «pf_exit … f, ?».
    164198[ @add_statement_inv @p
    165 | 2,3: @lookup_add_oblivious [ @(pi2 … (pf_entry le f)) | @(pi2 … (pf_exit le f)) ]
    166 | % #l' @lookup_add_oblivious
     199| @forall_nodes_add //
     200| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
     201| % [ #l' @lookup_add_oblivious | // ]
    167202] qed.
    168203
    169204(* Add a statement to the graph, making it the entry label. *)
    170 definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
    171 λle,l,s,f,p.
    172   mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
    173                 (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    174                 (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
    175                 «l, ?» «pf_exit ? f, ?».
     205definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
     206  labels_present (pf_graph … f) s →
     207  statement_typed_in … f s →
     208  Σf':partial_fn le env. fn_contains … f f' ≝
     209λle,env,l,s,f,p,tl.
     210  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
     211                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     212                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
     213                «l, ?» «pf_exit … f, ?».
    176214[ @add_statement_inv @p
     215| @forall_nodes_add //
    177216| whd >lookup_add_hit % #E destruct
    178 | @lookup_add_oblivious @(pi2 … (pf_exit le f))
    179 | % #l' @lookup_add_oblivious
     217| @lookup_add_oblivious @(pi2 … (pf_exit f))
     218| % [ #l' @lookup_add_oblivious | // ]
    180219] qed.
    181220
    182221(* Add a statement with a fresh label to the start of the function.  The
    183222   statement is parametrised by the *next* instruction's label. *)
    184 definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
    185 λle,s,f,p.
    186   let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
    187   let s' ≝ s (pf_entry ? f) in
    188     (mk_partial_fn le g (pf_reggen ? f)
    189                    (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    190                    (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
    191                    «l, ?» «pf_exit ? f, ?»).
    192 [ % #l' @lookup_add_oblivious
     223definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
     224  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
     225  (∀l. statement_typed_in … f (s l)) →
     226  Σf':partial_fn le env. fn_contains … f f' ≝
     227λle,env,s,f,p,tp.
     228  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
     229  let s' ≝ s (pf_entry … f) in
     230    (mk_partial_fn le env g (pf_reggen … f)
     231                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     232                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
     233                   «l, ?» «pf_exit … f, ?»).
     234[ % [ #l' @lookup_add_oblivious | // ]
    193235| @add_statement_inv @p @(pi2 … (pf_entry …))
     236| @forall_nodes_add //
    194237| whd >lookup_add_hit % #E destruct
    195238| @lookup_add_oblivious @(pi2 … (pf_exit …))
     
    198241(* Variants for labels which are (goto) labels *)
    199242
    200 lemma add_statement_inv' : ∀le,l,s.∀f.
    201   labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
    202   partially_closed le (add … (pf_graph ? f) l s).
    203 #le #l #s #f #p
     243lemma add_statement_inv' : ∀le,env,l,s.∀f.
     244  labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
     245  partially_closed le (add … (pf_graph f) l s).
     246#le #env #l #s #f #p
    204247#l' #s' #H cases (identifier_eq … l l')
    205248[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    206249  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    207 | #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
     250| #NE @(labels_P_mp … (pf_closed f l' s' ?))
    208251  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    209252  | >lookup_add_miss in H; /2/
     
    211254] qed.
    212255
    213 definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
    214 λle,s,f,p.
    215   let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
    216   let s' ≝ s (pf_entry ? f) in
    217     (mk_partial_fn le g (pf_reggen ? f)
    218                    (pf_result ? f) (pf_params ? f) (pf_locals ? f)
    219                    (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
    220                    «l, ?» «pf_exit ? f, ?»).
    221 [ % #l' @lookup_add_oblivious
     256definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
     257  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
     258  (∀l. statement_typed_in … f (s l)) →
     259  Σf':partial_fn le env. fn_contains … f f' ≝
     260λle,env,s,f,p,tp.
     261  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
     262  let s' ≝ s (pf_entry … f) in
     263    (mk_partial_fn le env g (pf_reggen … f)
     264                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
     265                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
     266                   «l, ?» «pf_exit … f, ?»).
     267[ % [ #l' @lookup_add_oblivious | // ]
    222268| @add_statement_inv' @p @(pi2 … (pf_entry …))
     269| @forall_nodes_add //
    223270| whd >lookup_add_hit % #E destruct
    224271| @lookup_add_oblivious @(pi2 … (pf_exit …))
    225272] qed.
    226273
    227 definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
    228 λle,f,ty.
    229   let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
    230     〈r, «mk_partial_fn le (pf_labgen ? f) g
    231                        (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
    232                        (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
    233 % #l // qed.
     274lemma extend_typ_env : ∀te,r,t,r',t'.
     275  env_has te r t → env_has (〈r',t'〉::te) r t.
     276#tw #r #t #r' #t' #H %2 @H
     277qed.
     278
     279lemma stmt_extend_typ_env : ∀te,r,t,s.
     280  statement_typed te s → statement_typed (〈r,t〉::te) s.
     281#tw #r #t *
     282[ 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     283| *: //
     284] qed.
     285
     286(* A little more nesting in the result type than I'd like, but it keeps the
     287   function closely paired with the proof that it contains f. *)
     288definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
     289  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
     290λle,env,f,ty.
     291  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
     292  let f' ≝
     293    «mk_partial_fn le env
     294       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
     295       (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
     296       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
     297  in
     298    ❬f' , ?(*«r, ?»*)❭.
     299[ @(«r, ?») % @refl
     300| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
     301| #i #t #r1 #H #L %2 @(pf_envok … f … L)
     302| %2 @(pi2 … rt)
     303| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
     304] qed.
    234305
    235306axiom UnknownVariable : String.
    236307
    237 definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     308definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
     309  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
    238310λle,env,ty,e,f.
    239   match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
    240   [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉
    241   | _ ⇒ λ_.fresh_reg le f ty
     311  match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) with
     312  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
     313  | _ ⇒ λ_.fresh_reg le env f ?
    242314  ].
    243 % // qed.
     315[ % //
     316| @(pf_envok … Env) @refl
     317] qed.
    244318 
    245319let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ 
    246320 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
    247 
    248 definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (present ?? env) ].
     321 
     322let rec foldr_all' (A:Type[0]) (P:A → Prop) (B:list A → Type[0]) (f:∀a:A. P a → ∀l. B l → B (a::l)) (b:B [ ]) (l:list A) (H:All ? P l) on l :B l ≝ 
     323 match l return λx.All ? P x → B x with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) l (foldr_all' A P B f b l (proj2 … H))] H.
     324
     325definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
     326
     327definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
     328λA,P,x. match x with [ mk_DPair a _ ⇒ a].
    249329
    250330definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
    251                          ∀f:partial_fn le. All ? (exprtyp_present env) es →
    252                          list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
     331                         ∀f:partial_fn le env. All ? (exprtyp_present env) es →
     332                         𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es) ≝
    253333λle,env,es,f,Env.
    254   foldr_all (𝚺t:typ.expr t) ??
    255     (λe,p,acc. let 〈rs,f〉 ≝ acc in
    256              let 〈r,f'〉 ≝ match e return λe.? → ? with [ mk_DPair t e ⇒ λp.choose_reg le env t e (pi1 ?? f) ? ] p in
    257              〈r::rs,«pi1 ?? f', ?»〉) 〈[ ], «f, ?»〉 es Env.
     334  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es))
     335    (λe,p,tl,acc.
     336      match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
     337        match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
     338          match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
     339            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
     340          ]
     341        ] p
     342      ]) ❬«f, ?», «[ ], I»❭ es Env.
    258343[ @p
    259 | @fn_graph_inc_trans [ 3: @(pi2 ?? f') | skip | @(pi2 ?? f) ]
    260 | % //
     344| cases r #r' #Hr' cases rs #rs' #Hrs'
     345  % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
     346| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
     347| @fn_con_refl
    261348]  qed.
    262349
     
    267354
    268355
    269 lemma choose_regs_length : ∀le,env,es,f,p,rs,f'.
    270   choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
    271 #le #env #es #f elim es
    272 [ #p #rs #f normalize #E destruct @refl
    273 | * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?); #E
    274   cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
    275   cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
    276   destruct (E4) skip (E1 E3) @eq_f @IH
    277   [ @(proj2 … p)
    278   | 3: @sym_eq @E1
    279   | 2: skip
    280   ]
    281 ] qed.
    282 
    283 lemma present_included : ∀le,f,f',l.
    284   fn_graph_included le f f' →
    285   present ?? (pf_graph le f) l →
    286   present ?? (pf_graph le f') l.
    287 #le #f #f' #l * #H1 #H2 @H1 @H2 qed.
     356lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
     357  choose_regs le env es f p = ❬f',rs❭ → |es| = |rs|.
     358#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
     359qed.
     360
     361lemma present_included : ∀le,env,f,f',l.
     362  fn_contains le env f f' →
     363  present ?? (pf_graph … f) l →
     364  present ?? (pf_graph … f') l.
     365#le #env #f #f' #l * #H1 #H2 @H1 qed.
    288366
    289367(* Some definitions for the add_stmt function later, which we introduce now so
     
    292370(* We need to show that the graph only grows, and that Cminor labels will end
    293371   up in the graph. *)
    294 definition Cminor_labels_added ≝ λle,s,f'.
     372definition Cminor_labels_added ≝ λle,env,s,f'.
    295373∀l. Exists ? (λl'.l=l') (labels_of s) →
    296 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
    297 
    298 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
    299 { stmt_graph_inc : fn_graph_included ? f f'
    300 ; stmt_labels_added : Cminor_labels_added le s f'
     374∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.
     375
     376record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝
     377{ stmt_graph_con : fn_contains … f f'
     378; stmt_labels_added : Cminor_labels_added s f'
    301379}.
    302380
    303 (* Build some machinery to solve fn_graph_included goals. *)
     381(* Build some machinery to solve fn_contains goals. *)
    304382
    305383(* A datatype saying how we intend to prove a step. *)
    306 inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
    307 | fn_inc_eq : ∀f. fn_inc_because le f
    308 | fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
    309     ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
    310 | fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
    311     ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
     384inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
     385| fn_con_eq : ∀f. fn_con_because le env f
     386| fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
     387    ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
     388| fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
     389    ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
    312390.
    313391
    314392(* Extract the starting function for a step. *)
    315 let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le
    316   match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_addinv f _ _ _ _ ⇒ f ].
     393let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env
     394  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
    317395
    318396(* Some unification hints to pick the right step to apply.  The dummy variable
     
    321399   have reached the desired starting point. *)
    322400
    323 unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True;
     401unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
    324402  f' ≟ f,
    325   b  ≟ fn_inc_eq le f
     403  b  ≟ fn_con_eq le env f
    326404
    327   fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
     405  fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
    328406.
    329407
    330 unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, f3:(Σf3:partial_fn le. fn_graph_included le f2 f3);
    331   b ≟ fn_inc_sig le f1 f2 H12 f3
     408unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, f3:(Σf3:partial_fn le env. fn_contains le env f2 f3);
     409  b ≟ fn_con_sig le env f1 f2 H12 f3
    332410
    333   fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
     411  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
    334412.
    335413
    336 unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, s:stmt, f3:(Σf3:partial_fn le. add_stmt_inv le s f2 f3);
    337   b ≟ fn_inc_addinv le f1 f2 H12 s f3
     414unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le env s f2 f3);
     415  b ≟ fn_con_addinv le env f1 f2 H12 s f3
    338416
    339   fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
     417  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
    340418.
    341419
    342420(* A lemma to perform a step of the proof.  We can repeat this to do the whole
    343421   proof. *) 
    344 lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
    345 #le #f *
    346 [ #f @fn_graph_included_refl
    347 | #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
    348 | #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23)
    349 ] qed.
    350 
     422lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
     423#le #env #f *
     424[ #f @fn_con_refl
     425| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
     426| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
     427] qed.
     428
     429notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
     430  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
    351431
    352432axiom BadCminorProgram : String.
    353433
    354 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝
    355 match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
    356 [ Id t i ⇒ λEnv.
    357     let r ≝ lookup_reg env i Env in
     434let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
     435  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
     436  (dst:Σdst. fn_env_has … f dst ty)
     437  on e: Σf':partial_fn le env. fn_contains … f f' ≝
     438match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with
     439[ Id t i ⇒ λEnv,dst.
     440    let r ≝ lookup_reg env i t Env in
    358441    match register_eq r dst with
    359442    [ inl _ ⇒ «f, ?»
    360     | inr _ ⇒ «pi1 … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
     443    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
    361444    ]
    362 | Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
    363 | Op1 t t' op e' ⇒ λEnv.
    364     let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    365     let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
    366     let f ≝ add_expr ? env ? e' Env r f in
     445| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const dst c) f ??, ?»
     446| Op1 t t' op e' ⇒ λEnv,dst.
     447    let ❬f,r❭ ≝ choose_reg … e' f Env in
     448    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
     449    let f ≝ add_expr … env ? e' Env f «r, ?» in
    367450      «pi1 … f, ?»
    368 | Op2 _ _ _ op e1 e2 ⇒ λEnv.
    369     let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
    370     let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
    371     let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
    372     let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
    373     let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
     451| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
     452    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
     453    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
     454    let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in
     455    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
     456    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
    374457      «pi1 … f, ?»
    375 | Mem _ _ q e' ⇒ λEnv.
    376     let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    377     let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
    378     let f ≝ add_expr ? env ? e' Env r f in
     458| Mem _ _ q e' ⇒ λEnv,dst.
     459    let ❬f,r❭ ≝ choose_reg … e' f Env in
     460    let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in
     461    let f ≝ add_expr … env ? e' Env f «r,?» in
    379462      «pi1 … f, ?»
    380 | Cond _ _ _ e' e1 e2 ⇒ λEnv.
    381     let resume_at ≝ pf_entry ? f in
    382     let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
    383     let lfalse ≝ pf_entry ? f in
    384     let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
    385     let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
    386     let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
    387     let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
    388     let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
     463| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
     464    let resume_at ≝ pf_entry f in
     465    let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
     466    let lfalse ≝ pf_entry f in
     467    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
     468    let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
     469    let ❬f,r❭ ≝ choose_reg … e' f ? in
     470    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
     471    let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
    389472      «pi1 … f, ?»
    390 | Ecost _ l e' ⇒ λEnv.
    391     let f ≝ add_expr ? env ? e' Env dst f in
    392     let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
     473| Ecost _ l e' ⇒ λEnv,dst.
     474    let f ≝ add_expr … env ? e' Env f dst in
     475    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
    393476      «f, ?»
    394 ] Env.
     477] Env dst.
    395478(* For new labels, we need to step back through the definitions of f until we
    396479   hit the point that it was added. *)
    397 try (repeat @fn_includes_step @I)
     480try (repeat @fn_contains_step @I)
    398481try (#l #H @H)
    399 [ #l #H whd % [ @H | @(present_included … (pi2 … lfalse)) repeat @fn_includes_step @I ]
    400 | #l #H @(present_included … (pi2 ?? resume_at)) repeat @fn_includes_step @I
     482try (#l @I)
     483[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
     484| 2,6,7: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     485| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
     486| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
     487| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
     488| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
     489| @(π1 (π1 Env))
     490| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
     491| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
    401492] qed.
    402493
    403494let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    404                   (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
    405 match es return λes.All ?? es → |es|=|dsts| → ? with
    406 [ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
     495                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le env)
     496                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
     497match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
     498[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
    407499| cons e et ⇒ λEnv.
    408     match dsts return λx. ?=|x| → ? with
    409     [ nil ⇒ λpf.⊥
    410     | cons r rt ⇒ λpf.
    411         let f ≝ add_exprs ? env et ? rt ? f in
    412         match e return λe.exprtyp_present ? e → ? with [ mk_DPair ty e ⇒ λEnv.
    413           let f ≝ add_expr ? env ty e ? r f in
    414             «pi1 … f, ?» ] (proj1 ?? Env)
     500    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
     501    [ nil ⇒ λ_.λpf.⊥
     502    | cons r rt ⇒ λHdsts,pf.
     503        let f' ≝ add_exprs ? env et ? rt ? f ? in
     504        match e return λe.exprtyp_present ? e → fn_env_has le env f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
     505          let f'' ≝ add_expr ? env ty e ? f' r in
     506            «pi1 … f'', ?»
     507        ] (proj1 ?? Env) (π1 Hdsts)
    415508    ]
    416 ] Env pf.
    417 try (repeat @fn_includes_step @I)
     509] Env Hdsts pf.
     510try (repeat @fn_contains_step @I)
    418511[ 1,2: normalize in pf; destruct
    419512| @Env
     513| @(fn_con_env … Hr) repeat @fn_contains_step @I
    420514| @(proj2 … Env)
    421515| normalize in pf; destruct @e0
     516| @(π2 Hdsts)
    422517] qed.
    423518
     
    426521
    427522definition stmt_inv : env → label_env → stmt → Prop ≝
    428 λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
     523λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
    429524
    430525(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
     
    468563qed.
    469564
    470 lemma empty_Cminor_labels_added : ∀le,s,f'.
    471   labels_of s = [ ] → Cminor_labels_added le s f'.
    472 #le #s #f' #E whd >E #l *;
    473 qed.
    474 
    475 lemma equal_Cminor_labels_added : ∀le,s,s',f.
    476   labels_of s = labels_of s' → Cminor_labels_added le s' f →
    477   Cminor_labels_added le s f.
    478 #le #s #s' #f #E whd in ⊢ (% → %); > E #H @H
    479 qed.
    480 
    481 lemma Cminor_labels_inc : ∀le,s,f,f'.
    482   fn_graph_included le f f' →
    483   Cminor_labels_added le s f →
    484   Cminor_labels_added le s f'.
    485 #le #s #f #f' #INC #ADDED
     565lemma empty_Cminor_labels_added : ∀le,env,s,f'.
     566  labels_of s = [ ] → Cminor_labels_added le env s f'.
     567#le #env #s #f' #E whd >E #l *;
     568qed.
     569
     570lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
     571  labels_of s = labels_of s' → Cminor_labels_added s' f →
     572  Cminor_labels_added le env s f.
     573#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
     574qed.
     575
     576lemma Cminor_labels_con : ∀le,env,s,f,f'.
     577  fn_contains le env f f' →
     578  Cminor_labels_added s f →
     579  Cminor_labels_added s f'.
     580#le #env #s #f #f' #INC #ADDED
    486581#l #E cases (ADDED l E) #l' * #L #P
    487582%{l'} % [ @L | @(present_included … P) @INC ]
    488583qed.
    489584
    490 lemma Cminor_labels_inv : ∀le,s,s',f.
    491   ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
    492   Cminor_labels_added le s f →
    493   Cminor_labels_added le s f'.
    494 #le #s #s' #f * #f' * #H1 #H2 #H3
     585lemma Cminor_labels_inv : ∀le,env,s,s',f.
     586  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
     587  Cminor_labels_added le env s f →
     588  Cminor_labels_added le env s f'.
     589#le #env #s #s' #f * #f' * #H1 #H2 #H3
    495590#l #E cases (H3 l E) #l' * #L #P
    496591%{l'} % [ @L | @(present_included … P) @H1 ]
    497592qed.
    498593
    499 lemma Cminor_labels_sig : ∀le,s,f.
    500   ∀f':Σf':partial_fn le. fn_graph_included le f f'.
    501   Cminor_labels_added le s f →
    502   Cminor_labels_added le s f'.
    503 #le #s #f * #f' #H1 #H2
     594lemma Cminor_labels_sig : ∀le,env,s,f.
     595  ∀f':Σf':partial_fn le env. fn_contains … f f'.
     596  Cminor_labels_added s f →
     597  Cminor_labels_added s f'.
     598#le #env #s #f * #f' #H1 #H2
    504599#l #E cases (H2 l E) #l' * #L #P
    505600%{l'} % [ @L | @(present_included … P) @H1 ]
    506601qed.
    507602
    508 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
    509 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
     603let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
     604match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
    510605[ St_skip ⇒ λ_. OK ? «f, ?»
    511 | St_assign _ x e ⇒ λEnv.
    512     let dst ≝ lookup_reg env x (π1 (π1 Env)) in
    513     OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
     606| St_assign t x e ⇒ λEnv.
     607    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
     608    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
    514609| St_store _ _ q e1 e2 ⇒ λEnv.
    515     let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
    516     let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
    517     let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
    518     let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
    519     OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
     610    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
     611    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
     612    let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
     613    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
     614    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
    520615| St_call return_opt_id e args ⇒ λEnv.
    521616    let return_opt_reg ≝
    522617      match return_opt_id return λo. ? → ? with
    523618      [ None ⇒ λ_. None ?
    524       | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
     619      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
    525620      ] Env in
    526     let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     621    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
    527622    let f ≝
    528623      match expr_is_Id ? e with
    529       [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
     624      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
    530625      | None ⇒
    531         let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
    532         let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
    533         «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
     626        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
     627        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
     628        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
    534629      ] in
    535     OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     630    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
    536631| St_tailcall e args ⇒ λEnv.
    537     let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     632    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
    538633    let f ≝
    539634      match expr_is_Id ? e with
    540       [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
     635      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
    541636      | None ⇒
    542         let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
    543         let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
    544         «pi1 … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
     637        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
     638        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
     639        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
    545640      ] in
    546     OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     641    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
    547642| St_seq s1 s2 ⇒ λEnv.
    548643    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
     
    550645      OK ? «pi1 … f1, ?»
    551646| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    552     let l_next ≝ pf_entry ? f in
     647    let l_next ≝ pf_entry f in
    553648    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
    554     let l2 ≝ pf_entry ? f2 in
    555     let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
     649    let l2 ≝ pf_entry f2 in
     650    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
    556651    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
    557     let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
    558     let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
    559     OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
     652    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
     653    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
     654    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
    560655| St_loop s ⇒ λEnv.
    561     let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
    562     let l_loop ≝ pf_entry ? f in
     656    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
     657    let l_loop ≝ pf_entry f in
    563658    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
    564     OK ? «pi1 … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
     659    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
    565660| St_block s ⇒ λEnv.
    566     do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
     661    do f ← add_stmt env label_env s (π2 Env) f («pf_entry f::exits, ?»);
    567662    OK ? «pi1 … f, ?»
    568663| St_exit n ⇒ λEnv.
    569664    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
    570     OK ? «pi1 … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
     665    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
    571666| St_switch sz sg e tab n ⇒ λEnv.
    572     let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
     667    let ❬f,r❭ ≝ choose_reg … e f ? in
    573668    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
    574     let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
    575     do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
     669    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
     670    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
    576671      do f ← f;
    577672      let 〈i,n〉 ≝ cs in
    578       let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
    579       let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
     673      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
     674      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
    580675      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    581       let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
    582       let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
    583       let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
     676      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
     677      let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
     678      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
    584679        OK ? «pi1 … f, ?») (OK ? f) tab;
    585     OK ? «pi1 … (add_expr ? env ? e (π1 Env) r f), ?»
     680    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
    586681| St_return opt_e ⇒ let f0 ≝ f in
    587     let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
    588     match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with
     682    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
     683    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with
    589684    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
    590685    | Some e ⇒
    591         match pf_result ? f with
     686        match pf_result f with
    592687        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
    593688        | Some r ⇒
    594             match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
    595             [ mk_DPair ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
    596                               OK ? «pi1 … f, ?» ]
     689            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with
     690            [ mk_DPair ty e ⇒ λEnv.
     691                match typ_eq (\snd r) ty with
     692                [ inl E ⇒ let f ≝ add_expr label_env env ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
     693                          OK ? «pi1 … f, ?»
     694                | inr _ ⇒ Error ? (msg ReturnMismatch)
     695                ]
     696            ]
    597697        ]
    598698    ]
     
    600700    do f ← add_stmt env label_env s' (π2 Env) f exits;
    601701    let l' ≝ lookup_label label_env l ? in
    602     OK ? «pi1 … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
     702    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
    603703| St_goto l ⇒ λEnv.
    604704    let l' ≝ lookup_label label_env l ? in
    605     OK ? «pi1 … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
     705    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
    606706| St_cost l s' ⇒ λEnv.
    607707    do f ← add_stmt env label_env s' (π2 Env) f exits;
    608     OK ? «pi1 … (add_fresh_to_graph ? (St_cost l) f ?), ?»
     708    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
    609709] Env.
    610710try @(π1 Env)
     
    613713try @(π2 (π1 Env))
    614714try @mk_add_stmt_inv
    615 try (repeat @fn_includes_step @I)
     715try (repeat @fn_contains_step @I)
    616716try (@empty_Cminor_labels_added @refl)
    617 try (@(All_mp … (pi2 ?? exits)))
    618717try (#l #H @I)
    619718try (#l #H @H)
    620 [ -f @(choose_regs_length … (sym_eq … Eregs))
    621 | whd in Env; @(π1 (π1 (π1 Env)))
    622 | -f @(choose_regs_length … (sym_eq … Eregs))
     719try (#l @I)
     720[ @(pf_envok … (π1 (π1 Env))) @refl
     721| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
     722| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
     723| 4,8: @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
     724| 5,9: @sym_eq @(All2_length … (pi2 ?? args_regs))
     725| 6,10: @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
     726| @(π1 (π1 (π1 Env)))
     727| 11,13,14,19,20: (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
    623728| #l #H cases (Exists_append … H)
    624   [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
    625   | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (pi2 ?? f2)) ]
    626   ]
    627 | #l #H @(present_included … H) repeat @fn_includes_step @I
    628 | #l #H @(present_included … (pi2 ?? l_next)) repeat @fn_includes_step @I
     729  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
     730  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
     731  ]
     732| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    629733| #l #H cases (Exists_append … H)
    630   [ @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f1))) repeat @fn_includes_step @I
    631   | @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f2))) repeat @fn_includes_step @I
    632   ]
    633 | #l #H % [ @H | @(present_included … (pi2 ?? l2)) repeat @fn_includes_step @I ]
    634 | 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
    635 | @(pi2 ?? (pf_entry ??))
    636 | @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
     734  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
     735  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
     736  ]
     737| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     738| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
     739| @(pi2 … (pf_entry …))
     740| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
    637741| % [ @pi2 | @(pi2 ?? exits) ]
    638 | @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
    639 | #l' #H @(pi2 ?? l)
    640 | #l #H @(present_included … (pi2 ?? l_default)) repeat @fn_includes_step @I
    641 | #l #H % [ @(present_included … (pi2 ?? l_case)) repeat @fn_includes_step @I | @H ]
     742| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
     743| #l' #H @(pi2 … l)
     744| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
     745| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     746| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
     747| #_ (* see above *) <E @(pi2 ?? r)
    642748| @(pi2 … (pf_entry …))
    643749| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    644         |@Cminor_labels_sig @(stmt_labels_added … (pi2 … f))
     750        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
    645751        ]
    646752| #l1 #H whd %2 @lookup_label_lpresent
    647 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added … (pi2 … f)) ]
    648 ] qed.
     753| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
     754] qed.
     755
    649756
    650757definition c2ra_function (*: internal_function → internal_function*) ≝
     
    655762let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
    656763let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
    657 let 〈result, locals, reggen〉
    658   match f_return f with
    659   [ None ⇒ 〈None ?, locals0, reggen2〉
     764let ❬locals_reggen, result❭
     765  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
     766  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
    660767  | Some ty ⇒
    661768      let 〈r,gen〉 ≝ fresh … reggen2 in
    662         〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
     769        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
     770let locals ≝ \fst locals_reggen in
     771let reggen ≝ \snd locals_reggen in
    663772let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
    664773let 〈l,labgen〉 ≝ fresh … labgen1 in
     
    666775  mk_partial_fn
    667776    label_env
     777    env
    668778    labgen
    669779    reggen
    670     result
    671780    params
    672781    locals
     782    result
     783    ?
    673784    (f_stacksize f)
    674785    (add ?? (empty_map …) l St_return)
     786    ?
    675787    ?
    676788    l
     
    678790do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
    679791OK ? (mk_internal_function
    680     (pf_labgen ? f)
    681     (pf_reggen ? f)
    682     (pf_result ? f)
    683     (pf_params ? f)
    684     (pf_locals ? f)
    685     (pf_stacksize ? f)
    686     (pf_graph ? f)
     792    (pf_labgen f)
     793    (pf_reggen f)
     794    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
     795    (pf_params f)
     796    (pf_locals f)
     797    (pf_stacksize f)
     798    (pf_graph f)
    687799    ?
    688     (pf_entry ? f)
    689     (pf_exit ? f)
     800    (pf_typed … f)
     801    (pf_entry … f)
     802    (pf_exit … f)
    690803  ).
    691804[ @I
     
    693806  #s * #V #L %
    694807  [ @(stmt_vars_mp … V)
    695     #i #H cases (Exists_append … H)
     808    #i #t #H cases (Exists_append … H)
     809    cases daemon (* XXX needs populates_env
    696810    [ #H1 @(populate_extends ?????? (sym_eq … E2))
    697811          @(populates_env … (sym_eq … E1)) @H1
    698812    | #H1 @(populates_env … (sym_eq … E2)) @H1
    699     ]
     813    ]*)
    700814  | @(stmt_labels_mp … L)
    701815    #l #H @(populates_label_env … (sym_eq … El)) @H
    702816  ]
    703 | #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
     817| #l #s #E @(labels_P_mp … (pf_closed f l s E))
    704818  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
    705819  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
     
    712826  ]
    713827  ]
     828| cases daemon (* XXX need information about env *)
    714829| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
    715830  [ * #E1 #E2 >E2 @I
    716831  | whd in ⊢ (??%? → ?); #E' destruct (E')
    717832  ]
    718 | *: whd >lookup_add_hit % #E destruct
     833| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
     834  [ * #E1 #E2 >E2 @I
     835  | whd in ⊢ (??%? → ?); #E' destruct (E')
     836  ]
     837| 7,8: whd >lookup_add_hit % #E destruct
     838| % @refl
    719839]
    720840qed.
  • src/RTLabs/syntax.ma

    r1369 r1626  
    1313| St_cost : costlabel → label → statement
    1414| St_const : register → constant → label → statement
    15 | St_op1 : ∀t,t'. unary_operation t t' → register → register → label → statement (* destination source *)
     15| St_op1 : ∀t,t'. unary_operation t' t → register → register → label → statement (* destination source *)
    1616| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    1717| St_load : memory_chunk → register → register → label → statement
     
    2525| St_return : statement
    2626.
     27
     28definition env_has : list (register × typ) → register → typ → Prop ≝
     29λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
     30
     31definition statement_typed : list (register × typ) → statement → Prop ≝
     32λe,s. match s with
     33[ St_op1 t t' _ r r' _ ⇒ env_has e r t ∧ env_has e r' t'
     34| _ ⇒ True
     35].
    2736
    2837definition labels_P : (label → Prop) → statement → Prop ≝
     
    5261λg,s. labels_P (present ?? g) s.
    5362
     63definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
     64λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
     65
    5466definition graph_closed : graph statement → Prop ≝
    55 λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
     67  λg. forall_nodes ? (labels_present g) g.
     68definition graph_typed : list (register × typ) → graph statement → Prop ≝
     69  λe. forall_nodes ? (statement_typed e).
    5670
    5771record internal_function : Type[0] ≝
     
    6478; f_graph     : graph statement
    6579; f_closed    : graph_closed f_graph
     80; f_typed     : graph_typed (f_locals @ f_params) f_graph
    6681; f_entry     : Σl:label. present ?? f_graph l
    6782; f_exit      : Σl:label. present ?? f_graph l
  • src/common/Errors.ma

    r1609 r1626  
    303303notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    304304
     305definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
     306  match f return λx. f = x → ? with
     307  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
     308  | Error msg ⇒ λ_. Error ? msg
     309  ] (refl ? f).
     310
     311notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
     312
    305313definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    306314 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
Note: See TracChangeset for help on using the changeset viewer.