% Safety of arrays and binary search % % Proving soundness of the `strict' type system for % the language made of System F plus `arrays' whose type reflects % their size. Arrays are modeled as lists, array indexing starts at 1. % The progress theorem below assures the safety property: % a well-typed program shall not attempt to access an out-of-bounds % element of an array. % This is a joint work with Chung-chieh Shan. % For the context, please see % http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html % ---------------------------------------------------------------------- % Some properties of naturals. nat : type. %name nat X. z : nat. s : nat -> nat. half : nat -> nat -> type. % compute floor(a/2) %mode half +N1 -N2. half_0 : half z z. half_1 : half (s z) z. half_2 : half (s (s N1)) (s N2) <- half N1 N2. %worlds () (half _ _). %total N1 (half N1 N2). halve : {N1:nat} {N2:nat} half N1 N2 -> type. % compute the proof of the former %mode halve +N1 -N2 -H. - : halve _ _ half_0. - : halve _ _ half_1. - : halve _ _ (half_2 H) <- halve _ _ H. %worlds () (halve _ _ _). %total N1 (halve N1 N2 _). mid : nat -> nat -> nat -> type. % (a+b)/2 %mode mid +N1 +N2 -N3. mid_z : mid z N2 N3 <- half N2 N3. mid_s_z : mid (s N1) z N3 <- half (s N1) N3. mid_s_s : mid (s N1) (s N2) (s N3) <- mid N1 N2 N3. %worlds () (mid _ _ _). %total {N1 N2} (mid N1 N2 N3). middle : {N1:nat} {N2:nat} {N3:nat} mid N1 N2 N3 -> type. %mode middle +N1 +N2 -N3 -M. - : middle _ _ _ (mid_z H) <- halve _ _ H. - : middle _ _ _ (mid_s_z H) <- halve _ _ H. - : middle _ _ _ (mid_s_s M) <- middle _ _ _ M. %worlds () (middle _ _ _ _). %total {N1 N2} (middle N1 N2 N3 M). leq : nat -> nat -> type. % check if a <= b %mode leq +N1 *N2. leq1 : leq z N. leq2 : leq (s N1) (s N2) <- leq N1 N2. leq_s_z = leq2 leq1. %worlds () (leq _ _). %terminates N1 (leq N1 N2). leq_refl : {N:nat} leq N N -> type. % prove that forall n. n <= n %mode leq_refl +N -P. leq_refl_z : leq_refl z leq1. leq_refl_s : leq_refl (s N) (leq2 P) <- leq_refl N P. %worlds () (leq_refl _ _). %total N (leq_refl N _). leq_succ : leq N1 N2 -> leq N1 (s N2) -> type. % n1 <= n2 ==> n1 <= (n2+1) %mode leq_succ +P -Q. leq_succ_z : leq_succ leq1 leq1. leq_succ_s : leq_succ (leq2 P) (leq2 Q) <- leq_succ P Q. %worlds () (leq_succ _ _). %total P (leq_succ P _). % Prove that leq establishes the total order on nat leq-gt : nat -> nat -> type. leq-gt_leq : leq N1 N2 -> leq-gt N1 N2. leq-gt_gt : leq (s N2) N1 -> leq-gt N1 N2. leq-proof-lemma : leq-gt N1 N2 -> leq-gt (s N1) (s N2) -> type. %mode leq-proof-lemma +M -M'. - : leq-proof-lemma (leq-gt_leq P) (leq-gt_leq (leq2 P)). - : leq-proof-lemma (leq-gt_gt P) (leq-gt_gt (leq2 P)). %worlds () (leq-proof-lemma _ _). %total {} (leq-proof-lemma _ _). leq-proof : {N1:nat} {N2:nat} leq-gt N1 N2 -> type. %mode leq-proof +N1 +N2 -M. - : leq-proof z _ (leq-gt_leq leq1). - : leq-proof (s _) z (leq-gt_gt leq_s_z). - : leq-proof (s N1) (s N2) M' <- leq-proof N1 N2 M <- leq-proof-lemma M M'. %worlds () (leq-proof _ _ _). %terminates {N1 N2} (leq-proof N1 N2 _). %total {N1 N2} (leq-proof N1 N2 _). % The following lemmas and theorems prove that if two indexes are within % bounds [a..b], then their middle is within the same bounds. %theorem leq_mid : % Ask Twelf to find the prove forall* {N:nat} {N1:nat} {N2:nat} {N3:nat} forall {P1:leq N N1} {P2:leq N N2} {P:mid N1 N2 N3} exists {Q:leq N N3} true. %prove 3 {P1 P2 P} (leq_mid P1 P2 P _). % Now do the same proof by hand, because % automatically found proofs cannot (yet) % be used in manual proofs. leq_half : leq N N2 -> half N N' -> leq N' N2 -> type. %mode leq_half +P +PH -Q. leq_half_z : leq_half (leq1) (half_0) (leq1). leq_half_s_z : leq_half (leq2 leq1) (half_1) (leq1). leq_half_s_s : leq_half (leq2 (leq2 P)) (half_2 PH) (leq2 Q) <- leq_half P PH Q1 <- leq_succ Q1 Q. %{ %theorem leq_half : forall* {N:nat} {N':nat} {N2:nat} forall {P:leq N N2} {PH:half N N'} exists {Q:leq N' N2} true. %prove 3 {P PH} (leq_half P PH _). }% %worlds () (leq_half _ _ _). %total P (leq_half P _ _). mid_leq : leq N1 N -> leq N2 N -> mid N1 N2 N3 -> leq N3 N -> type. %mode mid_leq +P1 +P2 +P -Q. mid_leq_z : mid_leq leq1 P2 (mid_z PH) Q <- leq_half P2 PH Q. mid_leq_s_z : mid_leq P1 leq1 (mid_s_z PH) Q <- leq_half P1 PH Q. mid_leq_s_s : mid_leq (leq2 P1) (leq2 P2) (mid_s_s PM) (leq2 Q) <- mid_leq P1 P2 PM Q. %{ %theorem mid_leq : forall* {N:nat} {N1:nat} {N2:nat} {N3:nat} forall {P1:leq N1 N} {P2:leq N2 N} {P:mid N1 N2 N3} exists {Q:leq N3 N} true. %prove 3 {P1 P2 P} (mid_leq P1 P2 P _). }% %worlds () (mid_leq _ _ _ _). %total P (mid_leq P1 P2 P _). leq_trans : leq N1 N2 -> leq N2 N3 -> leq N1 N3 -> type. %mode leq_trans +P1 +P2 -Q. leq_trans_z : leq_trans leq1 _ leq1. leq_trans_s : leq_trans (leq2 P1) (leq2 P2) (leq2 Q) <- leq_trans P1 P2 Q. %{ %theorem leq_trans : forall* {N1:nat} {N2:nat} {N3:nat} forall {P1:leq N1 N2} {P2:leq N2 N3} exists {Q:leq N1 N3} true. %prove 3 [P1 P2] (leq_trans P1 P2 _). }% %worlds () (leq_trans _ _ _). %total P1 (leq_trans P1 P2 _). % ---------------------------------------------------------------------- % Introducing our language % Types and type constructors tp : type. %name tp T. => : tp -> tp -> tp. %infix right 10 =>. all : (tp -> tp) -> tp. list : tp -> tp. % we represent a *one-based* array as a list tnum : nat -> tp. % Type-level numerals tint : tp. barray : tp -> tp -> tp. bindex : tp -> tp. bindexL : tp -> tp. bindexH : tp -> tp. % value constructors and constants: the term language exp : type. %name exp E. lam : (exp -> exp) -> exp. app : exp -> exp -> exp. tlam : (tp -> exp) -> exp. tapp : exp -> tp -> exp. % We model arrays as lists here. The follwoing are the two data constructors nil : exp. cons : exp -> exp -> exp. int : nat -> exp. % literal (non-negative) integers % --- security kernel % data constructors barrayV : exp -> exp. bindexV : nat -> exp. bindexLV : nat -> exp. bindexHV : nat -> exp. % functions brand : exp -> exp -> exp. bmiddle : exp -> exp -> exp. index_cmp : exp -> exp -> exp -> exp -> exp. bsucc : exp -> exp. bpred : exp -> exp. bget : exp -> exp -> exp. unbi : exp -> exp. llen : exp -> nat -> type. % list length %mode llen +L -N. llen1 : llen (nil) z. llen2 : llen (cons E R) (s N) <- llen R N. % %worlds () (llen _ _). % to be defined later % %terminates L (llen L N). % ---------------------------------------------------------------------- % Static semantics: type checking of : exp -> tp -> type. %name of P. %mode of +E *T. tp_lam : of (lam E) (T1 => T2) <- {x:exp} of x T1 -> of (E x) T2. tp_app : of (app E1 E2) T2 <- of E1 (T1 => T2) <- of E2 T1. 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_nil : of (nil) (list T). tp_cons : of (cons E1 E2) (list T) <- of E1 T <- of E2 (list T). tp_int : of (int _) tint. tp_unbi : of (unbi E) tint <- of E (bindex TS). tp_get : of (bget EA EI) TA <- of EA (barray TS TA) <- of EI (bindex TS). tp_bsucc : of (bsucc E) (bindexL TS) <- of E (bindex TS). tp_bpred : of (bpred E) (bindexH TS) <- of E (bindex TS). tp_bmiddle : of (bmiddle EI1 EI2) (bindex TS) <- of EI1 (bindex TS) <- of EI2 (bindex TS). tp_icmp : of (index_cmp EI1 EI2 EGK ELK) TW <- of EI1 (bindexL TS) <- of EI2 (bindexH TS) <- of EGK TW <- of ELK ((bindex TS) => (bindex TS) => TW). tp_brand : of (brand EA EK) TW <- of EA (list TA) <- of EK (all ([ts] ((barray ts TA) => (bindexL ts) => (bindexH ts) => TW))). % security properties, via special typing rules. % bindexV t i holds if 1 <= i <= repr t tp_bindex : of (bindexV N) (bindex (tnum TS)) <- leq N TS <- leq (s z) N. % an integer >=1 tp_bindexL : of (bindexLV (s _)) (bindexL (tnum TS)). % bindexHV t i holds if i <= repr t tp_bindexH : of (bindexHV N) (bindexH (tnum TS)) <- leq N TS. % value of type |(s,'a) barray| is an array of the length~\$n\$ % We could've required "val EL". tp_barrayV : of (barrayV EL) (barray (tnum TS) TA) <- of EL (list TA) <- llen EL TS. %block tp_var : some {T:tp} block {x:exp} {u:of x T}. %block tp_tvar : block {t:tp}. %worlds (tp_var | tp_tvar) (llen _ _). %worlds (tp_var | tp_tvar) (of E T). %terminates L (llen L N). %terminates E (of E T). % This fails thanks to our special typing rules: %covers of +E *T. % examples of typechecking of various expressions %query 1 2 of (tlam [t] cons (lam [x] x) (nil)) T. %query 1 2 of (cons (int (s z)) (nil)) T. %query 1 2 of (brand (cons (int z) (nil)) (tlam [ts] lam [ba] lam [bl] lam [bh] (index_cmp bl bh (int z) (lam [il] lam [ih] bget ba il)))) T. %query 0 2 of (brand (cons (int z) (nil)) (tlam [ts] lam [ba] lam [bl] lam [bh] (index_cmp bl bh (int z) (lam [il] lam [ih] bget ba bl)))) T. % bindexV ``cannot occur freely''. The type of the bget expression cannot be % generalized and so the expression can't be the argument of brand. %query 0 2 of (brand (cons (int z) (nil)) (tlam [ts] lam [ba] lam [bl] lam [bh] bget ba (bindexV z))) T. % ---------------------------------------------------------------------- % Dynamic semantics: small-step evaluation relation % values val : exp -> type. %name val P. %mode val +E. val_lam : val (lam E). val_tlam : val (tlam E). val_nil : val (nil). val_cons : val (cons E1 E2) <- val E1 <- val E2. val_int : val (int _). val_barrayV : val (barrayV E) <- val E. val_bindexV : val (bindexV E). val_bindexLV : val (bindexLV E). val_bindexHV : val (bindexHV E). %worlds () (val E). %terminates E (val E). val_llen : of E (list T) -> val E -> llen E N -> type. %mode val_llen +P +V -Q. - : val_llen tp_nil val_nil llen1. - : val_llen (tp_cons P _) (val_cons V _) (llen2 Q) <- val_llen P V Q. %worlds () (val_llen _ _ _). %total P (val_llen P _ _). listref : exp -> nat -> exp -> type. %mode listref +E1 +N -E2. list_ref1 : listref (cons E1 E2) (s z) E1 <- val E1 <- val E2. list_ref2 : listref (cons E1 E2) (s N) ER <- val E1 <- listref E2 N ER. %worlds () (listref _ _ _). %terminates N (listref E1 N E2). % Give the proof that if the index is within the array % bounds, we can obtain the correponding array element % This is the total function (i.e., proof) listref-p : {E1:exp} {N:nat} {E2:exp} val E1 -> llen E1 NL -> leq (s z) N -> leq N NL -> listref E1 N E2 -> type. %mode listref-p +E1 +N -E2 +EV +EL +ENL +ENH -M. - : listref-p _ _ _ (val_cons V2 V1) _ _ _ (list_ref1 V2 V1). - : listref-p _ _ _ (val_cons V2 V1) (llen2 EL) _ (leq2 ENH) (list_ref2 M V1) <- listref-p _ _ _ V2 EL leq_s_z ENH M. %worlds () (listref-p _ _ _ _ _ _ _ _). %terminates N (listref-p E1 N _ E2 _ _ _ M). %total EV (listref-p _ _ _ EV _ _ _ _). % Prove that listref is type-preserving tps_listref : of E (list T) -> listref E N E' -> of E' T -> type. %mode tps_listref +P +PL -Q. tps_listref_z : tps_listref (tp_cons P2 P1) (list_ref1 PL _) P1. tps_listref_s : tps_listref (tp_cons P2 P1) (list_ref2 PL _) Q <- tps_listref P2 PL Q. %{ %theorem tps_listref : forall* {E:exp} {T:tp} {N:nat} {E':exp} forall {P:of E (list T)} {PL:listref E N E'} exists {Q:of E' T} true. %prove 3 {P PL} (tps_listref P PL _). }% %worlds () (tps_listref _ _ _). %total P (tps_listref P _ _). eval : exp -> exp -> type. %name eval D. %mode eval +E -E'. eval_app : eval (app (lam E1) E2) (E1 E2) <- val E2. eval_tapp : {t:tp} eval (tapp (tlam E) t) (E t). eval_unbi : eval (unbi (bindexV N)) (int N). eval_bpred : eval (bpred (bindexV (s N))) (bindexHV N). eval_bsucc : eval (bsucc (bindexV N)) (bindexLV (s N)). eval_bmiddle : eval (bmiddle (bindexV N1) (bindexV N2)) (bindexV N3) <- mid N1 N2 N3. eval_bget : eval (bget (barrayV EA) (bindexV N)) ER <- listref EA N ER. eval_brand : eval (brand EL EK) (app (app (app (tapp EK (tnum N)) (barrayV EL)) (bindexLV (s z))) (bindexHV N)) <- val EL <- llen EL N. % Congruence rules (not interesting) eval_icmp1 : eval (index_cmp (bindexLV NL) (bindexHV NH) EG ELE) (app (app ELE (bindexV NL)) (bindexV NH)) <- leq NL NH. eval_icmp2 : eval (index_cmp (bindexLV NL) (bindexHV NH) EG ELE) EG <- leq (s NH) NL. eval_app1 : eval (app E1 E2) (app E1' E2) <- eval E1 E1'. eval_app2 : eval (app E1 E2) (app E1 E2') <- val E1 <- eval E2 E2'. eval_tapp1 : eval (tapp E T) (tapp E' T) <- eval E E'. eval_cons1 : eval (cons E1 E2) (cons E1' E2) <- eval E1 E1'. eval_cons2 : eval (cons E1 E2) (cons E1 E2') <- val E1 <- eval E2 E2'. eval_unbi1 : eval (unbi E) (unbi E') <- eval E E'. eval_bpred1 : eval (bpred E) (bpred E') <- eval E E'. eval_bsucc1 : eval (bsucc E) (bsucc E') <- eval E E'. eval_bmiddle1 : eval (bmiddle E1 E2) (bmiddle E1' E2) <- eval E1 E1'. eval_bmiddle2 : eval (bmiddle E1 E2) (bmiddle E1 E2') <- val E1 <- eval E2 E2'. eval_bget1 : eval (bget E1 E2) (bget E1' E2) <- eval E1 E1'. eval_bget2 : eval (bget E1 E2) (bget E1 E2') <- val E1 <- eval E2 E2'. eval_barrayV : eval (barrayV E) (barrayV E') <- eval E E'. eval_brand1 : eval (brand E1 E2) (brand E1' E2) <- eval E1 E1'. eval_icmp3 : eval (index_cmp E1 E2 EG ELE) (index_cmp E1' E2 EG ELE) <- eval E1 E1'. eval_icmp4 : eval (index_cmp E1 E2 EG ELE) (index_cmp E1 E2' EG ELE) <- val E1 <- eval E2 E2'. %worlds () (eval E E'). %terminates E (eval E E'). % Prove that evaluation preserves list length eval_llen : eval E E' -> llen E N -> llen E' N -> type. %mode eval_llen +D +P -Q. eval_llen_cons1 : eval_llen (eval_cons1 _) (llen2 P) (llen2 P). eval_llen_cons2 : eval_llen (eval_cons2 D _) (llen2 P) (llen2 Q) <- eval_llen D P Q. %{ %theorem eval_llen : forall* {E:exp} {T:tp} {N:nat} {E':exp} forall {D:eval E E'} {P:llen T E N} exists {Q:llen T E' N} true. %prove 3 {D P} (eval_llen D P _). }% %worlds () (eval_llen _ _ _). %total D (eval_llen D P _). % Big step: transitive closure of eval*: just to be able to run examples eval* : exp -> exp -> type. %mode eval* +E -E'. eval1* : eval* E E <- val E. eval2* : eval* E E'' <- eval E E' <- eval* E' E''. % sample example sample_list = (cons (int z) (cons (int (s z)) (cons (int (s (s z))) (nil)))). %query 1 2 llen sample_list N. %query 1 2 leq (s z) (s (s z)). %query 1 1 eval* (brand sample_list (tlam [ts] lam [ba] lam [bl] lam [bh] (index_cmp bl bh (int z) (lam [il] lam [ih] unbi il)))) E. %query 1 1 eval* (brand sample_list (tlam [ts] lam [ba] lam [bl] lam [bh] (index_cmp bl bh (int (s (s (s z)))) (lam [il] lam [ih] bget ba ih)))) E. %query 1 1 eval* (brand sample_list (tlam [ts] lam [ba] lam [bl] lam [bh] (index_cmp bl bh (int z) (lam [il] lam [ih] bget ba (bmiddle il ih))))) E. % ---------------------------------------------------------------------- % Proving type-preservation: small-step evaluation preserves types tps : eval E E' -> of E T -> of E' T -> type. %mode tps +D +P -Q. tps_app : tps (eval_app _) (tp_app P2 (tp_lam P1)) (P1 _ P2). tps_tapp : tps (eval_tapp T) (tp_tapp (tp_tlam P)) (P T). tps_unbi : tps (eval_unbi) _ tp_int. tps_bpred : tps (eval_bpred) (tp_bpred (tp_bindex _ (leq2 P))) (tp_bindexH Q) <- leq_succ P Q. tps_bsucc : tps (eval_bsucc) _ tp_bindexL. tps_bmiddle : tps (eval_bmiddle P) (tp_bmiddle (tp_bindex _ P2) (tp_bindex _ P1)) (tp_bindex leq_s_z Q) <- mid_leq P1 P2 P Q. tps_bget : tps (eval_bget PL) (tp_get _ (tp_barrayV _ P)) Q <- tps_listref P PL Q. tps_brand : tps (eval_brand PL _) (tp_brand PK P) (tp_app (tp_bindexH Q2) (tp_app tp_bindexL (tp_app (tp_barrayV PL P) (tp_tapp PK)))) <- leq_refl _ Q2. % dumb congruences tps_icmp1 : tps (eval_icmp1 P) (tp_icmp PK _ (tp_bindexH P2) (tp_bindexL)) (tp_app (tp_bindex Q1 P2) (tp_app (tp_bindex leq_s_z Q2) PK)) <- leq_trans (leq2 leq1) P Q1 <- leq_trans P P2 Q2. tps_icmp2 : tps (eval_icmp2 _) (tp_icmp PK PG _ _) PG. tps_app1 : tps (eval_app1 D) (tp_app P2 P1) (tp_app P2 P1') <- tps D P1 P1'. tps_app2 : tps (eval_app2 D _) (tp_app P2 P1) (tp_app P2' P1) <- tps D P2 P2'. tps_tapp1 : tps (eval_tapp1 D) (tp_tapp P) (tp_tapp P') <- tps D P P'. tps_cons1 : tps (eval_cons1 D) (tp_cons P2 P1) (tp_cons P2 P1') <- tps D P1 P1'. tps_cons2 : tps (eval_cons2 D _) (tp_cons P2 P1) (tp_cons P2' P1) <- tps D P2 P2'. tps_unbi1 : tps (eval_unbi1 D) (tp_unbi P) (tp_unbi P') <- tps D P P'. tps_bpred1 : tps (eval_bpred1 D) (tp_bpred P) (tp_bpred P') <- tps D P P'. tps_bsucc1 : tps (eval_bsucc1 D) (tp_bsucc P) (tp_bsucc P') <- tps D P P'. tps_bmiddle1 : tps (eval_bmiddle1 D) (tp_bmiddle P2 P1) (tp_bmiddle P2 P1') <- tps D P1 P1'. tps_bmiddle2 : tps (eval_bmiddle2 D _) (tp_bmiddle P2 P1) (tp_bmiddle P2' P1) <- tps D P2 P2'. tps_bget1 : tps (eval_bget1 D) (tp_get P2 P1) (tp_get P2 P1') <- tps D P1 P1'. tps_bget2 : tps (eval_bget2 D _) (tp_get P2 P1) (tp_get P2' P1) <- tps D P2 P2'. tps_barrayV : tps (eval_barrayV D) (tp_barrayV PL P) (tp_barrayV PL' P') <- tps D P P' <- eval_llen D PL PL'. tps_brand1 : tps (eval_brand1 D) (tp_brand PK P) (tp_brand PK P') <- tps D P P'. tps_icmp3 : tps (eval_icmp3 D) (tp_icmp PK PG P2 P1) (tp_icmp PK PG P2 P1') <- tps D P1 P1'. tps_icmp4 : tps (eval_icmp4 D _) (tp_icmp PK PG P2 P1) (tp_icmp PK PG P2' P1) <- tps D P2 P2'. %worlds () (tps _ _ _). %terminates E (tps E _ _). % %covers tps +E +T *T'. %total E (tps E _ _). % It is total, so tps is the proof of type preservation! %{ %theorem tpp : forall* {E:exp} {E':exp} {T:tp} forall {D:eval E E'} {P:of E T} exists {Q:of E' T} true. %prove 4 {D P} (tpp D P _). }% % ---------------------------------------------------------------------- % Proving progress: a well-typed expression is either a value, % or can be reduced. context : exp -> type. %mode context +E. context_app : context (app E1 E2) <- val E1 <- val E2. context_app1 : context (app E1 E2) <- context E1. context_app2 : context (app E1 E2) <- val E1 <- context E2. context_tapp : context (tapp E T) <- val E. context_tapp1 : context (tapp E T) <- context E. context_cons1 : context (cons E1 E2) <- context E1. context_cons2 : context (cons E1 E2) <- val E1 <- context E2. context_barrayV : context (barrayV E) <- context E. context_brand : context (brand V _) <- val V. context_brand1 : context (brand E _) <- context E. context_bmiddle : context (bmiddle E1 E2) <- val E1 <- val E2. context_bmiddle1 : context (bmiddle E1 E2) <- context E1. context_bmiddle2 : context (bmiddle E1 E2) <- val E1 <- context E2. context_icmp : context (index_cmp E1 E2 _ _) <- val E1 <- val E2. context_icmp1 : context (index_cmp E1 E2 _ _) <- context E1. context_icmp2 : context (index_cmp E1 E2 _ _) <- val E1 <- context E2. context_bsucc : context (bsucc E) <- val E. context_bsucc1 : context (bsucc E) <- context E. context_bpred : context (bpred E) <- val E. context_bpred1 : context (bpred E) <- context E. context_bget : context (bget E1 E2) <- val E1 <- val E2. context_bget1 : context (bget E1 E2) <- context E1. context_bget2 : context (bget E1 E2) <- val E1 <- context E2. context_unbi : context (unbi E) <- val E. context_unbi1 : context (unbi E) <- context E. %worlds () (context E). %terminates E (context E). % Proving that each expression is either a value, or is a `context' % (can be focused, in a unique way). falsum : type. uniqd : val E -> context E -> falsum -> type. %mode uniqd +PV +PC -F. uniqd_cons1 : uniqd (val_cons PV2 PV1) (context_cons1 PC1) F <- uniqd PV1 PC1 F. uniqd_cons2 : uniqd (val_cons PV2 PV1) (context_cons2 PC2 _) F <- uniqd PV2 PC2 F. uniqd_barrayV : uniqd (val_barrayV V) (context_barrayV C) F <- uniqd V C F. %worlds () (uniqd _ _ _). %total PV (uniqd PV _ _). decompose : exp -> type. %name decompose D. decompose_val : val E -> decompose E. decompose_context : context E -> decompose E. alwaysd_app : decompose E1 -> decompose E2 -> context (app E1 E2) -> type. %mode alwaysd_app +D1 +D2 -C. - : alwaysd_app (decompose_context C1) _ (context_app1 C1). - : alwaysd_app (decompose_val V1) (decompose_context C2) (context_app2 C2 V1). - : alwaysd_app (decompose_val V1) (decompose_val V2) (context_app V2 V1). %worlds () (alwaysd_app _ _ _). %total {} (alwaysd_app _ _ _). alwaysd_tapp : decompose E -> {T:tp} context (tapp E T) -> type. %mode alwaysd_tapp +D +T -C. - : alwaysd_tapp (decompose_val V) _ (context_tapp V). - : alwaysd_tapp (decompose_context C) _ (context_tapp1 C). %worlds () (alwaysd_tapp _ _ _). %total {} (alwaysd_tapp _ _ _). alwaysd_cons : decompose E1 -> decompose E2 -> decompose (cons E1 E2) -> type. %mode alwaysd_cons +D1 +D2 -D. - : alwaysd_cons (decompose_context C1) _ (decompose_context (context_cons1 C1)). - : alwaysd_cons (decompose_val V1) (decompose_context C2) (decompose_context (context_cons2 C2 V1)). - : alwaysd_cons (decompose_val V1) (decompose_val V2) (decompose_val (val_cons V2 V1)). %worlds () (alwaysd_cons _ _ _). %total {} (alwaysd_cons _ _ _). alwaysd_barrayV : decompose E -> decompose (barrayV E) -> type. %mode alwaysd_barrayV +D' -D. - : alwaysd_barrayV (decompose_val V) (decompose_val (val_barrayV V)). - : alwaysd_barrayV (decompose_context C) (decompose_context (context_barrayV C)). %worlds () (alwaysd_barrayV _ _). %total {} (alwaysd_barrayV _ _). alwaysd_brand : decompose EA -> {EK:exp} context (brand EA EK) -> type. %mode alwaysd_brand +D' +EK -C. - : alwaysd_brand (decompose_val V) _ (context_brand V). - : alwaysd_brand (decompose_context C) _ (context_brand1 C). %worlds () (alwaysd_brand _ _ _). %total {} (alwaysd_brand _ _ _). alwaysd_bmiddle : decompose E1 -> decompose E2 -> context (bmiddle E1 E2) -> type. %mode alwaysd_bmiddle +D1 +D2 -C. - : alwaysd_bmiddle (decompose_context C1) _ (context_bmiddle1 C1). - : alwaysd_bmiddle (decompose_val V1) (decompose_context C2) (context_bmiddle2 C2 V1). - : alwaysd_bmiddle (decompose_val V1) (decompose_val V2) (context_bmiddle V2 V1). %worlds () (alwaysd_bmiddle _ _ _). %total {} (alwaysd_bmiddle _ _ _). alwaysd_icmp : decompose E1 -> decompose E2 -> {EGK:exp} {ELK:exp} context (index_cmp E1 E2 EGK ELK) -> type. %mode alwaysd_icmp +D1 +D2 +EGK +ELK -C. - : alwaysd_icmp (decompose_context C1) _ _ _ (context_icmp1 C1). - : alwaysd_icmp (decompose_val V1) (decompose_context C2) _ _ (context_icmp2 C2 V1). - : alwaysd_icmp (decompose_val V1) (decompose_val V2) _ _ (context_icmp V2 V1). %worlds () (alwaysd_icmp _ _ _ _ _). %total {} (alwaysd_icmp _ _ _ _ _). alwaysd_bsucc : decompose E -> context (bsucc E) -> type. %mode alwaysd_bsucc +D -C. - : alwaysd_bsucc (decompose_val V) (context_bsucc V). - : alwaysd_bsucc (decompose_context C) (context_bsucc1 C). %worlds () (alwaysd_bsucc _ _). %total {} (alwaysd_bsucc _ _). alwaysd_bpred : decompose E -> context (bpred E) -> type. %mode alwaysd_bpred +D -C. - : alwaysd_bpred (decompose_val V) (context_bpred V). - : alwaysd_bpred (decompose_context C) (context_bpred1 C). %worlds () (alwaysd_bpred _ _). %total {} (alwaysd_bpred _ _). alwaysd_bget : decompose E1 -> decompose E2 -> context (bget E1 E2) -> type. %mode alwaysd_bget +D1 +D2 -C. - : alwaysd_bget (decompose_context C1) _ (context_bget1 C1). - : alwaysd_bget (decompose_val V1) (decompose_context C2) (context_bget2 C2 V1). - : alwaysd_bget (decompose_val V1) (decompose_val V2) (context_bget V2 V1). %worlds () (alwaysd_bget _ _ _). %total {} (alwaysd_bget _ _ _). alwaysd_unbi : decompose E -> context (unbi E) -> type. %mode alwaysd_unbi +D -C. - : alwaysd_unbi (decompose_val V) (context_unbi V). - : alwaysd_unbi (decompose_context C) (context_unbi1 C). %worlds () (alwaysd_unbi _ _). %total {} (alwaysd_unbi _ _). alwaysd : {E:exp} decompose E -> type. %mode alwaysd +E -D. - : alwaysd (lam _) (decompose_val val_lam). - : alwaysd (app E1 E2) (decompose_context C) <- alwaysd E1 D1 <- alwaysd E2 D2 <- alwaysd_app D1 D2 C. - : alwaysd (tlam _) (decompose_val val_tlam). - : alwaysd (tapp E T) (decompose_context C) <- alwaysd E D <- alwaysd_tapp D T C. - : alwaysd (nil) (decompose_val val_nil). - : alwaysd (cons E1 E2) D <- alwaysd E1 D1 <- alwaysd E2 D2 <- alwaysd_cons D1 D2 D. - : alwaysd (int _) (decompose_val val_int). - : alwaysd (barrayV E) D <- alwaysd E D' <- alwaysd_barrayV D' D. - : alwaysd (bindexV E) (decompose_val val_bindexV). - : alwaysd (bindexLV E) (decompose_val val_bindexLV). - : alwaysd (bindexHV E) (decompose_val val_bindexHV). - : alwaysd (brand EA EK) (decompose_context C) <- alwaysd EA D <- alwaysd_brand D EK C. - : alwaysd (bmiddle E1 E2) (decompose_context C) <- alwaysd E1 D1 <- alwaysd E2 D2 <- alwaysd_bmiddle D1 D2 C. - : alwaysd (index_cmp E1 E2 EGK ELK) (decompose_context C) <- alwaysd E1 D1 <- alwaysd E2 D2 <- alwaysd_icmp D1 D2 EGK ELK C. - : alwaysd (bsucc E) (decompose_context C) <- alwaysd E D <- alwaysd_bsucc D C. - : alwaysd (bpred E) (decompose_context C) <- alwaysd E D <- alwaysd_bpred D C. - : alwaysd (bget E1 E2) (decompose_context C) <- alwaysd E1 D1 <- alwaysd E2 D2 <- alwaysd_bget D1 D2 C. - : alwaysd (unbi E) (decompose_context C) <- alwaysd E D <- alwaysd_unbi D C. %worlds () (alwaysd _ _). %total E (alwaysd E _). %{ %theorem tprog1 : forall* {E:exp} {E':exp} {T:tp} forall {C:context E} {P:of E T} exists {D:eval E E'} true. %prove 4 {C P} (tprog1 C P _). }% prog_icmp : {N1:nat} {N2:nat} {E1:exp} {E2:exp} leq-gt N1 N2 -> eval (index_cmp (bindexLV N1) (bindexHV N2) E1 E2) E' -> type. %mode prog_icmp +N1 +N2 +E1 +E2 +M -D. - : prog_icmp _ _ _ _ (leq-gt_leq P) (eval_icmp1 P). - : prog_icmp _ _ _ _ (leq-gt_gt P) (eval_icmp2 P). %worlds () (prog_icmp _ _ _ _ _ _). %terminates {} (prog_icmp _ _ _ _ _ _). %total {} (prog_icmp _ _ _ _ _ _). % Unfortunately, Twelf makes us prove these impossible facts, % such as nil cannot be of the type bindex... kind_error_nil : of (nil) (bindex _) -> falsum -> type. %mode kind_error_nil +P -F. %worlds () (kind_error_nil _ _). %total {} (kind_error_nil _ _). kind_error_=> : of E (bindex (_ => _)) -> val E -> falsum -> type. %mode kind_error_=> +P +PV -F. - : kind_error_=> P val_nil F <- kind_error_nil P F. %worlds () (kind_error_=> _ _ _). %total {} (kind_error_=> _ _ _). kind_error_all : of E (bindex (all _)) -> val E -> falsum -> type. %mode kind_error_all +P +PV -F. - : kind_error_all P val_nil F <- kind_error_nil P F. %worlds () (kind_error_all _ _ _). %total {} (kind_error_all _ _ _). kind_error_list : of E (bindex (list _)) -> val E -> falsum -> type. %mode kind_error_list +P +PV -F. - : kind_error_list P val_nil F <- kind_error_nil P F. %worlds () (kind_error_list _ _ _). %total {} (kind_error_list _ _ _). kind_error_tint : of E (bindex tint) -> val E -> falsum -> type. %mode kind_error_tint +P +PV -F. - : kind_error_tint P val_nil F <- kind_error_nil P F. %worlds () (kind_error_tint _ _ _). %total {} (kind_error_tint _ _ _). kind_error_barray : of E (bindex (barray _ _)) -> val E -> falsum -> type. %mode kind_error_barray +P +PV -F. - : kind_error_barray P val_nil F <- kind_error_nil P F. %worlds () (kind_error_barray _ _ _). %total {} (kind_error_barray _ _ _). kind_error_bindex : of E (bindex (bindex _)) -> val E -> falsum -> type. %mode kind_error_bindex +P +PV -F. - : kind_error_bindex P val_nil F <- kind_error_nil P F. %worlds () (kind_error_bindex _ _ _). %total {} (kind_error_bindex _ _ _). kind_error_bindexL : of E (bindex (bindexL _)) -> val E -> falsum -> type. %mode kind_error_bindexL +P +PV -F. - : kind_error_bindexL P val_nil F <- kind_error_nil P F. %worlds () (kind_error_bindexL _ _ _). %total {} (kind_error_bindexL _ _ _). kind_error_bindexH : of E (bindex (bindexH _)) -> val E -> falsum -> type. %mode kind_error_bindexH +P +PV -F. - : kind_error_bindexH P val_nil F <- kind_error_nil P F. %worlds () (kind_error_bindexH _ _ _). %total {} (kind_error_bindexH _ _ _). ex_falso_eval : falsum -> {E:exp} eval E (int z) -> type. %mode ex_falso_eval +F +E -D. %worlds () (ex_falso_eval _ _ _). %total {} (ex_falso_eval _ _ _). % Finally, the proof of progress prog : context E -> of E T -> eval E E' -> type. %mode prog +C +P -D. - : prog (context_app V2 V1) _ (eval_app V2). - : prog (context_app1 C1) (tp_app P2 P1) (eval_app1 D) <- prog C1 P1 D. - : prog (context_app2 C2 V1) (tp_app P2 P1) (eval_app2 D V1) <- prog C2 P2 D. - : prog (context_tapp V) _ (eval_tapp _). - : prog (context_tapp1 C) (tp_tapp P) (eval_tapp1 D) <- prog C P D. - : prog (context_cons1 C1) (tp_cons P2 P1) (eval_cons1 D) <- prog C1 P1 D. - : prog (context_cons2 C2 V1) (tp_cons P2 P1) (eval_cons2 D V1) <- prog C2 P2 D. - : prog (context_barrayV C) (tp_barrayV _ P) (eval_barrayV D) <- prog C P D. - : prog (context_brand V) (tp_brand _ P) (eval_brand PL V) <- val_llen P V PL. - : prog (context_brand1 C) (tp_brand _ P) (eval_brand1 D) <- prog C P D. - : prog (context_bmiddle _ _) _ (eval_bmiddle MID) <- middle _ _ _ MID. - : prog (context_bmiddle1 C1) (tp_bmiddle P2 P1) (eval_bmiddle1 D) <- prog C1 P1 D. - : prog (context_bmiddle2 C2 V1) (tp_bmiddle P2 P1) (eval_bmiddle2 D V1) <- prog C2 P2 D. - : prog (context_bsucc _) _ (eval_bsucc). - : prog (context_bsucc1 C1) (tp_bsucc P1) (eval_bsucc1 D) <- prog C1 P1 D. - : prog (context_bpred _) _ (eval_bpred). - : prog (context_bpred1 C1) (tp_bpred P1) (eval_bpred1 D) <- prog C1 P1 D. - : prog (context_icmp (V2 : val (bindexHV N2)) (V1 : (val (bindexLV N1)))) P D <- leq-proof N1 N2 M <- prog_icmp _ _ _ _ M D. - : prog (context_icmp1 C1) (tp_icmp _ _ P2 P1) (eval_icmp3 D) <- prog C1 P1 D. - : prog (context_icmp2 C2 V1) (tp_icmp _ _ P2 P1) (eval_icmp4 D V1) <- prog C2 P2 D. - : prog (context_bget V2 (val_barrayV V1)) (tp_get (tp_bindex PL PH) (tp_barrayV P _) : of (bget (barrayV EA) (bindexV N)) _) (eval_bget M) <- listref-p EA N _ V1 P PL PH M. - : prog (context_bget V _) (tp_get P _) D <- kind_error_=> P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_all P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_list P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_tint P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_barray P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_bindex P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_bindexL P V F <- ex_falso_eval F _ D. - : prog (context_bget V _) (tp_get P _) D <- kind_error_bindexH P V F <- ex_falso_eval F _ D. - : prog (context_bget1 C1) (tp_get P2 P1) (eval_bget1 D) <- prog C1 P1 D. - : prog (context_bget2 C2 V1) (tp_get P2 P1) (eval_bget2 D V1) <- prog C2 P2 D. - : prog (context_unbi V1) (tp_unbi P1) (eval_unbi). - : prog (context_unbi1 C1) (tp_unbi P1) (eval_unbi1 D) <- prog C1 P1 D. %worlds () (prog C P D). %terminates C (prog C P D). %covers prog +C +P *D. %total C (prog C P D). progress : exp -> type. %mode progress +E. progress_val : val E -> progress E. progress_eval : eval E E' -> progress E. type_progress_alwaysd : decompose E -> of E T -> progress E -> type. %mode type_progress_alwaysd +Q +P -D. - : type_progress_alwaysd (decompose_val V) _ (progress_val V). - : type_progress_alwaysd (decompose_context C) P (progress_eval D) <- prog C P D. %worlds () (type_progress_alwaysd _ _ _). %total {} (type_progress_alwaysd _ _ _). type_progress : of E T -> progress E -> type. %mode type_progress +P -D. - : type_progress P D <- alwaysd _ Q <- type_progress_alwaysd Q P D. %worlds () (type_progress _ _). %total {} (type_progress _ _). % This declaration is accepted: we have a proof.