final-task.elf

%%% The absurd statement. A tool for reasoning from false.
%%%   Jesper Louis Andersen 2008

void : type.   %name void _|_.
%freeze void.
%%% Booleans
%%%   Jesper Louis Andersen

% ===== The Boolean type =====
bool : type.

bool/true : bool.
bool/false : bool.

% Convenience
true = bool/true.
false = bool/false.%%% Peano Style Arithmetic
%%%   Jesper Louis Andersen

% ===== Syntax =====

nat : type. %name nat N.

nat/z : nat.
nat/s : nat -> nat.

%% Notation
z = nat/z.
s = nat/s.

% ===== Lists of natural numbers =====

natlist : type. %name natlist NATL.

natlist/nil : natlist.
natlist/cons : nat -> natlist -> natlist.

%%% Sizes of natlists

natlist-size : natlist -> nat -> type.
%mode natlist-size +NL -N.

natlist-size/nil : natlist-size natlist/nil z.

natlist-size/cons : natlist-size (natlist/cons N NL) (s K)
		     <- natlist-size NL K.

% ===== Reflexive equality =====
nat-eq : nat -> nat -> type.
%mode nat-eq +N1 +N2.

nat-eq/z : nat-eq z z.

nat-eq/s : nat-eq (s N1) (s N2)
	    <- nat-eq N1 N2.

%worlds () (nat-eq _ _).
%terminates N1 (nat-eq N1 _).

% ===== Non-equality of natural numbers =====
nat-neq : nat -> nat -> type.
%mode nat-neq +N1 +N2.

nat-neq/zs : nat-neq z (s _).
nat-neq/sz : nat-neq (s _) z.

nat-neq/ss : nat-neq (s S1) (s S2)
	      <- nat-neq S1 S2.

%worlds () (nat-neq _ _).
%terminates T (nat-neq T _).

% ===== Total ordering =====
nat-lt : nat -> nat -> type.
%mode nat-lt +N1 +N2.

nat-lt/z : nat-lt z (s _).
nat-lt/s : nat-lt (s N1) (s N2)
	    <- nat-lt N1 N2.

%worlds () (nat-lt _ _).
%terminates N1 (nat-lt N1 _).

% ===== Operators =====

%% The ''plus'' operation.
plus-nat : nat -> nat -> nat -> type.
%mode plus-nat +N1 +N2 -N3.

plus-nat/z : plus-nat z N N.

plus-nat/s : plus-nat (s N1) N2 (s N3)
	      <- plus-nat N1 N2 N3.

%worlds () (plus-nat _ _ _).
%total T (plus-nat T _ _).

%query 1 * (plus-nat (s z) (s (s z)) (s (s (s z)))).
%query 1 * (plus-nat z (s z) (s z)).

%% The ''monus'' operation.
monus-nat : nat -> nat -> nat -> type.
%mode monus-nat +N1 +N2 -N3.

monus-nat/z/1 : monus-nat z N z.

monus-nat/z/2 : monus-nat N z N.

monus-nat/s : monus-nat (s N1) (s N2) N3
	       <- monus-nat N1 N2 N3.

%worlds () (monus-nat _ _ _).
%total T (monus-nat T _ _).

%query 1 * (monus-nat (s (s (s z))) (s (s z)) (s z)).
%query 1 * (monus-nat (s (s z)) (s (s (s z))) z).
%% 2 solutions to this one generated from monus-nat/z/1 and monus-nat/z/2.
%query 2 * (monus-nat (s z) (s z) z).

% ===== Relations between natural numbers and booleans =====
nat-eq->bool : nat -> nat -> bool -> type.
%mode nat-eq->bool +N1 +N2 -B.

nat-eq->bool/zz : nat-eq->bool z z true.

nat-eq->bool/zs : nat-eq->bool z (s _) false.

nat-eq->bool/sz : nat-eq->bool (s _) z false.

nat-eq->bool/ss : nat-eq->bool (s N1) (s N2) T
			<- nat-eq->bool N1 N2 T.

%worlds () (nat-eq->bool _ _ _).
%total N (nat-eq->bool N _ _).

nat-leq->bool : nat -> nat -> bool -> type.
%mode nat-leq->bool +N1 +N2 -B.

nat-leq->bool/zz : nat-leq->bool z z true.

nat-leq->bool/zs : nat-leq->bool z (s _) true.

nat-leq->bool/sz : nat-leq->bool (s _) z false.

nat-leq->bool/ss : nat-leq->bool (s N1) (s N2) T
		    <- nat-leq->bool N1 N2 T.

%worlds () (nat-leq->bool _ _ _).
%total N (nat-leq->bool N _ _).
%%% Locations in the language
%%%   Jesper Louis Andersen

%% Locations

%% Variables
var : type.
fvar : type.

