Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
%%% 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 _ _ _).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment