% 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.