varlist : type.
varlist/nil : varlist.
varlist/cons : var -> varlist -> varlist.
%%% Peano Style Arithmetic
%%%   Jesper Louis Andersen

% ===== Syntax =====


%% Arithmetic expressions
exp : type. %name exp E.

exp/n : nat -> exp.
exp/v : var -> exp.
exp/plus : exp -> exp -> exp.
exp/monus : exp -> exp -> exp.

%{
  We need a way to represent lists of expressions when we want to do funcalls.
  Hence, we have chosen to represent these as functional lists.
}%

explist : type. %name explist EXPL.

explist/nil : explist.
explist/cons : exp -> explist -> explist.

%%% Length of explists
explist-length : explist -> nat -> type.
%mode explist-length +EL -N.

explist-length/nil : explist-length explist/nil z.
explist-length/cons : explist-length (explist/cons _ EL') (s N)
	<- explist-length EL' N.

%worlds () (explist-length _ _).
%total T (explist-length T _).

% ===== Boolean expressions =====

bexp : type. %name bexp B.

bexp/t : bool -> bexp.
bexp/eq : exp -> exp -> bexp.
bexp/leq : exp -> exp -> bexp.
bexp/and : bexp -> bexp -> bexp.
bexp/not : bexp -> bexp.

% ===== Commands =====

cmd : type. %name cmd C.

cmd/skip : cmd.
cmd/assign : var -> exp -> cmd.
; : cmd -> cmd -> cmd. %infix left 500 ;.
cmd/if : bexp -> cmd -> cmd -> cmd.
cmd/while : bexp -> cmd -> cmd.
cmd/funcall : var -> fvar -> explist -> cmd.
cmd/return : exp -> cmd.

% ===== Programs =====
locbind : type. %name locbind LOCB.
locbind/nil : cmd -> locbind.
locbind/cons : (var -> locbind) -> locbind.

parbind : type. %name parbind PARB.
parbind/nil : locbind -> parbind.
parbind/cons : (var -> parbind) -> parbind.

program : type. %name program PGM.

program/main : (fvar -> parbind) -> program.
program/cons : (fvar -> parbind) -> (fvar -> program) -> program.

%% This is mapping from variables to types.
varenv-map : var -> nat -> type.
%mode varenv-map +V -N.

%% Mapping from function variables to function definitions
decenv-map : fvar -> parbind -> type.
%mode decenv-map +F -D.
%%% Implementation of the "store" or "store"
%%%    Jesper Louis Andersen

store : type. %name store S.

store/nil : store.
store/cons : nat -> store -> store.

%%% Length of a store
store-length : store -> nat -> type.
%mode store-length +H -N.

store-length/nil : store-length store/nil z.

store-length/cons : store-length (store/cons _ H) (s N)
	<- store-length H N.

%worlds () (store-length _ _).
%total H (store-length H _).
%unique store-length +H -1N.

%%% Look up a location in a store
store-find : nat -> store -> nat -> type.
%mode store-find +L +H -E.

store-find/yes : store-find z (store/cons N _) N.

store-find/no : store-find (s K) (store/cons _ H) N
	<- store-find K H N.

%worlds () (store-find _ _ _).
%terminates H (store-find _ H _).
%unique store-find +L +H -1E.

store-replace : store -> nat -> nat -> store -> type.
%mode store-replace +H1 +L +N -H2.

store-replace/yes : store-replace (store/cons N1 H) z N2 (store/cons N2 H).

store-replace/no : store-replace (store/cons N1 H) (s K) N2 (store/cons N1 H')
	<- store-replace H K N2 H'.

%%worlds () (store-replace _ _ _ _).
%%terminates H (store-replace H _ _ _).
%%unique store-replace +H1 +L +E -1H2.

%%% Append to a store

store-append : store -> nat -> store -> type.
%mode store-append +H1 +N -H2.

store-append/nil : store-append store/nil N (store/cons N store/nil).

store-append/cons : store-append (store/cons N' H) N (store/cons N' H')
	<- store-append H N H'.

%worlds () (store-append _ _ _).
%total H (store-append H _ _).
%unique store-append +H1 +N -1H2.

%%% Hack the SML option type for stores
store-option : type.

store-option/none : store-option.
store-option/some : store -> locbind -> store-option.
%%% Formalization of semantics.
%%%   Jesper Louis Andersen

% ===== Expression evaluation =====

%%% Arithmetic
eval-exp : exp -> store -> nat -> type.
%mode eval-exp +E +S -N.

eval-exp/n : eval-exp (exp/n N) S N.

eval-exp/v : eval-exp (exp/v V) S N
	<- varenv-map V L
	<- store-find L S N.

eval-exp/plus : eval-exp (exp/plus E1 E2) S N
		 <- eval-exp E1 S N1
		 <- eval-exp E2 S N2
		 <- plus-nat N1 N2 N.

eval-exp/monus : eval-exp (exp/monus E1 E2) S N
		  <- eval-exp E1 S N1
		  <- eval-exp E2 S N2
		  <- monus-nat N1 N2 N.

%terminates (E X) (eval-exp E _ _) (varenv-map X _).

% %%% Evaluation of arithmetic expressions
eval-explist : explist -> store -> natlist -> type.
%mode eval-explist +EL +S -N.

eval-explist/nil : eval-explist explist/nil S natlist/nil.

eval-explist/cons : eval-explist (explist/cons E EL) S (natlist/cons N NL)
		     <- eval-exp E S N
		     <- eval-explist EL S NL.

%terminates E (eval-explist E _ _).

%%% Booleans
eval-bexp : bexp -> store -> bool -> type.
%mode eval-bexp +E +S -B.

eval-bexp/bool : eval-bexp (bexp/t T) S T.

eval-bexp/eq : eval-bexp (bexp/eq E1 E2) S T
		<- eval-exp E1 S N1
		<- eval-exp E2 S N2
		<- nat-eq->bool N1 N2 T.

eval-bexp/leq : eval-bexp (bexp/leq E1 E2) S T
 		 <- eval-exp E1 S N1
 		 <- eval-exp E2 S N2
 		 <- nat-leq->bool N1 N2 T.

eval-bexp/and,1 : eval-bexp (bexp/and B1 B2) S false
		   <- eval-bexp B1 S false.

eval-bexp/and,2 : eval-bexp (bexp/and B1 B2) S T
 		   <- eval-bexp B1 S true
 		   <- eval-bexp B2 S T.

eval-bexp/not,1 : eval-bexp (bexp/not B) S true
 		   <- eval-bexp B S false.

eval-bexp/not,2 : eval-bexp (bexp/not B) S false
 		   <- eval-bexp B S true.

%terminates E (eval-bexp E _ _).

%%% Commands

%% Results
%{
  Commands require a notion of a result because there are multiple possible
  outcomes of the command
}%

store^ : type.

store^/wrong : store^.
store^/n : nat -> store^.
store^/store : store -> store^.

%%% Results from functions
fresult : type.

fresult/wrong : fresult.
fresult/n : nat -> fresult.

%%% Conversion
store^->fresult : store^ -> fresult -> type.
%mode store^->fresult +S^ -FR.

store^->fresult/n : store^->fresult (store^/n K) (fresult/n K).

store^->fresult/wrong : store^->fresult store^/wrong fresult/wrong.

store^->fresult/store : store^->fresult (store^/store _) fresult/wrong.

%% Commands
eval-cmd : cmd -> store -> store^ -> type.
%mode eval-cmd +C +S -S^.

bind-locals : locbind -> store -> store^ -> type.
%mode bind-locals +LB +S -S^.

bind-pars : parbind -> natlist -> store -> store^ -> type.
%mode bind-pars +PB +NL +S -S^.

eval-cmd/skip : eval-cmd cmd/skip S (store^/store S).

eval-cmd/assign : eval-cmd (cmd/assign V E) S (store^/store S')
	<- varenv-map V L
	<- eval-exp E S N
	<- store-replace S L N S'.

eval-cmd/semi,1 : eval-cmd (C1 ; C2) S S^
		       <- eval-cmd C1 S (store^/store S')
		       <- eval-cmd C2 S' S^.

eval-cmd/semi,2 : eval-cmd (C1 ; C2) S store^/wrong
 		       <- eval-cmd C1 S store^/wrong.

eval-cmd/semi,3 : eval-cmd (C1 ; C2) S (store^/n N)
		       <- eval-cmd C1 S (store^/n N).


eval-cmd/if,1 : eval-cmd (cmd/if B T E) S R
 		     <- eval-bexp B S true
 		     <- eval-cmd T S R.

eval-cmd/if,2 : eval-cmd (cmd/if B T E) S R
 		     <- eval-bexp B S false
 		     <- eval-cmd E S R.

eval-cmd/while,1 : eval-cmd (cmd/while B C) S R
  			<- eval-bexp B S true
  			<- eval-cmd C S (store^/store S')
  			<- eval-cmd (cmd/while B C) S' R.

eval-cmd/while,2,1 : eval-cmd (cmd/while B C) S store^/wrong
  			  <- eval-bexp B S true
  			  <- eval-cmd C S store^/wrong.

eval-cmd/while,2,2 : eval-cmd (cmd/while B C) S (store^/n N)
  			  <- eval-bexp B S true
  			  <- eval-cmd C S (store^/n N).

eval-cmd/while,3 : eval-cmd (cmd/while B C) S (store^/store S)
 			<- eval-bexp B S false.

eval-cmd/funcall,1 : eval-cmd (cmd/funcall X F EL) S (store^/store S')
	<- eval-explist EL S NL
	<- decenv-map F C
	<- bind-pars C NL store/nil R
	<- store^->fresult R (fresult/n N)
	<- varenv-map X L
	<- store-replace S L N S'.

eval-cmd/funcall,2 : eval-cmd (cmd/funcall X F EL) S store^/wrong
	<- eval-explist EL S NL	
	<- decenv-map F C
	<- bind-pars C NL store/nil R
	<- store^->fresult R fresult/wrong.

eval-cmd/return : eval-cmd (cmd/return E) S (store^/n N)
	<- eval-exp E S N. 

bind-locals/nil : bind-locals (locbind/nil C) S R
	<- eval-cmd C S R.
	
bind-locals/cons : bind-locals (locbind/cons ([y : var] C y)) S R
	<- store-length S L
	<- store-append S z S'
	<- ({x : var} varenv-map x L -> bind-locals (C x) S' R).

bind-pars/nil : bind-pars	(parbind/nil LB) natlist/nil S R
	<- bind-locals LB S R.

bind-pars/cons : bind-pars (parbind/cons ([x] C x)) (natlist/cons N NL) S R
	<- store-length S L
	<- store-append S N S'
	<- ({x : var} varenv-map x L -> bind-pars (C x) NL S' R).

bind-pars/f1 : bind-pars (parbind/cons ([x] C x)) natlist/nil S store^/wrong.
bind-pars/f2 : bind-pars (parbind/nil LB) (natlist/cons _ _) S store^/wrong.

eval-program : program -> natlist -> store^ -> type. 

eval-program/main : eval-program (program/main ([f] D f)) NL R
	<- ({f : fvar} decenv-map f (D f) -> bind-pars (D f) NL store/nil R).	

eval-program/cons : eval-program (program/cons ([f] D f) ([f] P f)) NL R
	<- ({f : fvar} decenv-map f (D f)
		-> eval-program (P f) NL R).

eval-p : program -> natlist -> fresult -> type.

eval-p,1 : eval-p P NL FL
	<- eval-program P NL S
	<- store^->fresult S FR.%%% Program definitions
%%%		Jesper Louis Andersen

%% Before trying our luck on the programs A and B, we do a series of queries
%% on much simpler structures for test purposes.

%% Arithmetic numbers
zero = z.
one = s z.
two = s (s z).
three = s two.
four = s three.
five = s four.
six = s five.
seven = s six.

%define twelf : nat = N
%solve twelf_compute : plus-nat six six N.

%define twentyfour : nat = K
%solve twentyfour_compute : plus-nat twelf twelf K.

test_1 : exp = (exp/plus (exp/n three) (exp/n four)).
%query 1 * (eval-exp test_1 store/nil seven).

test_2 : bexp = (bexp/eq (exp/n four) (exp/n four)).
test_2_1 : bexp = (bexp/not (bexp/t false)).
%query 1 * (eval-bexp test_2 store/nil true).
%query 1 * (eval-bexp test_2_1 store/nil true).

test_3 : (bool -> cmd) = [b] (cmd/if (bexp/t b) (cmd/return (exp/n three))
		(cmd/return (exp/n four))).
%query 1 * (eval-cmd (test_3 true) store/nil (store^/n three)).
%query 1 * (eval-cmd (test_3 false) store/nil (store^/n four)).

test_4_1 : parbind = (parbind/nil (locbind/nil
		(cmd/return (exp/n three)))).
%query 1 * (store-length store/nil z).

test_4_2 : parbind = (parbind/nil (locbind/cons [x] (locbind/nil
		(cmd/assign x (exp/n five);
		 cmd/return (exp/v x))))).


test_5 : parbind = (parbind/cons [x] (parbind/nil (locbind/nil
		(cmd/return (exp/v x))))).
test_5_i = (natlist/cons three natlist/nil).

test_5_1 : parbind = (parbind/cons [x] (parbind/nil (locbind/nil
		(cmd/skip)))).

test_6 : program = program/main ([fac] test_5).
%query 1 1 (eval-p test_6 natlist/nil fresult/wrong).
%query 1 1 (eval-p test_6 (natlist/cons three natlist/nil) (fresult/n three)).

test_7 : program = program/main ([callme]
	(parbind/cons [x] (parbind/nil (locbind/nil (cmd/if
		(bexp/eq (exp/v x) (exp/n z))
		(cmd/return (exp/n two))
		(cmd/funcall x callme (explist/cons
							(exp/monus (exp/v x)
							 (exp/n one)) explist/nil);
		 cmd/return (exp/v x))))))).
%query 1 1 (eval-p test_7 (natlist/cons two natlist/nil) (fresult/n two)).

%% Tests of the store...
%define s_1 = R
%solve s_1_compute : (store-append store/nil four R).
%query 1 1 (store-append store/nil four (store/cons four store/nil)).

%% Testing multiplication
program_mul = program/main
	([mul]
		(parbind/cons [x] (parbind/cons [y] (parbind/nil
			(locbind/cons [r] (locbind/nil
		((cmd/while (bexp/not (bexp/eq (exp/v x) (exp/n z)))
				((cmd/assign r (exp/plus (exp/v r) (exp/v y)));
				 (cmd/assign x (exp/monus (exp/v x) (exp/n one)))));
		 (cmd/return (exp/v r))))))))).

%query 1 1 (eval-p program_mul
			(natlist/cons one
			(natlist/cons one
				natlist/nil)) (fresult/n one)).

%% Project programs follow....
program_a = program/cons
	([mul]
		(parbind/cons [x] (parbind/cons [y] (parbind/nil
			(locbind/cons [r] (locbind/nil
		((cmd/while (bexp/not (bexp/eq (exp/v x) (exp/n z)))
				((cmd/assign r (exp/plus (exp/v r) (exp/v y)));
				 (cmd/assign x (exp/monus (exp/v x) (exp/n one)))));
		 (cmd/return (exp/v r)))))))))
	([mul] program/main ([fac] (parbind/cons [x] (parbind/nil
				(locbind/cons [r] (locbind/nil
			(cmd/if (bexp/eq (exp/v x) (exp/n z))
				(cmd/return (exp/n (s z)))
				((cmd/funcall r fac (explist/cons
									(exp/monus (exp/v x)
										(exp/n (s z)))
									explist/nil));
				 (cmd/funcall r mul (explist/cons (exp/v r)
										(explist/cons (exp/v x)
										explist/nil))));
				(cmd/return (exp/v r))))))))).

%query 1 * (eval-p program_a (natlist/cons z natlist/nil) (fresult/n one)).
%query 1 1 (eval-p program_a (natlist/cons one natlist/nil)
		(fresult/n one)).
%query 1 1 (eval-p program_a (natlist/cons four natlist/nil) (fresult/n twentyfour)).

program_b : program =
	(program/main [fun]
	(parbind/cons [x] (parbind/nil
		(locbind/nil
		(cmd/if (bexp/eq (exp/v x) (exp/n z))
			cmd/skip
			(cmd/if (bexp/eq (exp/v x) (exp/n one))
				(cmd/funcall x fun explist/nil)
				(cmd/if (bexp/eq (exp/v x) (exp/n two))
					(cmd/funcall x fun (explist/cons
									(exp/n z) (explist/cons (exp/v x)
										explist/nil)))
					(cmd/return (exp/monus (exp/v x) (exp/n four)))))))))).

eval_program_b = [n : nat] [r : fresult] (eval-p program_b
		(natlist/cons n natlist/nil) r).

%query 1 1 (eval-p program_b (natlist/cons z natlist/nil) fresult/wrong).
%query 1 1 (eval-p program_b (natlist/cons one natlist/nil) fresult/wrong).
%query 1 1 (eval-p program_b (natlist/cons two natlist/nil) fresult/wrong).
%query 1 1 (eval-p program_b (natlist/cons three natlist/nil) 
	(fresult/n z)).
%query 1 1 (eval-p program_b (natlist/cons four natlist/nil) 
	(fresult/n z)).
%query 1 1 (eval-p program_b (natlist/cons five natlist/nil)
	(fresult/n one)).%%% Language type system
%%%   Jesper Louis Andersen

%% Safety: Always encounters a return.
must-return : cmd -> type.
%mode must-return +C.

must-return/semi,1 : must-return (C1 ; C2)
	<- must-return C1.

must-return/semi,2 : must-return (C1 ; C2)
	<- must-return C2.

must-return/if : must-return (cmd/if B C1 C2)
	<- must-return C1
	<- must-return C2.

must-return/return : must-return (cmd/return E).

%% Arity environments
arityenv : fvar -> nat -> type.
%mode arityenv +F -N.

%% right-arguments checks that funcall has the right number of arguments.
right-arguments : cmd -> type.
%mode right-arguments +C.

right-arguments/skip : right-arguments cmd/skip.

right-arguments/assign : right-arguments (cmd/assign _ _).

right-arguments/semi : right-arguments (C1 ; C2)
	<- right-arguments C1
	<- right-arguments C2.

right-arguments/if : right-arguments (cmd/if B C1 C2)
	<- right-arguments C1
	<- right-arguments C2.

right-arguments/while : right-arguments (cmd/while B C)
	<- right-arguments C.

right-arguments/funcall : right-arguments (cmd/funcall V F EL)
	<- arityenv F K
	<- explist-length EL K.
	
right-arguments/return : right-arguments (cmd/return E).

check-command : cmd -> type.

check-command,1 : check-command C
	<- must-return C
	<- right-arguments C.

check-locbind : fvar -> locbind -> nat -> type.

check-locbind/cons : check-locbind F (locbind/cons ([x] R x)) K
	<- ({x : var} check-locbind F (R x) K).

check-locbind/nil : check-locbind F (locbind/nil C) K
	<- check-command C.

check-parbind : fvar -> parbind -> nat -> nat -> type.

check-parbind/cons : check-parbind F (parbind/cons ([x] R x)) K (s N)
	<- ({x : var} check-parbind F (R x) (s K) N).

check-parbind/nil : check-parbind F (parbind/nil LB) N z
	<- check-locbind F LB N.

check-program : program -> nat -> type.

check-program/main : check-program (program/main ([f : fvar] D f)) K
	<- ({f : fvar} arityenv f K -> check-parbind f (D f) z K).

check-program/cons : check-program (program/cons ([f] D f) ([f] P f)) N
	<- ({f : fvar} arityenv f K -> check-parbind f (D f) z K)
	<- ({f : fvar} arityenv f K -> check-program (P f) N).


%query 1 1 (check-program test_6 one).
%query 1 1 (check-program test_7 one).
%query 1 1 (check-program program_a one).

%%% The soundness theorem
%%%   Jesper Louis Andersen

%% A little lemma on expression lists
explist-lemma-1 : (eval-explist EL S NL) -> (explist-length EL K)
	-> (natlist-size NL K) -> type.
%mode explist-lemma-1 +EL +EEL -NLS.

explist-lemma-1/nil : explist-lemma-1
		eval-explist/nil
		explist-length/nil
		natlist-size/nil.

explist-lemma-1/cons : explist-lemma-1
		(eval-explist/cons EPL EP)
		(explist-length/cons EPL')
		(natlist-size/cons NLS')
	<- explist-lemma-1 EPL EPL' NLS'.

%% Bind together a function definition and its checked function body

checkenv : (arityenv F K) -> (decenv-map F D) ->
	(check-parbind F D z K) -> type.

%mode checkenv +AE +DECM -CP.

%% Contexts we are proving in.

%block varenv-block : some {L}
	block {x : var} {vm : varenv-map x L}.

%block checkenv-block : some {D : fvar -> parbind} {K} {CPB}
	block {f : fvar} {dm : decenv-map f (D f)} {ae : arityenv f K}
		{ce : checkenv ae dm (CPB f ae)}.

wrong-or-return : store^ -> type.
wrong-or-return/wrong : wrong-or-return store^/wrong.
wrong-or-return/res : wrong-or-return (store^/n N).

%% A contradiction on the form of the wrong-or-return.
rs-contradict-lemma-1 : wrong-or-return (store^/store S) -> void -> type.
%mode rs-contradict-lemma-1 +WR -V.
%worlds () (rs-contradict-lemma-1 _ _).
%total T (rs-contradict-lemma-1 T _).

rs-contradict-1-void-any : {S^} void -> (wrong-or-return S^) -> type.
%mode rs-contradict-1-void-any +S^ +V -WR.
%worlds () (rs-contradict-1-void-any _ _ _).
%total T (rs-contradict-1-void-any _ T _).

store-or-return : store^ -> type.
store-or-return/store : store-or-return (store^/store S).
store-or-return/res : store-or-return (store^/n N).


sresult-res : store^ -> type.

sresult-res/res : sresult-res (store^/n N).

sr-contradict : (sresult-res (store^/wrong)) -> void -> type.
%mode sr-contradict +SR -V.
%worlds () (sr-contradict _ _).
%total T (sr-contradict T _).

sr-contradict-2 : (sresult-res (store^/store _)) -> void -> type.
%mode sr-contradict-2 +SR -V.
%worlds () (sr-contradict-2 _ _).
%total T (sr-contradict-2 T _).

void-s-or-r : {S^} void -> (store-or-return S^) -> type.
%mode void-s-or-r +S^ +V -SR.
%worlds () (void-s-or-r _ _ _).
%total T (void-s-or-r _ T _).

void-sr : {S^} void -> (sresult-res S^) -> type.
%mode void-sr +S^ +V -SR.
%worlds () (void-sr _ _ _).
%total T (void-sr _ T _).

void-s : {N} void -> (sresult-res (store^/n N)) -> type.
%mode void-s +N +V -R.
%worlds () (void-s _ _ _).
%total T (void-s _ T _).

result-coerce : (store-or-return S^) -> (wrong-or-return S^)
		-> (sresult-res S^) -> type.
%mode result-coerce +SR +WR -S.

sresult->sr : (sresult-res S^) -> (store-or-return S^) -> type.
%mode sresult->sr +S -S'.

sresult->sr/res : sresult->sr sresult-res/res store-or-return/res.

%worlds () (sresult->sr _ _).
%total T (sresult->sr T _).

result-cource/ss : result-coerce
		store-or-return/res
		wrong-or-return/res
		sresult-res/res.

%worlds () (result-coerce _ _ _).
%total T (result-coerce T _ _).

return-soundness : (must-return C) -> (eval-cmd C S S^) -> (wrong-or-return S^) -> type.
%mode return-soundness +MR +EP -S.

return-soundness/return : return-soundness
		must-return/return
		(eval-cmd/return CP)
		wrong-or-return/res.
		
return-soundness/if,1 : return-soundness
		(must-return/if RP2 RP1)
		(eval-cmd/if,1 CP BP)
		R
	<- return-soundness RP1 CP R.

return-soundness/if,2 : return-soundness
		(must-return/if RP2 RP1)
		(eval-cmd/if,2 CP BP)
		R
	<- return-soundness RP2 CP R.

return-soundness/semi,3 : return-soundness
		(must-return/semi,1 RP)
		(eval-cmd/semi,3 CP)
		R
	<- return-soundness RP CP R.

return-soundness/semi,2 : return-soundness
		(must-return/semi,1 RP)
		(eval-cmd/semi,2 CP)
		R
	<- return-soundness RP CP R.

return-soundness/semi,1 : return-soundness
		(must-return/semi,2 RP)
		(eval-cmd/semi,1 CP2 CP1)
		R
	<- return-soundness RP CP2 R.

return-soundness/semi,2,2 : return-soundness
		(must-return/semi,2 RP)
		(eval-cmd/semi,2 CP)
		wrong-or-return/wrong.

return-soundness/semi,2,3 : return-soundness
		(must-return/semi,2 RP)
		(eval-cmd/semi,3 CP)
		wrong-or-return/res.

return-soundness/semi,1,1,r : return-soundness
		(must-return/semi,1 RP)
		(eval-cmd/semi,1 CP2 CP1)
		wrong-or-return/res.

return-soundness/semi,1,1,w : return-soundness
		(must-return/semi,1 RP)
		(eval-cmd/semi,1 CP2 CP1)
		wrong-or-return/wrong.

return-soundness/semi,1,1 : return-soundness
		(must-return/semi,1 RP)
		(eval-cmd/semi,1 CP2 CP1)
		Q
	<- return-soundness RP CP1 R
	<- rs-contradict-lemma-1 R V
	<- rs-contradict-1-void-any _ V Q.


argument-soundness : (eval-cmd C S S^) -> (right-arguments C)
				-> (store-or-return S^) -> type.
%mode argument-soundness +C +RA -S.

parbind-soundness : {F} (bind-pars PB NL S S^)
	-> (check-parbind F PB N K)  -> (natlist-size NL K)
	-> (sresult-res S^) -> type.
%mode parbind-soundness +F +BP +CB +NLS -SR.

argument-soundness/return : argument-soundness
		(eval-cmd/return EP)
		right-arguments/return
		store-or-return/res.

argument-soundness/skip : argument-soundness
		eval-cmd/skip
		right-arguments/skip
		store-or-return/store.

argument-soundness/while,1 : argument-soundness
		(eval-cmd/while,1 CP2 CP1 BP)
		RA
		R
	<- argument-soundness CP2 RA R.

argument-soundness/while,3 : argument-soundness
		(eval-cmd/while,3 BP)
		RA
		store-or-return/store.

argument-soundness/while,2,2 : argument-soundness
		(eval-cmd/while,2,2 CP BP)
		RA
		store-or-return/res.

argument-soundness/while,2,1 : argument-soundness
		(eval-cmd/while,2,1 CP BP)
		(right-arguments/while AP)
		R
	<- argument-soundness CP AP R.

argument-soundness/if,1 : argument-soundness
		(eval-cmd/if,1 CP BP)
		(right-arguments/if AP2 AP1)
		R
	<- argument-soundness CP AP1 R.

argument-soundness/if,2 : argument-soundness
		(eval-cmd/if,2 CP BP)
		(right-arguments/if AP2 AP1)
		R
	<- argument-soundness CP AP2 R.

argument-soundness/semi,1 : argument-soundness
		(eval-cmd/semi,1 CP2 CP1)
		(right-arguments/semi AP2 AP1)
		R
	<- argument-soundness CP2 AP2 R.

argument-soundness/semi,2 : argument-soundness
		(eval-cmd/semi,2 CP)
		(right-arguments/semi AP2 AP1)
		R
	<- argument-soundness CP AP1 R.

argument-soundness/semi,3 : argument-soundness
		(eval-cmd/semi,3 CP)
		(right-arguments/semi AP2 AP1)
		store-or-return/res.

argument-soundness/assign : argument-soundness
		(eval-cmd/assign SR EP VM)
		right-arguments/assign
		store-or-return/store.

argument-soundness/funcall,1 : argument-soundness
		(eval-cmd/funcall,1 _ _ _ _ _ _)
		(right-arguments/funcall EELL AE)
		store-or-return/store.

argument-soundness/funcall,2,1 : argument-soundness
		(eval-cmd/funcall,2 SRCONV BP DECENVM EVALEL)
		(right-arguments/funcall EVALLL (AE : arityenv _ K))
		Q
	<- explist-lemma-1 EVALEL EVALLL (NLS : natlist-size _ K)
	<- checkenv AE DECENVM CPB
	<- parbind-soundness F BP CPB NLS R
	<- sr-contradict R V
	<- void-s-or-r _ V Q.

argument-soundness/funcall,2,2 : argument-soundness
		(eval-cmd/funcall,2 SR BP DECM EEEL)
		(right-arguments/funcall EELL AE)
		Q
	<- explist-lemma-1 EEEL EELL NLS
	<- checkenv AE DECM CPB
	<- parbind-soundness F BP CPB NLS R
	<- sr-contradict-2 R V
	<- void-s-or-r _ V Q.

%%% Formulation of main soundness theorem.
fresult-res : fresult -> type.

fresult-res/res : fresult-res (fresult/n N).

command-soundness :
	(eval-cmd C S S^) -> (check-command C) -> (sresult-res S^) -> type.
%mode command-soundness +EP +CP -SR.

command-soundness,1 : command-soundness
		EP
		(check-command,1 RA MR)
		R
	<- return-soundness MR EP P
	<- argument-soundness EP RA Q
	<- result-coerce Q P R.

localbind-soundness : {F : fvar} (bind-locals LB S S^) -> (check-locbind F LB K)
	-> (sresult-res S^) -> type.
%mode localbind-soundness +F +BL +CP -SR.

localbind-soundness/nil : localbind-soundness F
		(bind-locals/nil EP)
		(check-locbind/nil  CP)
		R
	<- command-soundness EP CP R.

localbind-soundness/cons : localbind-soundness F
		(bind-locals/cons BL SA SL)
		(check-locbind/cons RP)
		R
	<- ({x : var} {vm : varenv-map x L}
		localbind-soundness F (BL x vm) (RP x) R).

parbind-soundness/nil : parbind-soundness F
		(bind-pars/nil BL)
		(check-parbind/nil CL)
		natlist-size/nil
		R
	<- localbind-soundness F BL CL R.

parbind-soundness/cons : parbind-soundness F
		(bind-pars/cons BP SA SL)
		(check-parbind/cons CP)
		(natlist-size/cons NLS')
		R
	<- ({x : var} {vm : varenv-map x L}
		parbind-soundness F (BP x vm) (CP x) NLS' R).

program-soundness : (eval-program P NL R) -> (natlist-size NL K) ->
	(check-program P K) -> (sresult-res R) -> type.

%mode program-soundness +EP +NLS +CP -R.

program-soundness/main,1 : program-soundness
		(eval-program/main EP)
		(NLS : natlist-size _ K)
		(check-program/main CP)
		Q
	<- ({f : fvar} {dm : decenv-map f (D f)} {ae : arityenv f K}
			{ce : checkenv ae dm (CP f ae)}
		parbind-soundness f (EP f dm) (CP f ae) NLS Q).

program-soundness/cons : program-soundness
		(eval-program/cons RP)
		NLS
		(check-program/cons CP CPB)
		S
	<- ({f : fvar} {dm : decenv-map f (D f)} {ae : arityenv f K}
			checkenv ae dm ((CPB f ae) : check-parbind _ _ _ K) ->	
		program-soundness  (RP f dm) NLS (CP f ae) S).

%worlds (varenv-block) (explist-lemma-1 _ _ _).
%total E (explist-lemma-1 E _ _).

%worlds (varenv-block | checkenv-block) (return-soundness _ _ _).
%total E (return-soundness E _ _).

%worlds (varenv-block | checkenv-block)
	(argument-soundness _ _ _)
	(command-soundness _ _ _)(checkenv _ _ _)
	(parbind-soundness _ _ _ _ _)(program-soundness _ _ _ _)
	(localbind-soundness _ _ _ _).

%total (T E E1 E2 E3 E4)
	(argument-soundness E4 _ _)
	(command-soundness E3 _ _)(checkenv _ T _)
	(localbind-soundness _ E2 _ _)
	(parbind-soundness _ E1 _ _ _)
	(program-soundness E _ _ _).