% Safety of yield. % Joint work with Chung-chieh Shan. % $Id: yield.elf 2811 2007-11-02 04:07:28Z oleg $ % % Monadic System F. nat: type. %name nat N. 0: nat. 1: nat -> nat. %prefix 200 1. %abbrev ilv = nat. % interrupt disability level. % 0 means interrupts are enabled, % positive values: nested disabled states % Types tp : type. %name tp T. int : tp. % only one base type => : tp -> tp -> tp. %infix right 10 =>. all : (tp -> tp) -> tp. m : ilv -> tp -> tp. % monad marked with the disabling level % Expressions exp : type. %name exp E. n : nat -> exp. %prefix 110 n. % Standard System F stuff lam : tp -> (exp -> exp) -> exp. @ : exp -> exp -> exp. %infix left 100 @. tlam : (tp -> exp) -> exp. tapp : exp -> tp -> exp. % Monadic meta-language ret : exp -> exp. do : exp -> (exp -> exp) -> exp. >> = [e1] [e2] do e1 ([_] e2). %infix left 10 >>. % Interrupts-related disable : exp -> exp. yield : exp. % Type system of : exp -> tp -> type. %name of P. %mode of +E *T. tp-n : of (n _) int. tp-lam : of (lam T1 E) (T1 => T2) <- {x:exp} of x T1 -> of (E x) T2. tp-app : of (E1 @ E2) T2 <- of E2 T1 <- of E1 (T1 => T2). tp-tlam : of (tlam E) (all T) <- {t:tp} of (E t) (T t). tp-tapp : of (tapp E T1) (T T1) <- of E (all T). tp-ret : of (ret E) (m N T) <- of E T. tp-do : of (do E1 E2F) (m N T) <- of E1 (m N T1) <- {x:exp} of x T1 -> of (E2F x) (m N T). % the following should have the value type of unit, % but we have only int as the base type. % The assigned types, actually, interrupt levels, % assure safety. tp-di : of (disable E) (m N T) <- of E (m (1 N) T). tp-yi : of yield (m 0 int). %block bl-ev : some {T:tp} block {x:exp} {u:of x T}. %block bl-tv : block {t:tp}. %worlds (bl-ev | bl-tv) (of _ _). %terminates E (of E T). %covers of +E *T. % Sample expressions (see yield.hs) % in_disabled in yield.hs in-dis = tlam [t] lam (m N t) [e] (lam T [a] a >> e >> ret n 0) @ (ret n (1 0)). in-dis1 = tlam [t] lam (m N t) [e] (lam T [a] a >> e >> yield >> ret n 0) @ (ret n (1 0)). t1 = ret n 0 >> yield >> disable ((tapp in-dis int) @ (ret n 0)) >> yield. % expected type error t11 = ret n 0 >> yield >> disable ((tapp in-dis int) @ yield) >> yield. % expected type error t12 = ret n 0 >> yield >> disable ((tapp in-dis1 int) @ (ret n 0)) >> yield. % test3 of yield.hs: recursive disabling t3 = ret n 0 >> yield >> disable (disable ((tapp in-dis int) @ (disable (ret n 0)))) >> yield. t31 = ret n 0 >> yield >> disable (disable ((tapp in-dis int) @ (disable yield))) >> yield. t32 = ret n 0 >> yield >> disable (disable ((tapp in-dis int) @ (disable (ret n 0))) >> yield) >> yield. %query 1 2 of in-dis R. % this shows in-dis1 must be used at level 0 only %query 1 2 of in-dis1 (all ([t:tp] m 0 t => m 0 int)). %query 1 2 of t1 (m 0 int). % should be a type error %query 0 2 of t11 R. %query 0 2 of t12 R. %query 1 2 of t3 (m 0 int). %query 0 2 of t31 R. %query 0 2 of t32 R. % Dynamic semantics % All types are disregarded here. % Our semantics is essentially small step, but with an implicit context. % we implicitly keep focusing until we hit a redex. Note that our semantics % is deterministic, unlike some other formalizations in Twelf. % We are thus sure that a nonsensical expression shall get stuck rather % that loop forever. % A big-step semantics can't be handled in Twelf meta-theoretically: % one can't prove progress because how to build an infinite eval % derivation? We have to do co-inductively, that is, small-step. % The examples of mini-ml or lambda-calculuator in the Twelf distribution % do show the big step semantics -- but no progress proofs. Not even % the mentioning of progress. Quite understandably... % some expressions are values (with respect to simplification) val : exp -> type. %mode val +E. val-n : val (n N). val-l : val (lam _ EF). val-L : val (tlam EF). val-r : val (ret E). val-d : val (do E EF). val-D : val (disable E). val-y : val yield. %worlds () (val _). % simplification: operates on pure values. It is CBN, reductions are % permitted in any order. % simplify operates only on non-values. simplify : exp -> exp -> type. %name simplify S. %mode simplify +E1 -E2. si-@ : simplify ((lam _ EF) @ E2) (EF E2). % CBN si-@1 : simplify (E1 @ E2) (E1' @ E2) <- simplify E1 E1'. si-A : simplify (tapp (tlam EF) T) (EF T). si-A1 : simplify (tapp E1 T) (tapp E1' T) <- simplify E1 E1'. %worlds () (simplify _ _). % Cover should not hold: we should get stuck on non-sensical expressions: % %covers simplify +E1 -E2. % simplify preserves types %{ %theorem simp-tpp : forall* {E:exp} {E':exp} {T:tp} forall {D:simplify E E'} {P:of E T} exists {Q:of E' T} true. %prove 6 D (simp-tpp D _ _). }% % Alas, we have to prove type preservation manually as we need it % for execution simp-tp : simplify E E' -> of E T -> of E' T -> type. %mode simp-tp +PS +PTI -PTO. -: simp-tp si-@ (tp-app (tp-lam PH) PTE2) (PH _ PTE2). -: simp-tp (si-@1 PSE1) (tp-app PTE1 PTE2) (tp-app PTE1' PTE2) <- simp-tp PSE1 PTE1 PTE1'. -: simp-tp (si-A:simplify (tapp _ T) _) (tp-tapp (tp-tlam PH)) (PH T). -: simp-tp (si-A1 PSE1) (tp-tapp PTE1) (tp-tapp PTE1') <- simp-tp PSE1 PTE1 PTE1'. %worlds () (simp-tp _ _ _). %total {PS} (simp-tp PS _ _). % executions: reduces configurations. Big-step semantics. % The configuration includes the command and the interrupt level cnF : ilv -> exp -> type. %name cnF F. cnf : {N:ilv} {E:exp} cnF N E. execable : exp -> type. %mode execable +E. exa-d: execable (do E1 EF). exa-D: execable (disable E). exa-y: execable yield. %worlds () (execable _). exec : cnF N E -> cnF N E' -> type. %mode exec +FI -FO. % administrative redexes ex-s : exec (cnf N E) (cnf N E') <- simplify E E'. ex-r : exec (cnf N (ret E)) (cnf N (ret E)). ex-ds : exec (cnf N (do E EF)) (cnf N (do E' EF)) <- simplify E E'. ex-dr : exec (cnf N (do (ret E) EF)) (cnf N (EF E)). ex-de : exec (cnf N (do E EF)) (cnf N (do E1' EF)) <- execable E <- exec (cnf N E) (cnf N E1'). % interrupt-related ex-Ds : exec (cnf N (disable E)) (cnf N (disable E')) <- simplify E E'. ex-Dr : exec (cnf N (disable (ret E))) (cnf N (ret E)). ex-De : exec (cnf N (disable E)) (cnf N (disable E')) <- execable E <- exec (cnf (1 N) E) (cnf (1 N) E'). % yield can only work at level 0 ex-y : exec (cnf 0 yield) (cnf 0 (ret (n 0))). %worlds () (exec _ _). % the cover should fail: we can get stuck! % but now it is not obvious to Twelf: we can get stuck because simplify % is partial... %covers exec +F1 -F2. % Just to be able to run the examples... exec* : cnF N E -> cnF N E' -> type. %mode exec* +F1 -F2. - : exec* (cnf 0 (ret E)) (cnf 0 (ret E)). - : exec* F1 R <- exec F1 F2 <- exec* F2 R. %query 1 1 exec (cnf 0 yield) R. %query 1 1 exec* (cnf 0 (ret n 0 >> yield >> yield)) R. %query 1 1 exec* (cnf 0 (disable (ret n 0))) R. % should get stuck... %query 0 1 exec* (cnf 0 (disable (ret n 0 >> yield))) R. %query 1 1 exec* (cnf 0 t1) (cnf 0 (ret (n 0))). % should get stuck %query 0 1 exec* (cnf 0 t11) R. %query 0 1 exec* (cnf 0 t12) R. %query 1 1 exec* (cnf 0 t3) (cnf 0 (ret (n 0))). % should get stuck %query 0 1 exec* (cnf 0 t31) R. %query 0 1 exec* (cnf 0 t32) R. % execution is type-preserving %{ % it seems Twelf can't prove it automatically %theorem exec-tpp : forall* {E:exp} {E':exp} {F:cnF E} {F':cnF E'} {T:tp} forall {D:exec F F'} {P:of E T} exists {Q:of E' T} true. %prove 6 D (exec-tpp D _ _). }% exec-tp : exec (_:cnF N E) (_:cnF N E') -> of E T -> of E' T -> type. %mode exec-tp +D1 +PTI -PTO. - : exec-tp (ex-s PS) PT PT' <- simp-tp PS PT PT'. - : exec-tp ex-r PT PT. - : exec-tp (ex-ds PS) (tp-do PTF PTE1) (tp-do PTF PTE1') <- simp-tp PS PTE1 PTE1'. - : exec-tp ex-dr (tp-do PTF (tp-ret PTE)) (PTF _ PTE). - : exec-tp (ex-de PX PXA) (tp-do PTF PTE1) (tp-do PTF PTE1') <- exec-tp PX PTE1 PTE1'. - : exec-tp (ex-Ds PS) (tp-di PT) (tp-di PT') <- simp-tp PS PT PT'. - : exec-tp ex-Dr (tp-di (tp-ret PT)) (tp-ret PT). - : exec-tp (ex-De PX PXA) (tp-di PT) (tp-di PT') <- exec-tp PX PT PT'. - : exec-tp ex-y _ (tp-ret tp-n). %worlds () (exec-tp _ _ _). %total {PE} (exec-tp PE _ _). % proving progress. Have to do it manually % First prove that if app and tapp have types, they can be % simplified simp-prog-app : of (E1 @ E2) T -> simplify (E1 @ E2) ER -> type. simp-prog-tapp : of (tapp E1 T1) T -> simplify (tapp E1 T1) ER -> type. %mode simp-prog-app +PT -PS. %mode simp-prog-tapp +PT -PS. - : simp-prog-app (tp-app (tp-lam PH) PTE2) si-@. - : simp-prog-app (tp-app (tp-app PTE11 PTE12) PTE2) (si-@1 PS) <- simp-prog-app (tp-app PTE11 PTE12) PS. - : simp-prog-app (tp-app (PTE1:of (tapp E TX) (T1 => T2)) PTE2) (si-@1 PS) <- simp-prog-tapp PTE1 PS. - : simp-prog-tapp (tp-tapp (tp-tlam PH)) si-A. - : simp-prog-tapp (tp-tapp (tp-app PTE11 PTE12)) (si-A1 PS) <- simp-prog-app (tp-app PTE11 PTE12) PS. - : simp-prog-tapp (tp-tapp (PTE1:of (tapp E TX) _)) (si-A1 PS) <- simp-prog-tapp PTE1 PS. %worlds () (simp-prog-tapp _ _) (simp-prog-app _ _). %terminates (PT PT1) (simp-prog-tapp PT _) (simp-prog-app PT1 _). %total (PT PT1) (simp-prog-tapp PT _) (simp-prog-app PT1 _). % Proof of the main theorem: if an expression has a monadic type, % it can be executed at some disability level. exec-prog : of E (m N T) -> exec (_:cnF N E) (_:cnF N E') -> type. %mode exec-prog +PT -PE. - : exec-prog (PT:of (E1 @ E2) (m N T)) (ex-s PS) <- simp-prog-app PT PS. - : exec-prog (PT:of (tapp E1 T1) (m N T)) (ex-s PS) <- simp-prog-tapp PT PS. - : exec-prog (tp-ret _) ex-r. - : exec-prog (tp-do _ (PT:of (E1 @ E2) _)) (ex-ds PS) <- simp-prog-app PT PS. - : exec-prog (tp-do _ (PT:of (tapp E1 T1) _)) (ex-ds PS) <- simp-prog-tapp PT PS. - : exec-prog (tp-do _ (tp-ret _)) ex-dr. - : exec-prog (tp-do _ (PT:of (do _ _) _)) (ex-de PX exa-d) <- exec-prog PT PX. - : exec-prog (tp-do _ (PT:of (disable _) _)) (ex-de PX exa-D) <- exec-prog PT PX. - : exec-prog (tp-do _ tp-yi) (ex-de PX exa-y) <- exec-prog tp-yi PX. - : exec-prog (tp-di (PT:of (E1 @ E2) _)) (ex-Ds PS) <- simp-prog-app PT PS. - : exec-prog (tp-di (PT:of (tapp E1 T1) _)) (ex-Ds PS) <- simp-prog-tapp PT PS. - : exec-prog (tp-di (tp-ret _)) ex-Dr. - : exec-prog (tp-di (PT:of (do _ _) _)) (ex-De PX exa-d) <- exec-prog PT PX. - : exec-prog (tp-di (PT:of (disable _) _)) (ex-De PX exa-D) <- exec-prog PT PX. - : exec-prog tp-yi ex-y. %worlds () (exec-prog _ _). %total {PT} (exec-prog PT _). % If we make a delibreate mistake in the typing derivation: % tp-yi : of yield (m N int). % That is, put N instead of 0, and thus make yield type at any level, % the proof of the main theorem fails, with a coverage error % {E1:exp} {F1:cnF 0 (disable yield)} {F2:cnF 0 E1} {X1:exec F1 F2} % |- exec-prog (tp-di tp-yi) X1, % {N1:nat} {E1:exp} {F1:cnF (1 N1) (disable yield)} {F2:cnF (1 N1) E1} % {X1:exec F1 F2} % |- exec-prog (tp-di tp-yi) X1, % {N1:nat} {E1:exp} {F1:cnF (1 N1) yield} {F2:cnF (1 N1) E1} {X1:exec F1 F2} % |- exec-prog tp-yi X1. % we proved the soundness!