%% Mechanized Proofs of type safety from %% "Distributed Control Flow with Classical Modal Logic" %% by Tom Murphy VII, Karl Crary, and Robert Harper %% %% Code by Tom Murphy %% Thanks: Jason Reed and Karl Crary %% 19 Aug 2004 %%%% %%%% Types. %%%% world : type. %name world W w. typ : type. %name typ A a. & : typ -> typ -> typ. %infix none 9 &. => : typ -> typ -> typ. %infix right 8 =>. ! : typ -> typ. %prefix 9 !. ? : typ -> typ. %prefix 9 ?. _|_ : typ. %%%% %%%% Syntax of expressions. %%%% % now we have constant worlds wconst : nat -> world. % expressions and continuation expressions exp : type. %name exp M m. cexp : type. %name cexp C c. % products pair : exp -> exp -> exp. fst : exp -> exp. snd : exp -> exp. % implication app : exp -> exp -> exp. lam : (exp -> exp) -> exp. % box box : (world -> exp) -> exp. unbox : exp -> exp. getbox : world -> exp -> exp. % dia here : exp -> exp. letdia : exp -> (world -> exp -> exp) -> exp. getdia : world -> exp -> exp. % falsehood rpc : world -> exp -> exp. % classical stuff throw : exp -> cexp -> exp. letcc : (cexp -> exp) -> exp. % new: runtime artifacts lab : nat -> exp. addr : world -> nat -> exp. caddr : world -> nat -> cexp. % proofs of value-ness value : exp -> type. valbox : value (box _). valaddr : value (addr _ _). valpair : value E1 -> value E2 -> value (pair E1 E2). vallam : value (lam _). %%%% %%%% Syntax of continuations. %%%% cont : type. %name cont K k. finish : cont. abort : cont. ffst : cont -> cont. fsnd : cont -> cont. funbox : cont -> cont. % returnbox w.k (world must be constant) freturnbox : nat -> nat -> cont. freturndia : nat -> nat -> cont. fletdia : cont -> (world -> exp -> exp) -> cont. % k |> ([], M) fpair1 : cont -> exp -> cont. % k |> (v, []) fpair2 : cont -> {V : exp} value V -> cont. % k |> here [] fhere : cont -> cont. % k |> ([] M) fapp1 : cont -> exp -> cont. % k |> (v []) fapp2 : cont -> {V : exp} value V -> cont. %%%% %%%% Networks. %%%% % pass in size of network (number of worlds) network : nat -> type. %name network NN net. % world configurations have tables of values vlist : nat -> type. vnil : vlist 0. v// : {V : exp} value V -> vlist N -> vlist (s N). % and tables of continuations clist : nat -> type. cnil : clist 0. c// : cont -> clist N -> clist (s N). % lists of world data wdlist : nat -> type. %name wdlist W w. wdnil : wdlist 0. % cont table value table wd// : clist X -> vlist Y -> wdlist N -> wdlist (s N). % mode of evaluation mode : type. eval : exp -> mode. ret : {V : exp} value V -> mode. net : % configuration of worlds wdlist N -> % current world {cur : nat} % current continuation cont -> % current mode (eval exp -or- ret v) mode -> network N. %%%% %%%% Store (configuration) typing. %%%% % tables mapping numbers to types % this is used for both continuation table types % and value table types typetable : nat -> type. ttnil : typetable 0. tt// : typ -> typetable N -> typetable (s N). % lists of world types wslist : nat -> type. %name wslist S s. wsnil : wslist 0. % continuation table, value table, tail ws// : typetable X -> typetable Y -> wslist N -> wslist (s N). %%%% %%%% Typing labels %%%% % typing for labels is tricky because we have to look in % the store type. % assert that b(n) = A. Note that labels count up from % the end of the list, so the user of this relation must % first compute the actual offset tt_sub : typetable X -> nat -> typ -> type. tts_found : tt_sub (tt// A _) 0 A. tts_next : tt_sub TL N A -> tt_sub (tt// _ TL) (s N) A. % assert that S |- lab : A @ W. % store lab A world labtype_is : wslist N -> nat -> typ -> nat -> type. % offset of this entry is (size - 1) - label lti_found : minus SIZE-1 L OFF -> tt_sub VT OFF A -> labtype_is (ws// _ (VT : typetable (s SIZE-1)) _) L A 0. lti_next : labtype_is TL L A W -> labtype_is (ws// _ _ TL) L A (s W). % same, looks in continuation table clabtype_is : wslist N -> nat -> typ -> nat -> type. %name clabtype_is CLTI clti. clti_found : minus SIZE-1 L OFF -> tt_sub CT OFF A -> clabtype_is (ws// (CT : typetable (s SIZE-1)) _ _) L A 0. clti_next : clabtype_is TL L A W -> clabtype_is (ws// _ _ TL) L A (s W). %%%% %%%% Typing of worlds. %%%% % essentially, just that the world exists welltyped_world : wslist X -> world -> type. %name welltyped_world WTW wtw. wtw_const : {S : wslist X} J < X -> welltyped_world S (wconst J). %%%% %%%% Typing of continuation expressions. %%%% welltyped_cexp : wslist X -> cexp -> typ -> world -> type. % continuation address constants wtce_caddr : clabtype_is S L A J -> welltyped_cexp S (caddr (wconst J) L) A (wconst J). %%%% %%%% Typing of expressions. %%%% welltyped_exp : wslist X -> exp -> typ -> world -> type. wte_pair : welltyped_exp S M A W -> welltyped_exp S N B W -> welltyped_exp S (pair M N) (A & B) W. wte_fst : welltyped_exp S M (A & B) W -> welltyped_exp S (fst M) A W. wte_snd : welltyped_exp S M (A & B) W -> welltyped_exp S (snd M) B W. wte_here : welltyped_exp S M A W -> welltyped_exp S (here M) (? A) W. wte_app : welltyped_exp S M (A => B) W -> welltyped_exp S N A W -> welltyped_exp S (app M N) B W. wte_lam : ({x : exp} {w : {X : nat}{S : wslist X} welltyped_exp S x A W} welltyped_exp S (M x) B W) -> welltyped_exp S (lam ([x] M x)) (A => B) W. wte_letdia : welltyped_exp S M (? A) W -> ({w : world} {wt1 : {X : nat}{S : wslist X} welltyped_world S w } {x : exp} {wt2 : {X : nat}{S : wslist X} welltyped_exp S x A w} welltyped_exp S (N w x) C W) -> welltyped_exp S (letdia M N) C W. wte_box : ({w : world} {wt : {X : nat}{S : wslist X} welltyped_world S w } welltyped_exp S (M w) A w) -> welltyped_exp S (box ([w] M w)) (! A) W. wte_unbox : welltyped_exp S M (! A) W -> welltyped_exp S (unbox M) A W. wte_letcc : ({u : cexp} {wt : {X : nat}{S : wslist X} welltyped_cexp S u A W} welltyped_exp S (M u) A W) -> welltyped_exp S (letcc M) A W. wte_throw : welltyped_cexp S U A W -> welltyped_exp S M A W -> welltyped_exp S (throw M U) C W'. wte_getbox : welltyped_world S W' -> welltyped_exp S M (! A) W' -> welltyped_exp S (getbox W' M) (! A) W. wte_getdia : welltyped_world S W' -> welltyped_exp S M (? A) W' -> welltyped_exp S (getdia W' M) (? A) W. wte_rpc : welltyped_world S W' -> welltyped_exp S M _|_ W' -> welltyped_exp S (rpc W' M) _|_ W. wte_lab : labtype_is S L A W -> welltyped_exp (S : wslist N) (lab L) A (wconst W). % addrs are like labels wte_addr : labtype_is S L A J -> welltyped_exp S (addr (wconst J) L) (? A) (wconst _). %%%% %%%% Typing of continuations. %%%% welltyped_cont : wslist N -> cont -> typ -> world -> type. %name welltyped_cont WTC wtc. wtc_finish : welltyped_cont _ finish _ _. wtc_abort : welltyped_cont S abort _|_ W. wtc_freturnbox : clabtype_is S L (! A) J -> welltyped_cont S (freturnbox J L) (! A) W. wtc_freturndia : clabtype_is S L (? A) J -> welltyped_cont S (freturndia J L) (? A) W. wtc_fst : welltyped_cont S K A W -> welltyped_cont S (ffst K) (A & _) W. wtc_snd : welltyped_cont S K B W -> welltyped_cont S (fsnd K) (_ & B) W. wtc_pair1 : welltyped_exp S M B W -> welltyped_cont S K (A & B) W -> welltyped_cont S (fpair1 K M) A W. wtc_pair2 : welltyped_exp S V A W -> welltyped_cont S K (A & B) W -> welltyped_cont S (fpair2 K V VP) B W. wtc_here : welltyped_cont S K (? A) W -> welltyped_cont S (fhere K) A W. wtc_app1 : welltyped_exp S M A W -> welltyped_cont S K B W -> welltyped_cont S (fapp1 K M) (A => B) W. wtc_app2 : welltyped_exp S V (A => B) W -> welltyped_cont S K B W -> welltyped_cont S (fapp2 K V VP) A W. wtc_unbox : welltyped_cont S K A W -> welltyped_cont S (funbox K) (! A) W. wtc_letdia : welltyped_cont S K C W -> ({w : world} {wtw : {X : nat}{SS : wslist X} welltyped_world SS w} {x : exp}{wt : {X : nat}{SS : wslist X} welltyped_exp SS x A w} welltyped_exp S (N w x) C W) -> welltyped_cont S (fletdia K N) (? A) W. % fletdia : cont -> (world -> exp -> exp) -> cont. % typing of expressions and continuations both respect equality on % worlds wte-resp : {J : nat} { J' : nat } nat-eq J J' -> welltyped_exp S M A (wconst J) -> welltyped_exp S M A (wconst J') -> type. %mode wte-resp +J +JJ' +N +W -W'. wte-respi : wte-resp _ _ nat-eqi D D. wtc-resp : {J : nat} { J' : nat } nat-eq J J' -> welltyped_cont S K A (wconst J) -> welltyped_cont S K A (wconst J') -> type. %mode wtc-resp +J +JJ' +N +W -W'. wtc-respi : wtc-resp _ _ nat-eqi D D. %%%% %%%% Typing of network bits. %%%% welltyped_mode : wslist N -> mode -> typ -> world -> type. wt_eval : welltyped_exp S M A W -> welltyped_mode S (eval M) A W. wt_ret : welltyped_exp S M A W -> welltyped_mode S (ret M _) A W. % ensure that a continuation table has the given type (at the supplied world) % under the given store type. welltyped_conts : wslist N -> typetable M -> clist M -> world -> type. wtcs_empty : welltyped_conts S ttnil cnil W. wtcs_one : welltyped_conts S TTL CTL W -> welltyped_cont S K A W -> welltyped_conts S (tt// A TTL) (c// K CTL) W. % same, but data table welltyped_datas : wslist N -> typetable M -> vlist M -> world -> type. wtds_empty : welltyped_datas S ttnil vnil W. wtds_one : welltyped_datas S TTL VTL W -> welltyped_exp S V A W -> welltyped_datas S (tt// A TTL) (v// V _ VTL) W. % the below requires a nested induction welltyped_worlds' : % size of rest {N : nat} % current index nat -> % full store and rest of store wslist M -> wslist N -> % world data wdlist N -> type. wtws'_empty : welltyped_worlds' 0 _ _ wsnil wdnil. wtws'_one : welltyped_worlds' N (s IDX) S STL WTL -> welltyped_conts S CT CD (wconst IDX) -> welltyped_datas S BT BD (wconst IDX) -> welltyped_worlds' (s N) IDX S (ws// CT BT STL) (wd// CD BD WTL). % ensure that the world configuration has the store type % indicated (in greater store type M) welltyped_worlds : wslist N -> wdlist N -> type. wtws : welltyped_worlds' N 0 S S L -> welltyped_worlds (S : wslist N) L. % sometimes we aggregate wtws in reverse welltyped_worldsr : {M : nat} wslist X -> wslist M -> wdlist M -> type. wtwsr_none : welltyped_worldsr 0 _ wsnil wdnil. wtwsr_one : welltyped_worldsr N-1 S STL WTL -> welltyped_conts S CT CD (wconst N-1) -> welltyped_datas S BT BD (wconst N-1) -> welltyped_worldsr (s N-1) S (ws// CT BT STL) (wd// CD BD WTL). %%%% %%%% Typing of networks. %%%% % type of network (store typing) wellformed : wslist N -> network N -> type. wf_net : % current world must be in bounds J < N -> % must be a mediating type for mode/cont {A : typ} welltyped_mode S M A (wconst J) -> welltyped_cont S K A (wconst J) -> welltyped_worlds S W -> wellformed (S : wslist N) (net W J K M : network N). % extendst T1 T2 iff T1 is a suffix of T2 % (specialized to the cases where the difference is either 0 or 1) extendst : typetable X -> typetable Y -> type. extendst-same : extendst TT TT. extendst-cons : extendst TT (tt// _ TT). % extends S S' if S' has strictly more information, % but they agree on the domain of S. extends : wslist N -> wslist N -> type. %name extends EX ex. ex-none : extends wsnil wsnil. ex-one : extends S S' -> extendst CT CT' -> extendst BT BT' -> extends (ws// CT BT S) (ws// CT' BT' S'). % lemma: a store type extends itself. For most cases of preservation % we don't change the store, so this gets used all over the place ex-id : {S : wslist N} extends S S -> type. %mode ex-id +S -E. ex-id-none : ex-id wsnil ex-none. ex-id-one : ex-id S E -> ex-id (ws// CT BT S) (ex-one E extendst-same extendst-same). %worlds () (ex-id S E). %total S (ex-id S E). %%%% %%%% Lookup of labels. %%%% % lookin B O V % the table B contains value V at offset O lookinv : vlist N -> nat -> {V : exp} value V -> type. %name lookinv LIV liv. lookinv_next : lookinv VTL OFF V VP -> lookinv (v// _ _ VTL) (s OFF) V VP. lookinv_found : lookinv (v// V VP _) 0 V VP. lookinv-resp : nat-eq L L' -> lookinv VL L V VP -> lookinv VL L' V VP -> type. %mode lookinv-resp +B +C -D. lookinv-respi : lookinv-resp nat-eqi D D. lookinc : clist N -> nat -> cont -> type. %name lookinc LIC lic. lookinc_next : lookinc VTL OFF K -> lookinc (c// _ VTL) (s OFF) K. lookinc_found : lookinc (c// K _) 0 K. lookinc-resp : nat-eq L L' -> lookinc VL L K -> lookinc VL L' K -> type. %mode lookinc-resp +B +C -D. lookinc-respi : lookinc-resp nat-eqi D D. % lookupv W J L V % ensure that in config W at world constant J, label L maps to % some value V. lookupv : wdlist N -> nat -> nat -> {V : exp} value V -> type. lookupv_next : lookupv BTL X L V VP -> lookupv (wd// _ BD BTL) (s X) L V VP. lookupv_found : minus SIZE-1 L OFF -> lookinv BD OFF V VP -> lookupv (wd// _ (BD : vlist (s SIZE-1)) _) 0 L V VP. % add_value W J V VAL W' L % adding value V to the world J within W results in worlds % W' and new label L. add_value : wdlist N -> nat -> {V : exp} value V -> wdlist N -> nat -> type. %mode add_value +W +J +V +VP -W' -L. addv_next : add_value BTL X V VP BTL' L -> add_value (wd// CD BD BTL) (s X) V VP (wd// CD BD BTL') L. % adds to the head of the list, which gets index n (the current length) addv_found : {BD : vlist N} add_value (wd// CD BD BTL) 0 V VP (wd// CD (v// V VP BD) BTL) N. % same, but for continuations lookupc : wdlist N -> nat -> nat -> cont -> type. %name lookupc LUC luc. lookupc_next : lookupc BTL X L K -> lookupc (wd// _ _ BTL) (s X) L K. lookupc_found : minus SIZE-1 L OFF -> lookinc CD OFF K -> lookupc (wd// (CD : clist (s SIZE-1)) _ _) 0 L K. add_cont : wdlist N -> nat -> cont -> wdlist N -> nat -> type. %mode add_cont +W +J +K -W' -L. addc_next : add_cont BTL X K BTL' L -> add_cont (wd// CD BD BTL) (s X) K (wd// CD BD BTL') L. % adds to the head of the list, which gets index n (the current length) addc_found : {CD : clist N} add_cont (wd// CD BD BTL) 0 K (wd// (c// K CD) BD BTL) N. %%%% %%%% Stepping relation. %%%% % stepping relation between networks % of the same size. |-> : network N -> network N -> type. %infix none 0 |->. % little trick: terminal network steps to itself % this makes the statement of progress easier. step_done : net W J finish (ret V VP) |-> net W J finish (ret V VP). % labels are complex step_lab : lookupv W J L V VP -> net W J K (eval (lab L)) |-> net W J K (ret V VP). step_pfst : net W J K (eval (fst M)) |-> net W J (ffst K) (eval M). step_psnd : net W J K (eval (snd M)) |-> net W J (fsnd K) (eval M). step_rfst : net W J (ffst K) (ret (pair V _) (valpair VP _)) |-> net W J K (ret V VP). step_rsnd : net W J (fsnd K) (ret (pair _ V) (valpair _ VP)) |-> net W J K (ret V VP). step_ppair : net W J K (eval (pair M N)) |-> net W J (fpair1 K N) (eval M). step_fpair : net W J (fpair1 K N) (ret V VP) |-> net W J (fpair2 K V VP) (eval N). step_rpair : net W J (fpair2 K V VP) (ret VV VVP) |-> net W J K (ret (pair V VV) (valpair VP VVP)). step_phere : net W J K (eval (here M)) |-> net W J (fhere K) (eval M). step_rhere : add_value W J V VP W' L -> net W J (fhere K) (ret V VP) |-> net W' J K (ret (addr (wconst J) L) valaddr). step_papp : net W J K (eval (app M N)) |-> net W J (fapp1 K N) (eval M). step_fapp : net W J (fapp1 K N) (ret V VP) |-> net W J (fapp2 K V VP) (eval N). step_rapp : net W J (fapp2 K (lam F) _) (ret V _) |-> net W J K (eval (F V)). % we need to flip from eval to ret when encountering certain expressions step_taddr : net W J K (eval (addr X L)) |-> net W J K (ret (addr X L) valaddr). step_tbox : net W J K (eval (box M)) |-> net W J K (ret (box M) valbox). step_tlam : net W J K (eval (lam B)) |-> net W J K (ret (lam B) vallam). step_punbox : net W J K (eval (unbox M)) |-> net W J (funbox K) (eval M). step_runbox : net W J (funbox K) (ret (box F) valbox) |-> net W J K (eval (F (wconst J))). step_pletdia : net W J K (eval (letdia M N)) |-> net W J (fletdia K N) (eval M). step_rletdia : net W J (fletdia K N) (ret (addr WW LL) valaddr) |-> net W J K (eval (N WW (lab LL))). step_rletcc : add_cont W J K W' L -> net W J K (eval (letcc M)) |-> net W' J K (eval (M (caddr (wconst J) L))). step_rreturnbox : lookupc W JNEW L K -> net W JOLD (freturnbox JNEW L) (ret (box MB) valbox) |-> net W JNEW K (ret (box MB) valbox). step_rreturndia : lookupc W JNEW L K -> net W JOLD (freturndia JNEW L) (ret (addr AW AL) valaddr) |-> net W JNEW K (ret (addr AW AL) valaddr). step_throw : lookupc W JNEW L K -> net W JOLD _ (eval (throw M (caddr (wconst JNEW) L))) |-> net W JNEW K (eval M). step_getbox : add_cont W JOLD K W' L -> net W JOLD K (eval (getbox (wconst JNEW) M)) |-> net W' JNEW (freturnbox JOLD L) (eval M). step_getdia : add_cont W JOLD K W' L -> net W JOLD K (eval (getdia (wconst JNEW) M)) |-> net W' JNEW (freturndia JOLD L) (eval M). step_rpc : net W JOLD _ (eval (rpc (wconst JNEW) M)) |-> net W JNEW abort (eval M). %%%% %%%% Lemmas. %%%% % lemmas about weakening. weaken-lti : {S : wslist N} {S' : wslist N} extends S S' -> labtype_is S L A W -> labtype_is S' L A W -> type. %mode weaken-lti +S +S' +E +LTI -LTI'. wlti-next : weaken-lti SL SL' E LTI LTI' -> weaken-lti (ws// CT BT SL) (ws// CT' BT' SL') (ex-one E _ _) (lti_next LTI) (lti_next LTI'). wlti-foundsame : weaken-lti _ _ (ex-one _ _ extendst-same) (lti_found MINUS TTS) (lti_found MINUS TTS). wlti-foundcons : minus-sfirst MINUS MINUS' -> weaken-lti (ws// _ (BT : typetable (s SIZE-1)) _) (ws// _ (tt// A BT) _) (ex-one _ _ extendst-cons) (lti_found MINUS TTS) (lti_found MINUS' (tts_next TTS)). %% same as above, for clabtypes weaken-clti : {S : wslist N} {S' : wslist N} extends S S' -> clabtype_is S L A W -> clabtype_is S' L A W -> type. %mode weaken-clti +S +S' +E +CLTI -CLTI'. wclti-next : weaken-clti SL SL' E CLTI CLTI' -> weaken-clti (ws// CT BT SL) (ws// CT' BT' SL') (ex-one E _ _) (clti_next CLTI) (clti_next CLTI'). wclti-foundsame : weaken-clti _ _ (ex-one _ extendst-same _) (clti_found MINUS TTS) (clti_found MINUS TTS). wclti-foundcons : minus-sfirst MINUS MINUS' -> weaken-clti (ws// (CT : typetable (s SIZE-1)) _ _) (ws// (tt// A CT) _ _) (ex-one _ extendst-cons _) (clti_found MINUS TTS) (clti_found MINUS' (tts_next TTS)). %% worlds weaken-wtw : extends S S' -> welltyped_world S W -> welltyped_world S' W -> type. %mode weaken-wtw +E +WT -WT'. wwtw-const : weaken-wtw EX (wtw_const S LT) (wtw_const S' LT). %% continuation expressions weaken-wtce : extends S S' -> welltyped_cexp S U A W -> welltyped_cexp S' U A W -> type. %mode weaken-wtce +E +WT -WT'. wwtce-caddr : weaken-clti _ _ EX CLTI CLTI' -> weaken-wtce EX (wtce_caddr CLTI) (wtce_caddr CLTI'). %% expressions weaken-wte : extends S S' -> welltyped_exp S M A W -> welltyped_exp S' M A W -> type. %mode weaken-wte +E +WT -WT'. wwte-throw : weaken-wtce EX CW CW' -> weaken-wte EX W W' -> weaken-wte EX (wte_throw CW W) (wte_throw CW' W'). wwte-unbox : weaken-wte EX W W' -> weaken-wte EX (wte_unbox W) (wte_unbox W'). wwte-lab : weaken-lti _ _ EX LTI LTI' -> weaken-wte EX (wte_lab LTI) (wte_lab LTI'). wwte-addr : weaken-lti _ _ EX LTI LTI' -> weaken-wte EX (wte_addr LTI) (wte_addr LTI'). wwte-pair : weaken-wte EX W1 W1' -> weaken-wte EX W2 W2' -> weaken-wte EX (wte_pair W1 W2) (wte_pair W1' W2'). wwte-app : weaken-wte EX W1 W1' -> weaken-wte EX W2 W2' -> weaken-wte EX (wte_app W1 W2) (wte_app W1' W2'). wwte-box : ({w : world} {wt : {X : nat} {S : wslist X} welltyped_world S w} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wt Y s) (wt Y s')} weaken-wte EX (WT w wt) (WT' w wt)) -> weaken-wte EX (wte_box WT) (wte_box WT'). % we have to do a little trick here. it seems there's no way % to prove directly what we want -- to hypothesize a well-typing % for x and assume that there exists some weakening of it. % instead, we assume a ridiculous thing: that there is a well-typing % for every possible store. later we will substitute this out with % another theorem. wwte-lam : ({x : exp} {w : {X : nat} {S : wslist X} welltyped_exp S x A W} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wte EX (w Y s) (w Y s')} weaken-wte EX (W1 x w) (W1' x w)) -> weaken-wte EX (wte_lam ([x] [wt] W1 x wt)) (wte_lam ([x] [wt] W1' x wt)). % ditto for this binder wwte-letdia : weaken-wte EX M M' -> ({w : world} {wtw : {X : nat}{S : wslist X} welltyped_world S w } {thm0 : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wtw Y s) (wtw Y s')} {x : exp} {wt : {X : nat} {S : wslist X} welltyped_exp S x A w} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wte EX (wt Y s) (wt Y s')} weaken-wte EX (N w wtw x wt) (N' w wtw x wt)) -> weaken-wte EX (wte_letdia M ([w][x][wt] N w x wt)) (wte_letdia M' ([w][x][wt] N' w x wt)). wwte-letcc : ({u : cexp} {w : {X : nat} {S : wslist X} welltyped_cexp S u A W} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtce EX (w Y s) (w Y s')} weaken-wte EX (M u w) (M' u w)) -> weaken-wte EX (wte_letcc ([u][wt] M u wt)) (wte_letcc ([u][wt] M' u wt)). wwte-fst : weaken-wte EX W W' -> weaken-wte EX (wte_fst W) (wte_fst W'). wwte-snd : weaken-wte EX W W' -> weaken-wte EX (wte_snd W) (wte_snd W'). wwte-here : weaken-wte EX W W' -> weaken-wte EX (wte_here W) (wte_here W'). wwte-getbox : weaken-wtw EX WO WO' -> weaken-wte EX W W' -> weaken-wte EX (wte_getbox WO W) (wte_getbox WO' W'). wwte-getdia : weaken-wtw EX WO WO' -> weaken-wte EX W W' -> weaken-wte EX (wte_getdia WO W) (wte_getdia WO' W'). wwte-rpc : weaken-wtw EX WO WO' -> weaken-wte EX W W' -> weaken-wte EX (wte_rpc WO W) (wte_rpc WO' W'). weaken-wtc : extends S S' -> welltyped_cont S K A J -> welltyped_cont S' K A J -> type. %mode weaken-wtc +E +W -W'. wwtc-finish : weaken-wtc _ wtc_finish wtc_finish. wwtc-abort : weaken-wtc _ wtc_abort wtc_abort. wwtc-freturnbox : weaken-clti _ _ E CLTI CLTI' -> weaken-wtc E (wtc_freturnbox CLTI) (wtc_freturnbox CLTI'). wwtc-freturndia : weaken-clti _ _ E CLTI CLTI' -> weaken-wtc E (wtc_freturndia CLTI) (wtc_freturndia CLTI'). wwtc-fst : weaken-wtc E K K' -> weaken-wtc E (wtc_fst K) (wtc_fst K'). wwtc-snd : weaken-wtc E K K' -> weaken-wtc E (wtc_snd K) (wtc_snd K'). wwtc-pair1 : weaken-wtc E K K' -> weaken-wte E M M' -> weaken-wtc E (wtc_pair1 M K) (wtc_pair1 M' K'). wwtc-pair2 : weaken-wtc E K K' -> weaken-wte E M M' -> weaken-wtc E (wtc_pair2 M K) (wtc_pair2 M' K'). wwtc-unbox : weaken-wtc E K K' -> weaken-wtc E (wtc_unbox K) (wtc_unbox K'). wwtc-here : weaken-wtc E K K' -> weaken-wtc E (wtc_here K) (wtc_here K'). wwtc-app1 : weaken-wtc E K K' -> weaken-wte E M M' -> weaken-wtc E (wtc_app1 M K) (wtc_app1 M' K'). wwtc-app2 : weaken-wtc E K K' -> weaken-wte E M M' -> weaken-wtc E (wtc_app2 M K) (wtc_app2 M' K'). wwtc-letdia : weaken-wtc E K K' -> ({w : world} {wtw : {X : nat}{S : wslist X} welltyped_world S w } {thm0 : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wtw Y s) (wtw Y s')} {x : exp}{wt : {X : nat}{SS : wslist X} welltyped_exp SS x A w} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wte EX (wt Y s) (wt Y s')} weaken-wte E (M w wtw x wt) (M' w wtw x wt)) -> weaken-wtc E (wtc_letdia K M) (wtc_letdia K' M'). weaken-wtds : extends S S' -> welltyped_datas S TT VT W -> welltyped_datas S' TT VT W -> type. %mode weaken-wtds +E +WD -WD'. wwtds-empty : weaken-wtds _ wtds_empty wtds_empty. wwtds-one : weaken-wtds E DS DS' -> weaken-wte E WE WE' -> weaken-wtds E (wtds_one DS WE) (wtds_one DS' WE'). weaken-wtcs : extends S S' -> welltyped_conts S TT VT W -> welltyped_conts S' TT VT W -> type. %mode weaken-wtcs +E +WD -WD'. wwtcs-empty : weaken-wtcs _ wtcs_empty wtcs_empty. wwtcs-one : weaken-wtcs E CS CS' -> weaken-wtc E K K' -> weaken-wtcs E (wtcs_one CS K) (wtcs_one CS' K'). weaken-wtws : extends S S' -> welltyped_worlds' N IDX S SL WL -> welltyped_worlds' N IDX S' SL WL -> type. %mode weaken-wtws +E +WD -WD'. wwtws-empty : weaken-wtws _ wtws'_empty wtws'_empty. wwtws-one : weaken-wtws S WT WT' -> weaken-wtds S WD WD' -> weaken-wtcs S WC WC' -> weaken-wtws S (wtws'_one WT WC WD) (wtws'_one WT' WC' WD'). %% first phase of totality/world checking %block blockm : some {A : typ} {J : nat} block {m:exp} {wt : {X : nat} {SS : wslist X} welltyped_exp SS m A (wconst J)} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {ex : extends s s'} weaken-wte ex (wt Y s) (wt Y s')}. %block blockx : some {A : typ} {W : world} block {x : exp} {w : {X : nat} {S : wslist X} welltyped_exp S x A W} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wte EX (w Y s) (w Y s')}. %block blocku : some {A : typ} {W : world} block {u : cexp} {w : {X : nat} {S : wslist X} welltyped_cexp S u A W} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtce EX (w Y s) (w Y s')}. %block blockww : block {w : world} {wtw : {X : nat}{S : wslist X} welltyped_world S w } {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wtw Y s) (wtw Y s')}. %worlds (blockm) (wte-resp _ _ _ _ _). %total {} (wte-resp _ _ _ _ _). %worlds (blockm) (wtc-resp _ _ _ _ _). %total {} (wtc-resp _ _ _ _ _). %worlds (blockm) (lookinv-resp _ _ _). %total {} (lookinv-resp _ _ _). %worlds (blockm) (lookinc-resp _ _ _). %total {} (lookinc-resp _ _ _). %worlds (blockx | blockww) (weaken-wtw _ _ _). %total W (weaken-wtw _ W _). %worlds (blockx | blockww | blocku) (weaken-lti _ _ _ _ _). %total LT (weaken-lti _ _ _ LT _). %worlds (blockx | blockww | blocku) (weaken-clti _ _ _ _ _). %total LT (weaken-clti _ _ _ LT _). %worlds (blockx | blockww | blocku | blockm) (weaken-wtce _ _ _). %total W (weaken-wtce _ W _). %worlds (blockx | blockww | blocku | blockm) (weaken-wte _ _ _). %total W (weaken-wte _ W _). %worlds (blockx | blockww | blockm) (weaken-wtc _ _ _). %total W (weaken-wtc _ W _). %worlds (blockm) (weaken-wtds _ _ _). %total W (weaken-wtds _ W _). %worlds (blockm) (weaken-wtcs _ _ _). %total W (weaken-wtcs _ W _). %worlds (blockm) (weaken-wtws _ _ _). %total W (weaken-wtws _ W _). % substitution for magic world hypotheses in % expression typing derivations. Sticks in the % constant world J; all we need to know is that % it's in the domain of the store type (J < SN). wte-wsubst : {J : nat} J < SN -> ({wt : {X : nat} {SS : wslist X} welltyped_world SS (wconst J)} welltyped_exp S M B WB) -> welltyped_exp (S : wslist SN) M B WB -> type. %mode wte-wsubst +D1 +D2 +D2 -D3. wtews-closed : wte-wsubst J LT ([wt] M) M. % uses var wtews-rpcv : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt : {X : nat} {SS : wslist X} welltyped_world SS (wconst J)] wte_rpc (wt _ S) (WT wt)) (wte_rpc (wtw_const S LT) WT'). % doesn't use var wtews-rpc : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt] wte_rpc WW (WT wt)) (wte_rpc WW WT'). % uses var wtews-getboxv : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt : {X : nat} {SS : wslist X} welltyped_world SS (wconst J)] wte_getbox (wt _ S) (WT wt)) (wte_getbox (wtw_const S LT) WT'). % doesn't use var wtews-getbox : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt] wte_getbox WW (WT wt)) (wte_getbox WW WT'). % uses var wtews-getdiav : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt : {X : nat} {SS : wslist X} welltyped_world SS (wconst J)] wte_getdia (wt _ S) (WT wt)) (wte_getdia (wtw_const S LT) WT'). % doesn't use var wtews-getdia : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt] wte_getdia WW (WT wt)) (wte_getdia WW WT'). wtews-throw : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt] wte_throw WC (WT wt)) (wte_throw WC WT'). wtews-unbox : wte-wsubst J LT ([wt] WT wt) WT' -> wte-wsubst J LT ([wt] wte_unbox (WT wt)) (wte_unbox WT'). wtews-app : wte-wsubst J LT ([w] WF w) WF' -> wte-wsubst J LT ([w] WB w) WB' -> wte-wsubst J LT ([w : {X : nat} {SS : wslist X} welltyped_world SS (wconst J)] wte_app (WF w) (WB w)) (wte_app WF' WB'). wtews-addr : wte-wsubst J LT ([w] wte_addr LTI) (wte_addr LTI). wtews-lab : wte-wsubst J LT ([wt] wte_lab LTI) (wte_lab LTI). wtews-pair : wte-wsubst J LT ([wt] W1 wt) W1' -> wte-wsubst J LT ([wt] W2 wt) W2' -> wte-wsubst J LT ([wt] wte_pair (W1 wt) (W2 wt)) (wte_pair W1' W2'). wtews-fst : wte-wsubst J LT ([wt] WW wt) WW' -> wte-wsubst J LT ([wt] wte_fst (WW wt)) (wte_fst WW'). wtews-snd : wte-wsubst J LT ([wt] WW wt) WW' -> wte-wsubst J LT ([wt] wte_snd (WW wt)) (wte_snd WW'). wtews-here : wte-wsubst J LT ([wt] WW wt) WW' -> wte-wsubst J LT ([wt] wte_here (WW wt)) (wte_here WW'). wtews-box : ({wo : world} {wtw : {X : nat}{S : wslist X} welltyped_world S wo } {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wtw Y s) (wtw Y s')} wte-wsubst J LT ([w] W w wo wtw) (W' wo wtw)) -> wte-wsubst J LT ([w] wte_box (W w)) (wte_box W'). wtews-lam : ({xx : exp} {ww : {X : nat} {SS : wslist X} welltyped_exp SS xx A' _} % substituting into this variable results in the variable {thm : {X : nat} {SS : wslist X} {JJ : nat} {LLT : JJ < X} wte-wsubst JJ LLT ([_] ww X SS) (ww X SS)} wte-wsubst J LT ([wt] WW xx ww wt) (WW' xx ww)) -> wte-wsubst J LT ([wt] wte_lam ([xx][ww] WW xx ww wt)) (wte_lam ([xx][ww] WW' xx ww)). wtews-letdia : wte-wsubst J LT ([wt] M wt) M' -> % essentially same as lambda case + box case ({wo : world} {wtw : {X : nat}{S : wslist X} welltyped_world S wo } {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wtw Y s) (wtw Y s')} {xx : exp} {wtt : {X : nat} {SS : wslist X} welltyped_exp SS xx A' wo} {thm : {X : nat} {SS : wslist X} {JJ : nat} {LLT : JJ < X} wte-wsubst JJ LLT ([_] wtt X SS) (wtt X SS)} wte-wsubst J LT ([wt] N wo wtw xx wtt wt) (N' wo wtw xx wtt)) -> wte-wsubst J LT ([wt] wte_letdia (M wt) ([ww : world][wwt][xx : exp][wtt] N ww wwt xx wtt wt)) (wte_letdia M' ([ww][wwt][xx][wtt] N' ww wwt xx wtt)). wtews-letcc : ({uu : cexp} {ww : {X : nat} {SS : wslist X} welltyped_cexp SS uu A' W'} wte-wsubst J LT ([wt] WW uu ww wt) (WW' uu ww)) -> wte-wsubst J LT ([wt] wte_letcc ([uu][ww] WW uu ww wt)) (wte_letcc ([uu][ww] WW' uu ww)). wte-csubst : welltyped_cexp S N A WA -> ({u : cexp}{wt : {X : nat} {SS : wslist X} welltyped_cexp SS u A WA} welltyped_exp S (M u) B WB) -> welltyped_exp S (M N) B WB -> type. %mode wte-csubst +D1 +D2 -D3. % vars are throws wtecs-throwv : wte-csubst WTA ([x][w] WT x w) WT' -> wte-csubst WTA ([x][w] wte_throw (w _ S) (WT x w)) (wte_throw WTA WT'). % (but we might throw to a different var) wtecs-throw : wte-csubst WTA ([x][w] WT x w) WT' -> wte-csubst WTA ([x][w] wte_throw WC (WT x w)) (wte_throw WC WT'). wtecs-rpc : wte-csubst WTA ([x][w] WT x w) WT' -> wte-csubst WTA ([x][w] wte_rpc WW (WT x w)) (wte_rpc WW WT'). wtecs-getbox : wte-csubst WTA ([x][w] WT x w) WT' -> wte-csubst WTA ([x][w] wte_getbox WW (WT x w)) (wte_getbox WW WT'). wtecs-getdia : wte-csubst WTA ([x][w] WT x w) WT' -> wte-csubst WTA ([x][w] wte_getdia WW (WT x w)) (wte_getdia WW WT'). wtecs-unbox : wte-csubst WTA ([x][w] WT x w) WT' -> wte-csubst WTA ([x][w] wte_unbox (WT x w)) (wte_unbox WT'). wtecs-app : wte-csubst WTA ([x][w] WF x w) WF' -> wte-csubst WTA ([x][w] WB x w) WB' -> wte-csubst WTA ([u : cexp] [w : {X : nat} {SS : wslist X} welltyped_cexp SS u A WA] wte_app (WF u w) (WB u w)) (wte_app WF' WB'). wtecs-addr : wte-csubst WTA ([x][w] wte_addr LTI) (wte_addr LTI). wtecs-lab : wte-csubst WTA ([x][w] wte_lab LTI) (wte_lab LTI). wtecs-pair : wte-csubst WTA ([x][w] W1 x w) W1' -> wte-csubst WTA ([x][w] W2 x w) W2' -> wte-csubst WTA ([x][w] wte_pair (W1 x w) (W2 x w)) (wte_pair W1' W2'). wtecs-fst : wte-csubst WTA ([x][w] WW x w) WW' -> wte-csubst WTA ([x][w] wte_fst (WW x w)) (wte_fst WW'). wtecs-snd : wte-csubst WTA ([x][w] WW x w) WW' -> wte-csubst WTA ([x][w] wte_snd (WW x w)) (wte_snd WW'). wtecs-here : wte-csubst WTA ([x][w] WW x w) WW' -> wte-csubst WTA ([x][w] wte_here (WW x w)) (wte_here WW'). wtecs-box : ({wo : world} {wtw : {X : nat}{S : wslist X} welltyped_world S wo } wte-csubst WTA ([x][w] W x w wo wtw) (W' wo wtw)) -> wte-csubst WTA ([x][w] wte_box (W x w)) (wte_box W'). wtecs-lam : ({xx : exp} {ww : {X : nat} {SS : wslist X} welltyped_exp SS xx A' W'} % substituting into this variable results in the variable {thm : {X : nat} {SS : wslist X} {B : typ} {WO : world} {U : cexp} {WTN : welltyped_cexp SS U B WO} wte-csubst WTN ([_][_] ww X SS) (ww X SS)} wte-csubst WTA ([u][w] WW xx ww u w) (WW' xx ww)) -> wte-csubst WTA ([u][w] wte_lam ([xx][ww] WW xx ww u w)) (wte_lam ([xx][ww] WW' xx ww)). wtecs-letdia : wte-csubst WTA ([x][wt] M x wt) M' -> % essentially same as lambda case + box case ({ww : world} {wwt : {X : nat} {SS : wslist X} welltyped_world SS ww} {xx : exp} {wtt : {X : nat} {SS : wslist X} welltyped_exp SS xx A' ww} {thm : {X : nat} {SS : wslist X} {B : typ} {WO : world} {U : cexp} {WTN : welltyped_cexp SS U B WO} wte-csubst WTN ([_][_] wtt X SS) (wtt X SS)} wte-csubst WTA ([u][w] N ww wwt xx wtt u w) (N' ww wwt xx wtt)) -> wte-csubst WTA ([u][wt] wte_letdia (M u wt) ([ww : world][wwt][xx : exp][wtt] N ww wwt xx wtt u wt)) (wte_letdia M' ([ww][wwt][xx][wtt] N' ww wwt xx wtt)). wtecs-letcc : ({uu : cexp} {ww : {X : nat} {SS : wslist X} welltyped_cexp SS uu A' W'} % no need for theorem here. wte-csubst WTA ([u][w] WW uu ww u w) (WW' uu ww)) -> wte-csubst WTA ([u][w] wte_letcc ([uu][ww] WW uu ww u w)) (wte_letcc ([uu][ww] WW' uu ww)). wtecs-closed : wte-csubst WTA ([x][w] M) M. % substitution lemma allows us to substitute out "magic" hypotheses. wte-subst : welltyped_exp S N A WA -> ({e : exp}{w : {X : nat} {SS : wslist X} welltyped_exp SS e A WA} welltyped_exp S (M e) B WB) -> welltyped_exp S (M N) B WB -> type. %mode wte-subst +D1 +D2 -D3. wtes-closed : wte-subst WTA ([x][w] M) M. wtes-var : wte-subst (WTA : welltyped_exp S N A WA) ([x][w] w _ S) WTA. wtes-throw : wte-subst WTA ([x][w] WT x w) WT' -> wte-subst WTA ([x][w] wte_throw WC (WT x w)) (wte_throw WC WT'). wtes-rpc : wte-subst WTA ([x][w] WT x w) WT' -> wte-subst WTA ([x][w] wte_rpc WW (WT x w)) (wte_rpc WW WT'). wtes-getbox : wte-subst WTA ([x][w] WT x w) WT' -> wte-subst WTA ([x][w] wte_getbox WW (WT x w)) (wte_getbox WW WT'). wtes-getdia : wte-subst WTA ([x][w] WT x w) WT' -> wte-subst WTA ([x][w] wte_getdia WW (WT x w)) (wte_getdia WW WT'). wtes-unbox : wte-subst WTA ([x][w] WT x w) WT' -> wte-subst WTA ([x][w] wte_unbox (WT x w)) (wte_unbox WT'). wtes-app : wte-subst WTA ([x][w] WF x w) WF' -> wte-subst WTA ([x][w] WB x w) WB' -> wte-subst WTA ([x : exp] [w : {X : nat} {SS : wslist X} welltyped_exp SS x A WA] wte_app (WF x w) (WB x w)) (wte_app WF' WB'). wtes-addr : wte-subst WTA ([x][w] wte_addr LTI) (wte_addr LTI). wtes-lab : wte-subst WTA ([x][w] wte_lab LTI) (wte_lab LTI). wtes-pair : wte-subst WTA ([x][w] W1 x w) W1' -> wte-subst WTA ([x][w] W2 x w) W2' -> wte-subst WTA ([x][w] wte_pair (W1 x w) (W2 x w)) (wte_pair W1' W2'). wtes-fst : wte-subst WTA ([x][w] WW x w) WW' -> wte-subst WTA ([x][w] wte_fst (WW x w)) (wte_fst WW'). wtes-snd : wte-subst WTA ([x][w] WW x w) WW' -> wte-subst WTA ([x][w] wte_snd (WW x w)) (wte_snd WW'). wtes-here : wte-subst WTA ([x][w] WW x w) WW' -> wte-subst WTA ([x][w] wte_here (WW x w)) (wte_here WW'). wtes-box : ({wo : world} {wot : {X : nat} {S : wslist X} welltyped_world S wo} wte-subst WTA ([x][w] W x w wo wot) (W' wo wot)) -> wte-subst WTA ([x][w] wte_box (W x w)) (wte_box W'). wtes-lam : ({xx : exp} {ww : {X : nat} {SS : wslist X} welltyped_exp SS xx A' W'} % substituting into this variable results in the variable {thm : {X : nat} {SS : wslist X} {B : typ} {WO : world} {N : exp} {WTN : welltyped_exp SS N B WO} wte-subst WTN ([_][_] ww X SS) (ww X SS)} wte-subst WTA ([x][w] WW xx ww x w) (WW' xx ww)) -> wte-subst WTA ([x][w] wte_lam ([xx][ww] WW xx ww x w)) (wte_lam ([xx][ww] WW' xx ww)). wtes-letcc : ({uu : cexp} {ww : {X : nat} {SS : wslist X} welltyped_cexp SS uu A' W'} % no need for theorem here. wte-subst WTA ([x][w] WW uu ww x w) (WW' uu ww)) -> wte-subst WTA ([x][w] wte_letcc ([uu][ww] WW uu ww x w)) (wte_letcc ([uu][ww] WW' uu ww)). wtes-letdia : wte-subst WTA ([x][wt] M x wt) M' -> % essentially same as lambda case + box case ({ww : world} {wwt : {X : nat} {SS : wslist X} welltyped_world SS ww} {xx : exp} {wtt : {X : nat} {SS : wslist X} welltyped_exp SS xx A' ww} {thm : {X : nat} {SS : wslist X} {B : typ} {WO : world} {N : exp} {WTN : welltyped_exp SS N B WO} wte-subst WTN ([_][_] wtt X SS) (wtt X SS)} wte-subst WTA ([x][w] N ww wwt xx wtt x w) (N' ww wwt xx wtt)) -> wte-subst WTA ([x][wt] wte_letdia (M x wt) ([ww : world][wwt][xx : exp][wtt] N ww wwt xx wtt x wt)) (wte_letdia M' ([ww][wwt][xx][wtt] N' ww wwt xx wtt)). %block blocksubst : some {A' : typ} {W' : world} block {xx : exp} {ww : {X : nat} {SS : wslist X} welltyped_exp SS xx A' W'} {thm : {X : nat} {SS : wslist X} {B : typ} {WO : world} {N : exp} {WTN : welltyped_exp SS N B WO} wte-subst WTN ([_][_] ww X SS) (ww X SS)}. %block blocksubstu : some {A' : typ} {W' : world} block {uu : cexp} {ww : {X : nat} {SS : wslist X} welltyped_cexp SS uu A' W'}. %block blockcsubst : some {A' : typ} {W' : world} block {xx : exp} {ww : {X : nat} {SS : wslist X} welltyped_exp SS xx A' W'} {thm : {X : nat} {SS : wslist X} {B : typ} {WO : world} {U : cexp} {WTN : welltyped_cexp SS U B WO} wte-csubst WTN ([_][_] ww X SS) (ww X SS)}. %block blockwsubst' : some {A' : typ} {W' : world} block {xx : exp} {ww : {X : nat} {SS : wslist X} welltyped_exp SS xx A' W'} {thm : {X : nat} {SS : wslist X} {JJ : nat} {LLT : JJ < X} wte-wsubst JJ LLT ([_] ww X SS) (ww X SS)}. %block blockcsubstu : some {A' : typ} {W' : world} block {uu : cexp} {ww : {X : nat} {SS : wslist X} welltyped_cexp SS uu A' W'}. %block blockwwt : block {w : world} {wtw : {X : nat}{S : wslist X} welltyped_world S w }. %block blockwsubst : block {wo : world} {wtw : {X : nat}{S : wslist X} welltyped_world S wo } {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtw EX (wtw Y s) (wtw Y s')}. %worlds (blockm | blockcsubst | blockwsubst' | blockwsubst | blockcsubstu) (wte-wsubst _ _ _ _). %total D3 (wte-wsubst D1 D2 D3 D4). %worlds (blockm | blockcsubst | blockwwt | blockcsubstu) (wte-csubst _ _ _). %total D2 (wte-csubst D1 D2 D3). %worlds (blockm | blocksubst | blockwwt | blocksubstu) (wte-subst _ _ _). %total D2 (wte-subst D1 D2 D3). % %%%% Big lemmas, mostly about labels. % need to know that label lookup will succeed. label-lemma : {W : wdlist N} {S : wslist N} {J : nat} J < N -> welltyped_exp S (lab L) A (wconst J) -> welltyped_worlds S W -> lookupv W J L V VP -> welltyped_exp S V A (wconst J) -> type. %mode label-lemma +W +S +J +LT +WE +WW +L -WV. ll-findworld : {S : wslist X} {J : nat} % searching through the following two {W' : wdlist N} {S' : wslist N} % for this offset {J' : nat} labtype_is S' L A J' -> welltyped_worlds' N IDX S S' W' -> lookupv W' J' L V VP -> % wtw counts up, lookups down. at % every iteration we're getting % closer to (resp. further from) J plus IDX J' J -> welltyped_exp S V A (wconst J) -> type. %mode ll-findworld +S +J +W +S' +J' +LTI +WTW +LV +PLUS -WE. % as findworld, find a label once we've reached % the specific world. This is a little simpler ll-findlab : % storetype -- result must be wellformed in this {S : wslist X} % the world we're looking in {J : nat} % trace of subscripting type table and value table, resp tt_sub VT OFF A -> lookinv VL OFF V VP -> % trace of checking the table against its type welltyped_datas S VT VL (wconst J) -> welltyped_exp S V A (wconst J) -> type. %mode ll-findlab +S +J +TTS +LIV +WTD -WE. llfl-search : ll-findlab S J TTS LIV WTDS WE -> ll-findlab S J (tts_next TTS) (lookinv_next LIV) (wtds_one WTDS _) WE. llfl-found : ll-findlab S J tts_found lookinv_found (wtds_one _ WE) WE. llfw-search : ll-findworld S J WDTL STL J' LTIN WTWTL LUVTL PLUS' WE -> plus-flip PLUS PLUS' -> ll-findworld S J (wd// _ _ WDTL) (ws// _ _ STL) (s J') (lti_next LTIN) (wtws'_one WTWTL _ _) (lookupv_next LUVTL) (PLUS : plus IDX (s J') J) WE. % here we have TTS, which finds that at the offset OFF, % the value table contains the type A. % we also have LIV, which finds that at the offset OFF', % the value table contains the value V. % the sizes of the two tables are the same, because % wtws'_one requires them to be. % OFF and OFF' are actually equal as a result, but LF doesn't % know this because it doesn't know that minus is determinisic. llfw-found : ll-findworld S IDX=J (wd// _ VL _) (ws// _ VTT _) 0 (lti_found LTIM TTS) (wtws'_one _ _ WTDS) (lookupv_found LUVM LIV) PLUS WE % as it turns out, I don't think we need the plus stuff <- plus-zero PLUS EQP <- minus-eq LUVM LTIM EQO <- lookinv-resp EQO LIV LIV' <- ll-findlab S IDX=J TTS LIV' WTDS WE. label-lemma-unwrap : % lt seems unnecessary -- well typedness will ensure % that the label is in range. label-lemma W S J LT (wte_lab LTI : welltyped_exp S (lab L) A (wconst J)) (wtws WTW') LV WE <- plus-commutes p0 POO <- ll-findworld S J W S J LTI WTW' LV POO WE. % same, for continuation labels clabel-lemma : {W : wdlist N} {S : wslist N} {J : nat} J < N -> clabtype_is S L A J -> welltyped_worlds S W -> lookupc W J L K -> welltyped_cont S K A (wconst J) -> type. %mode clabel-lemma +W +S +J +LT +WE +WW +L -WC. cll-findworld : {S : wslist X} {J : nat} % searching through the following two {W' : wdlist N} {S' : wslist N} % for this offset {J' : nat} clabtype_is S' L A J' -> welltyped_worlds' N IDX S S' W' -> lookupc W' J' L K -> % wtw counts up, lookups down. at % every iteration we're getting % closer to (resp. further from) J plus IDX J' J -> welltyped_cont S K A (wconst J) -> type. %mode cll-findworld +S +J +W +S' +J' +CLTI +WTW +LV +PLUS -WK. cll-findlab : % storetype -- result must be wellformed in this {S : wslist X} % the world we're looking in {J : nat} % trace of subscripting type table and value table, resp tt_sub CT OFF A -> lookinc CL OFF K -> % trace of checking the table against its type welltyped_conts S CT CL (wconst J) -> welltyped_cont S K A (wconst J) -> type. %mode cll-findlab +S +J +TTS +LIC +WTC -WK. cllfl-search : cll-findlab S J TTS LIC WTCS WC -> cll-findlab S J (tts_next TTS) (lookinc_next LIC) (wtcs_one WTCS _) WC. cllfl-found : cll-findlab S J tts_found lookinc_found (wtcs_one WTCS WC) WC. cllfw-search : cll-findworld S J WDTL STL J' LTIN WTWTL LUVTL PLUS' WC -> plus-flip PLUS PLUS' -> cll-findworld S J (wd// _ _ WDTL) (ws// _ _ STL) (s J') (clti_next LTIN) (wtws'_one WTWTL _ _) (lookupc_next LUVTL) (PLUS : plus IDX (s J') J) WC. cllfw-found : cll-findworld S IDX=J (wd// CL _ _) (ws// CTT _ _) 0 (clti_found LTIM TTS) (wtws'_one _ WTCS _) (lookupc_found LUVM LIV) PLUS WE % as it turns out, I don't think we need the plus stuff <- plus-zero PLUS EQP <- minus-eq LUVM LTIM EQO <- lookinc-resp EQO LIV LIV' <- cll-findlab S IDX=J TTS LIV' WTCS WE. clabel-lemma-unwrap : % lt seems unnecessary -- well typedness will ensure % that the label is in range. clabel-lemma W S J LT (CLTI : clabtype_is S L A J) (wtws WTW') LV WC <- plus-commutes p0 POO <- cll-findworld S J W S J CLTI WTW' LV POO WC. % % addlabel lemma % % need to know that we have a well-typed network after introducing % a new label. addlabel-lemma : {S : wslist N} {A : typ} {J : nat} J < N -> welltyped_exp S V A (wconst J) -> welltyped_worlds S W -> add_value W J V VP W' L -> % out {S' : wslist N} extends S S' -> labtype_is S' L A J -> welltyped_worlds S' W' -> type. %mode addlabel-lemma +S +A +J +LT +WTE +WTWS +AV -S' -EXT -LTI -WTWS'. % we need to trace the generation of S' to provide breadcrumbs later % the length-j prefix of S and S' is equal, and when we get to the jth % world, we add type A. news-trace : {J : nat} {A : typ} {S : wslist N} {S' : wslist N} type. news-trace-zero : news-trace 0 A (ws// CT BT S) (ws// CT (tt// A BT) S). news-trace-succ : news-trace J A S S' -> news-trace (s J) A (ws// CT BT S) (ws// CT BT S'). all-newstore : % looking through this storetype tail {SL : wslist M} % for this offset {JL : nat} JL < M -> % and will add this type {A : typ} add_value WL JL V VP WL' L -> welltyped_worlds' M IDX S SL WL -> % outputs {SL' : wslist M} extends SL SL' -> labtype_is SL' L A JL -> news-trace JL A SL SL' -> type. %mode all-newstore +SL +JL +LT +A +AV +WT' -SL' -EXT -LTI -NT. allns-miss : all-newstore TTL J LT A AV WT' TTL' E LTI NT -> all-newstore (ws// CT BT TTL) (s J) (lts LT) A (addv_next AV) (wtws'_one WT' _ _) (ws// CT BT TTL') (ex-one E extendst-same extendst-same) (lti_next LTI) (news-trace-succ NT). allns-hit : minus-self SIZE-1 M0 -> ex-id TTL E -> all-newstore (ws// CT BT TTL) 0 lt0 A (addv_found (BD : vlist SIZE-1)) % this just gets us |BT| = |BD| (wtws'_one _ _ _) (ws// CT (tt// A BT) TTL) (ex-one E extendst-same extendst-cons) (lti_found M0 tts_found) news-trace-zero. %worlds (blockm) (all-newstore _ _ _ _ _ _ _ _ _ _). %total JL (all-newstore SL JL LT A AV WT' SL' EXT LTI NT). % after extending a world with a label, the worlds are still well-typed. all-still-wtws : {S : wslist N} {S' : wslist N} {SL : wslist M} {SL' : wslist M} {WL : wdlist M} {WL' : wdlist M} {JL : nat} welltyped_exp S' V A (wconst J) -> welltyped_worlds' M IDX S SL WL -> add_value WL JL V VP WL' L -> extends S S' -> % must know that we haven't changed S except where we did addvalue. news-trace JL A SL SL' -> plus JL IDX J -> extends SL SL' -> welltyped_worlds' M IDX S' SL' WL' -> type. %mode all-still-wtws +S +S' +SL +SL' +WL +WL' +JL +WTE +WT +AV +E +NT +P +EE -WT'. asw-hit : weaken-wtws EXTS WTWS WTWS' -> weaken-wtcs EXTS WTCS WTCS' -> weaken-wtds EXTS WTDS WTDS' -> wte-resp _ _ EQ' WTE WTE' -> eq-refl EQ EQ' -> plus-zero-eq PLUS EQ -> all-still-wtws S S' % nb need to ensure that SL = SL' (ws// CT BT SL) (ws// CT (tt// A BT) SL) (wd// CD BD WL) (wd// CD (v// V VP BD) WL) 0 WTE (wtws'_one WTWS WTCS WTDS) (addv_found BD) EXTS news-trace-zero PLUS (ex-one E extendst-same extendst-cons) (wtws'_one WTWS' WTCS' (wtds_one WTDS' WTE')). asw-skip : weaken-wtds EXTS WTD WTD' -> weaken-wtcs EXTS WTC WTC' -> all-still-wtws S S' SL SL' WL WL' JL WTE WTWS' AV EXTS SF PLUS' E WTW2 -> plus-commutes PLUSR' PLUS' -> plus-flip PLUSR PLUSR' -> plus-commutes PLUS PLUSR -> all-still-wtws S S' (ws// CT BT SL) (ws// CT BT SL') (wd// CD BD WL) (wd// CD BD WL') (s JL) WTE (wtws'_one WTWS' WTC WTD) (addv_next AV) EXTS (news-trace-succ SF) PLUS (ex-one E _ _) (wtws'_one WTW2 WTC' WTD'). %worlds (blockm) (all-still-wtws _ _ _ _ _ _ _ _ _ _ _ _ _ _ _). %total WT (all-still-wtws S S' SL SL' WL WL' JL WTE WT AV E NT P EE WT'). % strategy for addlabel-lemma: first, recurse to create S' and EXT and LTI. % these are the *inputs* to the code that gets WTWS. all-unwrap : all-still-wtws S S' S S' W W' J WTE' WTWS' AV EXT NT p0 EXT WTWS2 -> weaken-wte EXT WTE WTE' -> all-newstore S J LT A AV WTWS' S' EXT LTI NT -> addlabel-lemma S A J LT WTE (wtws WTWS') AV S' EXT LTI (wtws WTWS2). % now cut and paste for addcont-lemma % this is almost exactly the same, except we modify the % continuation table instead of the value table. addcont-lemma : {S : wslist N} {A : typ} {J : nat} J < N -> welltyped_cont S K A (wconst J) -> welltyped_worlds S W -> add_cont W J K W' L -> % out {S' : wslist N} extends S S' -> clabtype_is S' L A J -> welltyped_worlds S' W' -> type. %mode addcont-lemma +S +A +J +LT +WC +WTWS +AC -S' -EX -CLTI -W'. cnews-trace : {J : nat} {A : typ} {S : wslist N} {S' : wslist N} type. cnews-trace-zero : cnews-trace 0 A (ws// CT BT S) (ws// (tt// A CT) BT S). cnews-trace-succ : cnews-trace J A S S' -> cnews-trace (s J) A (ws// CT BT S) (ws// CT BT S'). acl-newstore : % looking through this storetype tail {SL : wslist M} % for this offset {JL : nat} JL < M -> % and will add this type {A : typ} add_cont WL JL K WL' L -> welltyped_worlds' M IDX S SL WL -> % outputs {SL' : wslist M} extends SL SL' -> clabtype_is SL' L A JL -> cnews-trace JL A SL SL' -> type. %mode acl-newstore +SL +JL +LT +A +AV +WT' -SL' -EXT -LTI -NT. aclns-miss : acl-newstore TTL J LT A AC WT' TTL' E LTI NT -> acl-newstore (ws// CT BT TTL) (s J) (lts LT) A (addc_next AC) (wtws'_one WT' _ _) (ws// CT BT TTL') (ex-one E extendst-same extendst-same) (clti_next LTI) (cnews-trace-succ NT). aclns-hit : minus-self SIZE-1 M0 -> ex-id TTL E -> acl-newstore (ws// CT BT TTL) 0 lt0 A (addc_found (CD : clist SIZE-1)) % this just gets us |BT| = |BD| (wtws'_one _ _ _) (ws// (tt// A CT) BT TTL) (ex-one E extendst-cons extendst-same) (clti_found M0 tts_found) cnews-trace-zero. %worlds (blockm) (acl-newstore _ _ _ _ _ _ _ _ _ _). %total JL (acl-newstore SL JL LT A AV WT' SL' EXT LTI NT). % after extending a world with a label, the worlds are still well-typed. acl-still-wtws : {S : wslist N} {S' : wslist N} {SL : wslist M} {SL' : wslist M} {WL : wdlist M} {WL' : wdlist M} {JL : nat} welltyped_cont S' K A (wconst J) -> welltyped_worlds' M IDX S SL WL -> add_cont WL JL K WL' L -> extends S S' -> % must know that we haven't changed S except where we did addvalue. cnews-trace JL A SL SL' -> plus JL IDX J -> extends SL SL' -> welltyped_worlds' M IDX S' SL' WL' -> type. %mode acl-still-wtws +S +S' +SL +SL' +WL +WL' +JL +WTE +WT +AV +E +NT +P +EE -WT'. acsw-hit : weaken-wtws EXTS WTWS WTWS' -> weaken-wtcs EXTS WTCS WTCS' -> weaken-wtds EXTS WTDS WTDS' -> wtc-resp _ _ EQ' WTC WTC' -> eq-refl EQ EQ' -> plus-zero-eq PLUS EQ -> acl-still-wtws S S' % nb need to ensure that SL = SL' (ws// CT BT SL) (ws// (tt// A CT) BT SL) (wd// CD BD WL) (wd// (c// K CD) BD WL) 0 WTC (wtws'_one WTWS WTCS WTDS) (addc_found CD) EXTS cnews-trace-zero PLUS (ex-one E extendst-cons extendst-same) (wtws'_one WTWS' (wtcs_one WTCS' WTC') WTDS'). acsw-skip : weaken-wtds EXTS WTDS WTDS' -> weaken-wtcs EXTS WTCS WTCS' -> acl-still-wtws S S' SL SL' WL WL' JL WTC WTWS' AV EXTS SF PLUS' E WTW2 -> plus-commutes PLUSR' PLUS' -> plus-flip PLUSR PLUSR' -> plus-commutes PLUS PLUSR -> acl-still-wtws S S' (ws// CT BT SL) (ws// CT BT SL') (wd// CD BD WL) (wd// CD BD WL') (s JL) WTC (wtws'_one WTWS' WTCS WTDS) (addc_next AV) EXTS (cnews-trace-succ SF) PLUS (ex-one E _ _) (wtws'_one WTW2 WTCS' WTDS'). %worlds (blockm) (acl-still-wtws _ _ _ _ _ _ _ _ _ _ _ _ _ _ _). %total WT (acl-still-wtws S S' SL SL' WL WL' JL WTE WT AV E NT P EE WT'). acl-unwrap : acl-still-wtws S S' S S' W W' J WTC' WTWS' AC EXT NT p0 EXT WTWS2 -> weaken-wtc EXT WTC WTC' -> acl-newstore S J LT A AC WTWS' S' EXT CLTI NT -> addcont-lemma S A J LT WTC (wtws WTWS') AC S' EXT CLTI (wtws WTWS2). %worlds (blockm) (addlabel-lemma _ _ _ _ _ _ _ _ _ _ _). %total [] (addlabel-lemma _ _ _ _ _ _ _ _ _ _ _). %worlds (blockm) (addcont-lemma _ _ _ _ _ _ _ _ _ _ _). %total [] (addcont-lemma _ _ _ _ _ _ _ _ _ _ _). % if subscripting into the type table worked, then % subscripting into the value table will work. lprog-sub : {VT : typetable (s N3)} {VD : vlist (s N3)} tt_sub VT OFF A -> lookinv VD OFF M VAL -> type. %mode lprog-sub +VT +VD +TTS -LIV. lprog-sub-next : lprog-sub VT' VD' TTS' LIV' -> lprog-sub (tt// _ VT') (v// _ _ VD') (tts_next TTS') (lookinv_next LIV'). lprog-sub-found : lprog-sub (tt// A _) (v// M VAL _) tts_found lookinv_found. %worlds () (lprog-sub _ _ _ _). %total TTS (lprog-sub _ _ TTS _). % similar lemma for progress. % knowing that the label is well-formed, % and that all worlds are well formed, % we just need to know that we can produce % a value label-progress : labtype_is SL L A J -> welltyped_worlds' REST IDX S SL WL -> lookupv WL J L V VP -> type. %mode label-progress +LTI +WT -LUV. label-progress-next : label-progress LTI WTWS LUV -> label-progress (lti_next LTI) (wtws'_one WTWS _ _) (lookupv_next LUV). label-progress-found : lprog-sub VT VD TTS LIV -> label-progress (lti_found (MIN : minus _ _ OFF) TTS) (wtws'_one _ _ (DTS : welltyped_datas S VT VD _)) (lookupv_found MIN LIV). %worlds () (label-progress _ _ _). %total L (label-progress L _ _). % another cut'n'paste job for continuation labels clprog-sub : {CT : typetable (s N3)} {CD : clist (s N3)} tt_sub CT OFF A -> lookinc CD OFF K -> type. %mode clprog-sub +VT +VD +TTS -LIC. clprog-sub-next : clprog-sub CT' CD' TTS' LIC' -> clprog-sub (tt// _ CT') (c// _ CD') (tts_next TTS') (lookinc_next LIC'). clprog-sub-found : clprog-sub (tt// A _) (c// K _) tts_found lookinc_found. %worlds () (clprog-sub _ _ _ _). %total TTS (clprog-sub _ _ TTS _). clabel-progress : clabtype_is SL L A J -> welltyped_worlds' REST IDX S SL WL -> lookupc WL J L K -> type. %mode clabel-progress +CLTI +WT -LUC. clabel-progress-next : clabel-progress CLTI WTWS LUC -> clabel-progress (clti_next CLTI) (wtws'_one WTWS _ _) (lookupc_next LUC). clabel-progress-found : clprog-sub CT CD TTS LIC -> clabel-progress (clti_found (MIN : minus _ _ OFF) TTS) (wtws'_one _ (CTS : welltyped_conts S CT CD _) _) (lookupc_found MIN LIC). %worlds () (clabel-progress _ _ _). %total L (clabel-progress L _ _). % some small lemmas for progress addvalue-progress : {W : wdlist N} {J : nat} J < N -> {V : exp} {VAL : value V} add_value W J V VAL W' L -> type. %mode addvalue-progress +W +J +LT +V +VAL -AV. avp-next : addvalue-progress W' J' LT' V VAL AV' -> addvalue-progress (wd// _ _ W') (s J') (lts LT') V VAL (addv_next AV'). avp-found : addvalue-progress (wd// CD BD _) 0 lt0 V VAL (addv_found BD). %worlds () (addvalue-progress _ _ _ _ _ _). %total J (addvalue-progress _ J _ _ _ _). % ditto, continuations addcont-progress : {W : wdlist N} {J : nat} J < N -> {K : cont} add_cont W J K W' L -> type. %mode addcont-progress +W +J +LT +K -AV. acp-next : addcont-progress W' J' LT' K AC' -> addcont-progress (wd// _ _ W') (s J') (lts LT') K (addc_next AC'). acp-found : addcont-progress (wd// CD BD _) 0 lt0 K (addc_found CD). %worlds () (addcont-progress _ _ _ _ _). %total J (addcont-progress _ J _ _ _). % if we index into a world's continuation table, then it is in bounds. rcont-inbounds : {S : wslist X} clabtype_is S L A J -> J < X -> type. %mode rcont-inbounds +S +C -LT. rci-found : rcont-inbounds _ (clti_found _ _) lt0. rci-next : rcont-inbounds TL CLTI LT -> rcont-inbounds (ws// _ _ TL) (clti_next CLTI) (lts LT). %worlds () (rcont-inbounds _ _ _). %total C (rcont-inbounds _ C _). % or value table... rval-inbounds : {S : wslist X} labtype_is S L A J -> J < X -> type. %mode rval-inbounds +S +C -LT. rvi-found : rval-inbounds _ (lti_found _ _) lt0. rvi-next : rval-inbounds TL LTI LT -> rval-inbounds (ws// _ _ TL) (lti_next LTI) (lts LT). %worlds () (rval-inbounds _ _ _). %total C (rval-inbounds _ C _). % there's no canonical form for bottom % strangely, we need to insert an arbitrary % case to cause the coverage checker to split % on the typing derivation and then decide % all of the cases are impossible. Let's do % rpc ... notval-rpc : value (rpc W M) -> (({N : nat} {NN : network N} {NN' : network N} NN |-> NN')) -> type. %mode notval-rpc +V -F. %worlds () (notval-rpc _ _). %total V (notval-rpc V _). no-cf-bottom : {V : exp} value V -> welltyped_exp S V _|_ W -> ({N : nat} {NN : network N} {NN' : network N} NN |-> NN') -> type. %mode no-cf-bottom +A +B +C -D. ncb-rpc : notval-rpc V FALSE -> no-cf-bottom (rpc _ _) V (wte_rpc _ _) FALSE. %worlds () (no-cf-bottom _ _ _ _). %total C (no-cf-bottom A B C D). %%%% %%%% Theorems. %%%% %%%%% Preservation progress : {NN : network N} wellformed S NN -> (NN |-> NN') -> type. %mode progress +NN +WF -STEP. % cases on evaluating proge-fst : progress (net W C K (eval (fst M))) _ step_pfst. proge-snd : progress (net W C K (eval (snd M))) _ step_psnd. proge-here : progress (net W C K (eval (here M))) _ step_phere. proge-pair1 : progress (net W C K (eval (pair M N))) _ step_ppair. proge-addr : progress (net W C K (eval (addr _ _))) _ step_taddr. proge-lab : label-progress LTI WTWS LUV -> progress (net _ _ _ (eval (lab _))) (wf_net _ _ (wt_eval (wte_lab LTI)) _ (wtws WTWS)) (step_lab LUV). proge-lam : progress (net _ _ _ (eval (lam B))) _ step_tlam. proge-box : progress (net _ _ _ (eval (box B))) _ step_tbox. proge-app : progress (net _ _ _ (eval (app M N))) _ step_papp. proge-unbox : progress (net _ _ _ (eval (unbox M))) _ step_punbox. proge-letdia : progress (net _ _ _ (eval (letdia M N))) _ step_pletdia. proge-letcc : addcont-progress W J LT K AC -> progress (net W J K (eval (letcc M))) (wf_net LT _ _ _ WTWS) (step_rletcc AC). proge-getbox : addcont-progress W J LT K AC -> progress (net W J K (eval (getbox (wconst JNEW) M))) (wf_net LT _ _ _ WTWS) (step_getbox AC). proge-getdia : addcont-progress W J LT K AC -> progress (net W J K (eval (getdia (wconst JNEW) M))) (wf_net LT _ _ _ WTWS) (step_getdia AC). proge-rpc : progress (net W J _ (eval (rpc (wconst JNEW) M))) _ step_rpc. % cases on returning % loop to ourselves progr-done : progress (net W C finish (ret V _)) WF step_done. % impossible case % is there a better way to do this? Unlike the other cases, % twelf can't seem to figure out on its own that there is no % canonical form for bottom progr-abort : no-cf-bottom M V WT RIDICULOUS -> progress (net W J abort (ret M V)) (wf_net _ _|_ (wt_ret WT) wtc_abort _) (RIDICULOUS _ _ (net W J abort (ret M V))). % nb, canonical forms comes free because Twelf is so smart! progr-ffst : progress (net _ _ (ffst K) (ret (pair M1 _) (valpair VAL1 _))) (wf_net _ _ (wt_ret WTP) (wtc_fst _) _) step_rfst. progr-fsnd : progress (net _ _ (fsnd K) (ret (pair _ M2) (valpair _ VAL2))) (wf_net _ _ (wt_ret WTP) (wtc_snd _) _) step_rsnd. progr-fpair1 : progress (net _ _ (fpair1 K M) (ret N NV)) (wf_net _ _ _ _ _) step_fpair. progr-fpair2 : progress (net _ _ (fpair2 K M MV) (ret N NV)) (wf_net _ _ _ _ _) step_rpair. progr-fapp1 : progress (net _ _ (fapp1 K M) (ret N NV)) (wf_net _ _ _ _ _) step_fapp. progr-fapp2 : progress (net _ _ (fapp2 K (lam _) vallam) (ret _ _)) (wf_net _ _ _ _ _) step_rapp. progr-fletdia : progress (net _ _ (fletdia K N) (ret (addr W L) valaddr)) _ step_rletdia. progr-funbox : progress (net _ _ (funbox K) (ret (box M) valbox)) _ step_runbox. progr-rhere : addvalue-progress W J LT V VAL AV -> progress (net W J (fhere K) (ret V VAL)) (wf_net LT _ (wt_ret WTA) _ WTWS) (step_rhere AV). progr-rreturnbox : clabel-progress CLTI WTWS LUC -> progress (net W J (freturnbox JNEW L) (ret (box MB) valbox)) (wf_net LT (! A) (wt_ret (wte_box WTB)) (wtc_freturnbox CLTI) (wtws WTWS)) (step_rreturnbox LUC). progr-rreturndia : clabel-progress CLTI WTWS LUC -> progress (net W J (freturndia JNEW L) (ret (addr _ _) valaddr)) (wf_net LT (? A) (wt_ret (wte_addr _)) (wtc_freturndia CLTI) (wtws WTWS)) (step_rreturndia LUC). proge-throw : clabel-progress CLTI WTWS LUC -> progress (net W J _ (eval (throw M (caddr (wconst JNEW) L)))) (wf_net LT _ (wt_eval (wte_throw (wtce_caddr CLTI) WE)) _ (wtws WTWS)) (step_throw LUC). %%%%% Preservation preservation : {NN : network N} {S : wslist N} wellformed S NN -> (NN |-> NN') -> {S' : wslist N} extends S S' -> wellformed S' NN' -> type. %mode preservation +NN +S +WF +STEP -S' -E -WF'. % by induction on step relation |-> presv-done : ex-id S E -> preservation _ S WF step_done S E WF. presv-pfst : ex-id S E -> preservation _ S (wf_net LT A (wt_eval (wte_fst WE)) WC WTWS) step_pfst S E (wf_net LT (A & B) (wt_eval WE) (wtc_fst WC) WTWS). presv-psnd : ex-id S E -> preservation _ S (wf_net LT B (wt_eval (wte_snd WE)) WC WTWS) step_psnd S E (wf_net LT (A & B) (wt_eval WE) (wtc_snd WC) WTWS). presv-rfst : ex-id S E -> preservation _ S (wf_net LT (A & _) (wt_ret (wte_pair WEA _)) (wtc_fst WC) WTWS) step_rfst S E (wf_net LT A (wt_ret WEA) WC WTWS). presv-rsnd : ex-id S E -> preservation _ S (wf_net LT (_ & B) (wt_ret (wte_pair _ WEB)) (wtc_snd WC) WTWS) step_rsnd S E (wf_net LT B (wt_ret WEB) WC WTWS). presv-phere : ex-id S E -> preservation _ S (wf_net LT (? A) (wt_eval (wte_here WH)) WC WTWS) step_phere S E (wf_net LT A (wt_eval WH) (wtc_here WC) WTWS). presv-ppair : ex-id S E -> preservation _ S (wf_net LT (A & B) (wt_eval (wte_pair WA WB)) WC WTWS) step_ppair S E (wf_net LT A (wt_eval WA) (wtc_pair1 WB WC) WTWS). presv-fpair : ex-id S E -> preservation _ S (wf_net LT A (wt_ret WA) (wtc_pair1 WB WC) WTWS) step_fpair S E (wf_net LT B (wt_eval WB) (wtc_pair2 WA WC) WTWS). presv-fapp : ex-id S E -> preservation _ S (wf_net LT _ (wt_ret WF) (wtc_app1 WB WC) WTWS) step_fapp S E (wf_net LT A (wt_eval WB) (wtc_app2 WF WC) WTWS). presv-rpair : ex-id S E -> preservation _ S (wf_net LT B (wt_ret WB) (wtc_pair2 WA WK) WTWS) step_rpair S E (wf_net LT (A & B) (wt_ret (wte_pair WA WB)) WK WTWS). % this case is a bit more complex because we have our own substitution % theorem; see wwte-lam presv-rapp : ex-id S E -> wte-subst WA WF WS -> preservation _ S (wf_net LT A (wt_ret WA) (wtc_app2 (wte_lam WF) WC) WTWS) step_rapp S E (wf_net LT B (wt_eval WS) WC WTWS). % same here, but even worse because we have to substitute for the expression % and the world presv-rletdia : ex-id S E -> wte-subst (wte_lab LTI) WN' WE' -> % blockm ({m:exp} {wt : {X : nat} {SS : wslist X} welltyped_exp SS m A (wconst JOTHER)} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {ex : extends s s'} weaken-wte ex (wt Y s) (wt Y s')} wte-wsubst JOTHER LTOTHER ([wwt] WN (wconst JOTHER) wwt m wt) (WN' m wt)) -> rval-inbounds S LTI LTOTHER -> preservation (net W J (fletdia K N) (ret (addr (wconst JOTHER) L) valaddr)) S (wf_net LT (? A) (wt_ret (wte_addr LTI)) (wtc_letdia WC WN) WTWS) step_rletdia S E (wf_net LT C (wt_eval WE') WC WTWS). presv-runbox : ex-id S E -> wte-wsubst J LT (WB (wconst J)) WB' -> preservation _ S (wf_net LT (! A) (wt_ret (wte_box WB)) (wtc_unbox WC) WTWS) step_runbox S E (wf_net LT A (wt_eval WB') WC WTWS). presv-tlam : ex-id S E -> preservation _ S (wf_net LT (A => B) (wt_eval WA) WC WTWS) step_tlam S E (wf_net LT (A => B) (wt_ret WA) WC WTWS). presv-tbox : ex-id S E -> preservation _ S (wf_net LT (! A) (wt_eval WA) WC WTWS) step_tbox S E (wf_net LT (! A) (wt_ret WA) WC WTWS). presv-taddr : ex-id S E -> preservation _ S (wf_net LT (? A) (wt_eval WA) WC WTWS) step_taddr S E (wf_net LT (? A) (wt_ret WA) WC WTWS). presv-papp : ex-id S E -> preservation _ S (wf_net LT B (wt_eval (wte_app WF WB)) WC WTWS) step_papp S E (wf_net LT (A => B) (wt_eval WF) (wtc_app1 WB WC) WTWS). presv-punbox : ex-id S E -> preservation _ S (wf_net LT A (wt_eval (wte_unbox WB)) WC WTWS) step_punbox S E (wf_net LT (! A) (wt_eval WB) (wtc_unbox WC) WTWS). presv-pletdia : ex-id S E -> preservation _ S (wf_net LT C (wt_eval (wte_letdia WM WN)) WC WTWS) step_pletdia S E (wf_net LT (? A) (wt_eval WM) (wtc_letdia WC WN) WTWS). presv-rhere : % insertion preserves and creates all sorts of stuff weaken-wtc EXT WC WC' -> addlabel-lemma S A _ LT WTE WTWS AV S' EXT LTI WTWS' -> preservation _ S (wf_net LT A (wt_ret WTE) (wtc_here WC) WTWS) (step_rhere AV) S' EXT (wf_net LT (? A) (wt_ret (wte_addr LTI)) WC' WTWS'). presv-lab : % lookup preserves type label-lemma W S J LT WE WTWS LUV WEL -> ex-id S E -> preservation _ S (wf_net LT A (wt_eval WE) WTC WTWS) (step_lab LUV) S E (wf_net LT A (wt_ret WEL) WTC WTWS). presv-rreturnbox : clabel-lemma W S J LTNEW CLTI WTWS LUC WTC -> rcont-inbounds S CLTI LTNEW -> ex-id S E -> preservation _ S (wf_net LT (! A) (wt_ret (wte_box WB)) (wtc_freturnbox CLTI) WTWS) (step_rreturnbox LUC) S E (wf_net LTNEW (! A) (wt_ret (wte_box WB)) WTC WTWS). presv-rreturndia : clabel-lemma W S J LTNEW CLTI WTWS LUC WTC -> rcont-inbounds S CLTI LTNEW -> ex-id S E -> preservation _ S (wf_net LT (? A) (wt_ret (wte_addr ALTI)) (wtc_freturndia CLTI) WTWS) (step_rreturndia LUC) S E (wf_net LTNEW (? A) (wt_ret (wte_addr ALTI)) WTC WTWS). % throw is rather like the above presv-throw : clabel-lemma W S JNEW LTNEW CLTI (wtws WTWS) LUC WTC -> rcont-inbounds S CLTI LTNEW -> ex-id S E -> preservation (net W JOLD _ (eval (throw M (caddr (wconst JNEW) L)))) S (wf_net LT _ (wt_eval (wte_throw (wtce_caddr CLTI) WE)) _ (wtws WTWS)) (step_throw LUC) S E (wf_net LTNEW _ (wt_eval WE) WTC (wtws WTWS)). % addition of continuation label preserves stuff presv-rletcc : wte-csubst (wtce_caddr CLTI) WTBOD' WTS -> ({c:cexp} {wt : {n:nat} {s1:wslist n} welltyped_cexp s1 c A _} {thm : {Y : nat} {s : wslist Y} {s' : wslist Y} {EX : extends s s'} weaken-wtce EX (wt Y s) (wt Y s')} weaken-wte EXT (WTBODY c wt) (WTBOD' c wt)) -> weaken-wtc EXT WC WC' -> addcont-lemma S A _ LT WC WTWS AC S' EXT CLTI WTWS' -> preservation _ S (wf_net LT A (wt_eval (wte_letcc WTBODY)) WC WTWS) (step_rletcc AC) S' EXT (wf_net LT A (wt_eval WTS) WC' WTWS'). presv-rpc : ex-id S EXT -> preservation _ S (wf_net LT _|_ (wt_eval (wte_rpc (wtw_const _ LTNEW) WT)) _ WTWS) step_rpc S EXT (wf_net LTNEW _|_ (wt_eval WT) wtc_abort WTWS). presv-getbox : weaken-wte EXT WT WT' -> addcont-lemma S (! A) _ LT WC WTWS AC S' EXT CLTI WTWS' -> preservation _ S (wf_net LT (! A) (wt_eval (wte_getbox (wtw_const _ LTNEW) WT)) WC WTWS) (step_getbox AC) S' EXT (wf_net LTNEW (! A) (wt_eval WT') (wtc_freturnbox CLTI) WTWS'). presv-getdia : weaken-wte EXT WT WT' -> addcont-lemma S (? A) _ LT WC WTWS AC S' EXT CLTI WTWS' -> preservation _ S (wf_net LT (? A) (wt_eval (wte_getdia (wtw_const _ LTNEW) WT)) WC WTWS) (step_getdia AC) S' EXT (wf_net LTNEW (? A) (wt_eval WT') (wtc_freturndia CLTI) WTWS'). %%%% %%%% Check lemmas and theorems. %%%% %worlds (blockm) (ll-findlab S J TTS LIV WTD WE) (ll-findworld S J W' S' J' LTI WTW LV PLUS WE) (label-lemma W S J LT WE WW L WV) (cll-findlab _ _ _ _ _ _) (cll-findworld _ _ _ _ _ _ _ _ _ _) (clabel-lemma _ _ _ _ _ _ _ _). %total [TTS LIV WTD] (ll-findlab S J TTS LIV WTD WE). %total [W' S' J' LTI WTW LV] (ll-findworld S J W' S' J' LTI WTW LV PLUS WE). %total [WE WW] (label-lemma W S J LT WE WW L WV). %total [TTS LIV WTD] (cll-findlab S J TTS LIV WTD WE). %total [W' S' J' LTI WTW LV] (cll-findworld S J W' S' J' LTI WTW LV PLUS WE). %total [WE WW] (clabel-lemma W S J LT WE WW L WV). % the key type safety results %worlds (blockm) (preservation NN S WF STEP S E WF). %total [STEP] (preservation _ _ _ STEP _ _ _). %worlds () (progress NN WF STEP). %total [NN WF] (progress NN WF STEP).