Syntax:
i ::= 0 | 1 | -1 | ... // integers
c ::= () | i | // constants
| l | (!_t) | (:=_t) | sel_t | upd_t // state constants
| fix_pure_tx_t'_t''| fix_omega_tx_t' // fixpoint constants
| alloc_t | contains_t // heap allocation and containment
H ::= // heap
| .
| l |-> v, H
v ::= // values
| c // constant
| asHeap H // heaps
| fun (x:t) -> e // lambda
| let rec (f^d:t) x = e // fixpoint
| sel_t v1 // partially applied sel
| upd_t v1 | upd_t v1 v2 // partially applied upd
| (:=_t) v // partially applied write
| contains_t v
| alloc_t v1 // partially applied contains and alloc
| fix_pure_tx_t'_t'' wp
| fix_pure_tx_t'_t'' wp d
| fix_pure_tx_t'_t'' wp d F // partially applied fix_pure
| fix_omega_tx_t' wp
| fix_omega_tx_t' wp F // partially applied fix_omega
e ::= // expressions
| x // variable
| v // value
| e1 e2 // application
| if0 e then e1 else e2 // zero test
d ::= epsilon | e // optional metric
M ::= PURE | ALL // effects
// these are fixed. in addition user
// can define more (explained below)
T ::= // type constants
| unit | int | ref | heap // some type constants
| false | and // some logical constants
| forall // forall over expressions of a type
| forall_k // forall over the types with kind k
| eq // expression equality
| eq_k // type equality at kind k
| precedes // well-founded ordering
t,phi,wp ::= // types
| a // type variable
| T // type constant
| x:t1 -> M t2 phi // dependent function type
| fun (a:k) -> t // type-to-type function
| fun (x:t1) -> t2 // expression-to-type function
| t1 t2 // type applied to type
| t e // type applied to expression
k ::= // kinds
| Type // regular types
| a:k -> k' // type-indexed type constructor
| x:t -> k' // expression-indexed type constructor
================================================================================
Syntactic sugar:
We write (forall (x:t). b) for (forall t (fun (x:t) -> b))
Derived logical constants:
(a ==> b) = (forall (_:a). b)
~t = (t ==> false)
true = ~false
(a \/ b) = (~a ==> b)
We view H as a partial map from locations to values. We write H(l) and
H[l -> v] to select and update H. Note that H(l) is partial and defined
only if l is in dom(H).
================================================================================
Reduction:
We have 3 judgments:
t ~> t' and e ~> e' - are mutually inductively defined and evaluate
types and pure expressions
(e ~> e' is really just an auxiliary for defining
type reduction and thus type conversion)
(H,e) ~> (H',e') - evaluates expressions, including impure ones
using call-by-value reduction (the small-step
operational semantics of F*)
___________________________
| |
| t ~> t' (Type reduction) |
|___________________________|
(fun (x:t) -> t') e ~> t'[e/x] [TS-EBeta]
(fun (a:k) -> t') t ~> t'[t/a] [TS-TBeta]
t1 ~> t1'
--------------------------------------- [TS-ArrT1]
(x:t1 -> M t2 wp) ~> (x:t1' -> M t2 wp)
t1 ~> t1'
--------------- [TS-TAppT1]
t1 t2 ~> t1' t2
t2 ~> t2'
--------------- [TS-TAppT2]
t1 t2 ~> t1 t2'
t ~> t'
----------- [TS-EAppT]
t e ~> t' e
e ~> e'
----------- [TS-EAppE]
t e ~> t e'
t ~> t'
------------------------------------- [TS-TLamT]
(fun (a:k) -> t) ~> (fun (a:k) -> t')
t1 ~> t1'
----------------------------------------- [TS-ELamT1]
(fun (x:t1) -> t2) ~> (fun (x:t1') -> t2)
______________________________________
| |
| e ~> e' (Pure expression reduction) |
|______________________________________|
(fun (x:t) -> e) e' ~> e[e'/x] [PS-Beta]
fix_pure_tx_t'_t'' wp d F v ~> F (fix_pure_tx_t'_t'' wp F) v [PS-FixPure]
if0 0 then e1 else e2 ~> e1 [PS-If0]
i <> 0
--------------------------- [PS-IfS]
if0 i then e1 else e2 ~> e2
e1 ~> e1'
--------------- [PS-AppE1]
e1 e2 ~> e1' e2
e2 ~> e2'
--------------- [PS-AppE2]
e1 e2 ~> e1 e2'
t ~> t'
------------------------------------- [PS-LamT]
(fun (x:t) -> e) ~> (fun (x:t') -> e)
t ~> t'
--------------------------------------------------- [PS-LetRecT]
(let rec (f^d:t) x = e) ~> (let rec (f^d:t') x = e)
d ~> d'
--------------------------------------------------- [PS-LetRecD]
(let rec (f^d:t) x = e) ~> (let rec (f^d':t) x = e)
e0 ~> e0'
----------------------------------------------------- [PS-If0E0]
(if0 e0 then e1 else e2) ~> (if0 e0' then e1 else e2)
sel (asHeap H) l ~> H(l) [PS-Sel]
upd (asHeap H) l i ~> asHeap (H[l<-i]) [PS-Upd]
b = true if l in dom(H), false otherwise
----------------------------------------- [PS-Contains]
contains (asHeap H) l ~> b
______________________________________________
| |
| (H, e) ~> (H', e') (Call-by-value reduction) |
|______________________________________________|
l notin dom(H) meta l = q
--------------------------------- [IS-Alloc]
(H, alloc q v) ~> (H[l -> v], l)
(See "Heap modeling" below for explanation of meta)
(H, (!_t) l) ~> (H, H(l)) [IS-Read]
(H, l :=_t v) ~> (H[l -> v], ()) [IS-Write]
(H, (fun (x:t) -> e) v) ~> (H, e[v/x]) [IS-Beta]
(H, fix_pure_tx_t'_t'' wp d F v) ~>
(H, F v (fix_pure_tx_t'_t'' wp F)) [IS-FixPure]
(H, fix_omega_tx_t' wp F v) ~>
(H, F v (fix_omega_tx_t' wp F)) [IS-FixOmega]
(H, if0 0 then e1 else e2) ~> (H, e1) [IS-If0]
i <> 0
------------------------------------- [IS-IfS]
(H, if0 i then e1 else e2) ~> (H, e2)
(H, e1) ~> (H', e1')
-------------------------- [IS-AppE1]
(H, e1 e2) ~> (H', e1' e2)
(H, e2) ~> (H', e2')
------------------------ [IS-AppE2]
(H, v e2) ~> (H', v e2')
(H, e0) ~> (H', e0')
------------------------------------------------------------ [IS-If0E0]
(H, if0 e0 then e1 else e2) ~> (H', if0 e0' then e1 else e2)
(H', sel (asHeap H) l) ~> (H', H(l)) [IS-Sel]
(H', upd (asHeap H) l v) ~> (H', asHeap (H[l->v])) [IS-Upd]
b = true if l in dom(H), false otherwise
----------------------------------------- [IS-Contains]
(H, contains (asHeap H) l) ~> (H, b)
================================================================================
Type system:
The type system has 8 mutually inductively defined judgments:
(1) expression typing: G |- e : M t wp
(2) sub-computation: G |- e : M t wp <: M' t' wp'
(3) sub-typing: G |- t <: t'
(4) kinding: G |- t : k
(5) sub-kinding: G |- k <: k'
(6) kind well-formedness: G |- k ok
(7) logical validity (including type conversion): G |= t
(8) environment well-formedness: G |- ok
--------------------------------------------------------------------------------
Environments are lists of binders and location typings:
G ::= . | G, x:t | G, a:k | G, l:t
--------------------------------------------------------------------------------
Kinds for type constants (T : k_T):
unit : Type
int : Type
ref : Type -> Type
heap : Type
false : Type
and : Type -> Type -> Type
forall : a:Type -> (a -> Type) -> Type
eq : a:Type -> a -> a -> Type
precedes : a:Type -> b:Type -> a -> b -> Type
eq_k : a1:k -> a2:k -> Type
forall_k : (a:k -> Type) -> Type
Note: because of the lack of kind polymorphism eq_k and forall_k are
infinitely many constants, an equality and a universal
quantifier for each kind k.
Derived logical constants:
true : Type
not : Type -> Type
or : Type -> Type -> Type
impl : Type -> Type -> Type
--------------------------------------------------------------------------------
Heap modeling:
We provide a logical model of the native heap using the (logical) type heap and
functions:
sel_t : heap -> ref t -> Tot t
upd_t : heap -> ref t -> t -> Tot heap
contains_t: heap -> ref t -> Tot bool
(TinyF* does not have polymorphism, hence we assume that sel_t, upd_t, and
contains_t are infinitely many constants. The pattern also shows up below
for !, :=, and alloc. Of course, in full F*, these have the usual polymorphic
types)
The semantics of these functions is axiomatized in the logic using rules
V-SelEq and V-SelNeq.
We bring the meta-level heap H to logic using an uninterpreted function asHeap
that takes a meta-level heap H as input and returns a value of type heap.
However, the programmer is not tied to the native heap model for reasoning
about state. Indeed, the programmer is allowed to choose a memory model
and write (and verify) specs using that memory model. We require some sanity
checks on the memory model to ensure its soundness (w.r.t. the operational semantics).
The programmer provided memory model MUST provide the following interface:
type mem
type mem_meta_data // meta_data that programmer wants to associate with each ref
msel_t : mem -> ref t -> Tot t
mupd_t : mem -> ref t -> t -> Tot mem
mcontains_t: mem -> ref t -> Tot bool
meta_t : ref t -> mem_meta_data
and MUST provide the following memory model axiom about the semantics
of these functions:
mcontains_t (mupd_t m l v) l /\
msel_t (mupd_t m l v) l = v /\
forall l' <> l. mcontains_t (mupd_t m l v) l' = mcontains_t m l' /\
msel_t (mupd_t m l v) l' = msel_t m l'
--------------------------------------------------------------------------------
Types for expression constants except locations (c : t_c):
(Locations are typed using store typing as usual)
(Also see "Requirements on lattice" below for types of '!' and ':=')
() : unit
0, 1, -1, ... : int
alloc_t: q:meta_data -> x:t ->
ALL (ref t) (fun p h -> forall l. not (contains h l) /\ meta h l = q
==> p l (mupd h l x))
(!_t) : x:ref t -> ALL t (fun p h -> p (msel h x) h)
(:=_t) : x:ref t -> y:t -> ALL unit (fun p h -> p () (mupd h x y))
fix_pure_tx_t'_t'' : wp:(x:tx->K_PURE(t'' x)) -> d:(x:tx -> Tot (t' x)) ->
F:(x:tx -> f: (y:tx -> PURE (t'' y)
(up_PURE (precedes (d y) (d x)) /\_PURE (wp y)))
-> PURE (t'' x) (wp x)) ->
Tot t (where t = y:tx -> PURE (t'' y) (wp y))
fix_omega_tx_t' : wp:(x:tx->K_ALL(t' x)) ->
F:(x:tx -> f:t -> ALL (t' x) (wp x)) -> Tot t
(where t = y:tx -> ALL (t' y) (wp y))
where Tot t = PURE t (fun p -> forall (x:t). p x)
Note: because of the lack polymorphism in TinyF* (!_t), (:=_t), alloc_t,
fix_pure_tx_t'_t'' and fix_omega_tx_t' are infinitely many constants.
This problem will go away as soon as we add polymorphism, which is present
of course in full F*. The kinds of tx, t', and t'' are as follows:
tx:Type, t':(tx->Type), t'':(tx->Type)
--------------------------------------------------------------------------------
We assume abstract type mem for programmer chosen memory model.
Lattice of effects: We assume an arbitrary lattice of effects with the bottom of
lattice fixed as PURE and the top of lattice fixed as ALL.
In the middle programmer can define arbitrary effects. Here
we provide the specs for PURE and ALL. After this, we would
specify the requirements on the user defined
lattice and lifts.
-- Kinds
Pre_PURE = Type
Pre_ALL = mem -> Type
Post_PURE(t:Type) = t -> Type
Post_ALL (t:Type) = t -> mem -> Type
K_M(t) = Post_M(t) -> Pre_M
-- Operations inside monads
return_M : #a:Type -> x:a -> K_M a
return_PURE #a x p = p x
return_ALL #a x p h = p x h
bind_M : #a:Type -> #b:Type -> K_M a -> (x:a -> K_M b) -> K_M b
bind_PURE #a #b wp f p = wp (fun x -> f x p)
bind_ALL #a #b wp f p h = wp (fun x h' -> f x p h') h
monotonic_M: #a:Type -> K_M(a) -> Type
monotonic_PURE #a wp = forall p1 p2. (forall x. p1 x ==> p2 x) ==> (wp p1 ==> wp p2)
monotonic_ALL #a wp = forall p1 p2. (forall x h. p1 x h ==> p2 x h) ==> (forall h. wp p1 h ===> wp p2 h)
Say op : Type -> Type -> Type.
op_M: #a:Type -> K_M a -> K_M a -> K_M a
op_PURE #a wp1 wp2 p = (wp1 p) op (wp2 p)
op_ALL #a wp1 wp2 p h = (wp1 p h) op (wp2 p h)
up_M: #a:Type -> Type -> K_M a
up_PURE #a t p = t
up_ALL #a t p h = t
down_M : #a:Type -> K_M(a) -> Type
down_PURE #a wp = forall p. wp p
down_ALL #a wp = forall p h. wp p h
ite_M: #a:type -> K_M int -> K_M a -> K_M a -> K_M a
ite_M #a wp0 wp1 wp2 = bind_M wp0 (fun b ->
(up_M (i = 0) ==>_M wp1) /\_M
(up_M (i != 0) ==>_M wp2))
-- Operations between monads, in the lattice
lift_M_M': #a:Type -> K_M a -> K_M' a
lift_PURE_ALL #a wp p h = wp (fun x -> p x h)
It is easy to check that all the operations on WPs preserve monotonicity.
For example:
monotonic_M a wp1
/\ forall (x:a). monotonic b (wp2 x)
==> monotonic_M b (bind_M a b wp1 wp2)
And also that the lift_PURE_ALL satisfies the monad morphism laws.
--------------------------------------------------------------------------------
Requirements on lattice:
-- lifts should be monad morphisms
-- lifts should preserve monotonicity
-- lifts should commute over wp ops, i.e.
lift_M_M' (wp1 op_M wp2) = (lift_M_M' wp1) op_M' (lift_M_M' wp2)
-- lifts should preserve down_M validity, i.e.
If G |= down_M wp, then G |= down_M' (lift_M_M' wp)
-- M < M' < M'', then
lift_M_M'' wp = lift_M'_M'' (lift_M_M' wp)
!_t, :=_t, and alloc_t can be typed anywhere in the lattice (except PURE),
as long as:
-- . |- !_t: x:ref t -> M t wp as long as
x:ref t |= down_ALL (lift_M_ALL wp <==>_ALL (fun p h -> p (msel h x) h))
-- . |- :=_t x:ref t -> y:t -> M unit wp as long as
x:ref t, y:t |= down_ALL (lift_M_ALL wp <==>_ALL (fun p h -> p () (mupd h x y)))
-- . |- alloc : q:meta_data -> x:t -> M (ref t) wp as long as
x:t, q:meta_data |= down_ALL (lift_M_ALL wp <==> forall l. not (contains h l) /\ meta h l = q
==> p l (mupd h l x))
Illustrations of the lattice (assuming heap as the memory model):
Reader monad:
-------------
Pure < Reader < ALL
Pre_Reader = heap -> Type
Post_Reader (a:Type) = a -> Type
return_Reader (a:Type) (x:a) = fun p -> p x h0
bind_Reader (a:Type) wp1 wp2 = fun p h0 -> wp1 (fun x -> (wp2 x) p h0) h0
down_Reader (a:Type) wp = forall p h. wp p h
lift_Pure_Reader (a:Type) wp = fun p h0 -> wp p
lift_Reader_ALL (a:Type) wp = fun p h0 -> wp (fun x -> p x h0) h0
Verify: lift_Pure_ALL wp = lift_Reader_ALL (lift_Pure_Reader wp)
R.H.S. =
lift_Reader_ALL (fun p_reader h0 -> wp p_reader)
(let wp_reader = (fun p_reader h0 -> wp p_reader))
= fun p_all h0 -> wp_reader (fun x -> p_all x h0) h0
= fun p_all h0 -> wp (fun x -> p_all x h0)
= L.H.S. (Qed)
Verify: Commutation for M = Pure, M' = Reader. let lift = lift_Pure_Reader
Given: G |= down_Reader (wp ==>_Reader (lift wp')) -- (1)
G |= down_Pure (wp' ==>_Pure wp'') -- (2)
To prove: G |= down_Reader (wp ==>_Reader (lift wp''))
Expanding (1):
G |= forall p, h. wp p h ==> wp' p -- (3)
Expanding (2):
G |= forall p. wp' p ==> wp'' p -- (4)
Expanding (3), our goal is:
G |= forall p, h. wp p h ==> wp'' p
Use quantifier elims (for p and h), modes ponens, and quantifier intros on (3) and (4) to get goal. (Qed)
Verify: Commutation for M = Reader, M' = ALL. let lift = lift_Reader_ALL
Given: G |= down_ALL (wp ==>_ALL (lift wp')) -- (1)
G |= down_Reader (wp' ==>_Reader wp'') -- (2)
To prove: G |= down_ALL (wp ==>_ALL (lift wp''))
Expanding (1):
G |= forall p, h. wp p h ==> wp' (fun x -> p x h) h -- (3)
Expanding (2):
G |= forall p, h. wp' p h ==> wp'' p h -- (4)
Expanding (3), our goal is:
G |= forall p, h. wp p h ==> wp'' (fun x -> p x h) h
On (3) instantiate p with (fun x -> p x h), then similar to Pure_Reader case. (Qed)
Typing constants in Reader monad:
! : x:ref int -> Reader int (fun p h -> p (sel h x))
Verify: . |= down_ALL (lift_Reader_ALL wp ==>_ALL (fun p h -> p (sel h x) h))
lift_Reader_ALL wp = fun p h -> p (sel h x) h (Qed)
Writer monad:
-------------
Pure < Reader < Writer < ALL
Pre_Writer = heap -> Type
Post_Writer (a:Type) = a -> heap -> set ref -> Type
let sub_heap h0 s h1 = forall r. r in dom(h0) /\ r notin s ==>
sel h1 r = sel h0 r
let {} = empty set
let s1 ++ s2 = union s1 s2
return_Writer (a:Type) (x:a) = fun p h0 -> p x h0 {}
bind_Writer (a:Type) wp1 wp2 =
fun p h0 -> wp1 (fun y h1 s1. sub_heap h0 s1 h1 ==>
(wp2 x) (fun y h2 s2. sub_heap h1 s2 h2 ==>
p y h2 (s1 ++ s2)))
down_Writer (a:Type) wp = forall p, h, s. wp p h s
lift_Pure_Writer wp = fun p h0 -> wp (fun x -> p x h0 {})
lift_Reader_Writer wp = fun p h0 -> wp (fun x -> p x h0 {}) h0
lift_Writer_ALL wp = fun p h0 -> wp (fun x h1 s1 -> p x h1) h0
Verify: lift_Pure_Writer wp = lift_Reader_Writer (lift_Pure_Reader wp)
R.H.S. =
lift_Reader_Writer (fun p_reader h0 -> wp p_reader)
(let wp_reader = (fun p_reader h0 -> wp p_reader)
= fun p_writer h0 -> wp_reader (fun x -> p_writer x h0 {}) h0
= fun p_writer h0 -> wp (fun x -> p_writer x h0 {})
= L.H.S. (Qed)
Verify: lift_Pure_ALL wp = lift_Writer_ALL (lift_Pure_Writer wp)
R.H.S. =
lift_Writer_ALL (fun p_writer h0 -> wp (fun x -> p_writer x h0 {})
(let wp_writer = fun p_writer h0 -> wp (fun x -> p_writer x h0 {}))
= fun p_all h0 -> wp_writer (fun x h1 s1 -> p_all x h1) h0
= fun p_all h0 -> wp (fun x -> p_all x h0)
= L.H.S. (Qed)
Verify: Commutation for M = Reader, M' = Writer. let lift = lift_Reader_Writer
Given: G |= down_Writer (wp ==>_Writer (lift wp')) -- (1)
G |= down_Reader (wp' ==>_Reader wp'') -- (2)
To prove: G |= down_Writer (wp ==>_Writer (lift wp''))
Expanding (1):
G |= forall p, h, s. wp p h s ==> wp' (fun x -> p x h {}) h -- (3)
Expanding (2):
G |= forall p, h. wp' p h ==> wp'' p h -- (4)
Expanding (3), our goal is:
G |= forall p, h, s. wp p h s ==> wp'' (fun x -> p x h {}) h
On (3) instantiate p with (fun x -> p x h {}), then similar to Pure_Reader case. (Qed)
Verify: Commutation for M = Writer, M' = ALL. let lift = lift_Writer_ALL
Given: G |= down_ALL (wp ==>_ALL (lift wp')) -- (1)
G |= down_Writer (wp' ==>_Writer wp'') -- (2)
To prove: G |= down_ALL (wp ==>_ALL (lift wp''))
Expanding (1):
G |= forall p, h. wp p h ==> wp' (fun x h1 s1 -> p x h1) h -- (3)
Expanding (2):
G |= forall p, h, s. wp' p h s ==> wp'' p h s -- (4)
Expanding (3), our goal is:
G |= forall p, h. wp p h ==> wp'' (fun x h1 s1 -> p x h1 {}) h
On (3) instantiate p with (fun x h1 s1 -> p x h1), then similar to Pure_Reader case. (Qed)
Typing constants in Writer monad:
! : x:ref int -> Writer int (fun p h -> p (sel h x) h {})
Verify: . |= down_ALL (lift_Writer_ALL wp ==>_ALL (fun p h -> p (sel h x) h))
lift_Writer_ALL wp = fun p h -> p (sel h x) h (Qed)
--------------------------------------------------------------------------------
Expression typing (G |- e : M t wp):
e = x \/ e = l
G, e:t, G' |- ok
----------------------- [T-Var]
G, e:t, G' |- e : Tot t
G |- ok
---------------- [T-Const]
G |- c : Tot T_c
G |- t1 : Type
G, x:t1 |- e : M t2 wp
--------------------------------------------- [T-Abs]
G |- fun (x:t1) -> e : Tot (x:t1 -> M t2 wp)
G |- e0 : M int wp0
G |- e1 : M t wp1
G |- e2 : M t wp2
------------------------------------------------------ [T-If]
G |- if0 e0 then e1 else e2 : M t (ite_M wp0 wp1 wp2)
G |- e1 : M (x:t -> M t' wp) wp1
G |- e2 : M t wp2
x in FV t' ==> wp2=return_M e2 /\ G |- e2 : Tot t
-------------------------------------------------------------------- [T-App]
G |- e1 e2 : M (t'[e2/x]) (bind_M #(x:t -> M t' wp) #(t'[e2/x])
wp1
(fun _ -> bind_M #t #(t'[e2/x])
wp2 (fun (x:t) -> wp)))
(Remark: In the paper we split this T-App rule into two rules
T-App1 and T-App2 for clarity. The split happens on the condition
x in FV t'. If x in FV t', we write the result bind as bind_M
(wp1 (fun _ -> wp[e2/x])), which is what we get after reducing
bind_M wp2 (fun (x:t) -> wp)) one step.)
G |- e : Tot t
------------------------------- [T-Ret]
G |- e : PURE t (return_PURE e)
G |- e : M' t' wp'
G |- M' t' wp' <: M t wp
------------------------- [T-Sub]
G |- e : M t wp
--------------------------------------------------------------------------------
Sub-computations (G |- M' t' wp' <: w t wp):
M' <= M
G |- t' <: t
G |- wp : K_M(t)
G |= monotonic_M t wp
G |- wp' : K_M(t')
G |= monotonic_M t' wp'
G |= down_M (wp ==>_M (lift_M'_M wp'))
-------------------------------------- [S-Comp]
G |- M' t' wp' <: M t wp
--------------------------------------------------------------------------------
Sub-typing (G |- t' <: t):
G |= t' =_Type t
G |- t : Type
G |- t' : Type
---------------- [Sub-Conv]
G |- t' <: t
G |- t <: t'
G, x:t |- M' s' wp' <: M s wp
G |- (x:t' -> M' s' wp') ok
------------------------------------------- [Sub-Fun]
G |- (x:t' -> M' s' wp') <: (x:t -> M s wp)
G |- t1 <: t2
G |- t2 <: t3
------------- [Sub-Trans]
G |- t1 <: t3
--------------------------------------------------------------------------------
Kinding (G |- t : k):
G |- ok
------------- [K-Var]
G |- a : G(a)
G |- K_T ok need to check this because of eq_k and forall_k
------------ [K-Const]
G |- T : K_T
G |- t1 : Type
G, x:t1 |- t2 : Type
G, x:t1 |- wp : K_M(t2)
G, x:t1 |= monotonic_M t2 wp
---------------------------- [K-Arr]
G |- x:t1 -> M t2 wp : Type
G |- k ok
G, a:k |- t : k'
----------------------------------- [K-TLam]
G |- (fun (a:k) -> t) : (a:k -> k')
G |- t1 : Type
G, x:t1 |- t2 : k2
-------------------------------------- [K-ELam]
G |- (fun (x:t1) -> t2) : (x:t1 -> k2)
G |- t1 : a:k -> k'
G |- t2 : k
G |- k'[t2/a] ok
--------------------- [K-TApp]
G |- t1 t2 : k'[t2/a]
G |- t : x:t' -> k
G |- e : Tot t'
G |- k[e/x] ok
------------------ [K-EApp]
G |- t e : k[e/x]
G |- t : k'
G |- k' <: k
------------ [K-Sub]
G |- t : k
--------------------------------------------------------------------------------
Sub-kinding (G |- k1 <: k2):
G |- k ok
----------- [KSub-Refl]
G |- k <: k
G |- k2 <: k1
G, a:k2 |- k1' <: k2'
G |- a:k1 -> k1' ok
------------------------------- [KSub-KArr]
G |- a:k1 -> k1' <: a:k2 -> k2'
G |- t2 <: t1
G, x:t2 |- k1 <: k2
G |- x:t1 -> k1 ok
----------------------------- [KSub-TArr]
G |- x:t1 -> k1 <: x:t2 -> k2
--------------------------------------------------------------------------------
Kind well-formedness (G |- k ok):
G |- ok
------------ [KOk-Type]
G |- Type ok
G |- t : Type
G, x:t |- k' ok
----------------- [KOk-TArr]
G |- x:t -> k' ok
G |- k ok
G, a:k |- k' ok
----------------- [KOk-KArr]
G |- a:k -> k' ok
--------------------------------------------------------------------------------
Validity (G |= phi):
We represent logical validity as yet another inductive judgment
(mutually inductive with all the others).
G |- e : Pure t wp
------------------------------------------------------ [V-Construct]
G |= forall post:Post_PURE(t). wp post ==> t /\ post e
G |- e : Tot t
G |- e' : Tot t
e ~> e'
--------------- [V-RedE]
G |= e = e'
G |- e : Tot t
-------------- [V-EqReflE]
G |= e = e
G |= e1 = e2 this rule might force equality to be homogeneous
G |- e1 : Tot t'
G |- e2 : Tot t'
G, x:t' |- t : Type
G |= t[e1/x]
------------------- [V-SubstE]
G |= t[e2/x]
G |- t : k
G |- t' : k
t ~> t'
------------- [V-RedT]
G |= t =_k t'
G |- t : k
------------ [V-EqReflT]
G |= t =_k t
G |= t1 =_k t2
G, a:k |- t : Type
G |= t{t1/a}
------------------ [V-SubstT]
G |= t{t2/a}
G |- eh : Tot heap
G |- el : Tot (ref t)
G |- ei : Tot t
------------------------------------ [V-SelEq]
G |= sel_t (upd_t eh el ei) el = ei /\
contains_t (upd_t eh el ei) el
G |- eh : Tot heap
G |- el : Tot (ref t)
G |- el' : Tot (ref t)
G |- ei : Tot t
G |= ~(el = el')
------------------------------------------------------ [V-SelNeq]
G |= sel_t (upd_t eh el' ei) el = sel_t eh el /\
contains_t (upd_t eh el' ei) el = contains_t eh el
G, x:t |= phi
---------------------- [V-ForallIntro]
G |= forall (x:t). phi
G, a:k |= phi
------------------------ [V-ForallTypIntro]
G |= forall_k (a:k). phi
G |= forall (x:t). phi
G |- e : Tot t
---------------------- [V-ForallElim]
G |= phi[e/x]
G |= forall_k (a:k). phi
G |- t : k
------------------------ [V-ForallTypElim]
G |= phi[t/a]
G |= p1 /\ p2
------------- [V-AndElim1]
G |= p1
G |= p1 /\ p2
------------- [V-AndElim2]
G |= p2
G |- t1 G |- t2
------------------ [V-AndIntro]
G |= t1 /\ t2
G, x:t1 |= t3
G, x:~t1 |= t3
G |- t3 : Type
-------------- [V-ExMiddle]
G |= t3
G |= false
G |- t : Type
------------- [V-FalseElim]
G |= t
v1 << v2
G |- v1 : Tot t1
G |- v2 : Tot t2
------------------- [V-PrecedesIntro]
G |= precedes v1 v2
where v1 << v2 = { i1 < i2, if v1 = i1, i1 >= 0, v2 = i2, and i2 >= 0
{ false, otherwise
G |- c1 : Tot t
G |- c2 : Tot t
c1 <> c2
--------------- [V-DistinctC]
G |= ~(c1 = c2)
G |- T_h \bar{tau} : Type
G |- T_h' \bar{tau}' : Type
T_h <> T_h'
-------------------------------------------- [V-DistinctTH]
G |= ~(T_h \bar{tau} =_Type T_h' \bar{tau}')
where T_h ::= ->PURE | ->ALL | T // type head
tau ::= e | t // expression or type
G |= T_h \bar{tau} =_Type T_h \bar{tau}'
---------------------------------------- [V-InjTH]
G |= tau_i =_Type tau_i'
--------------------------------------------------------------------------------
Environment well-formedness (G |- ok)
. |- ok [G-Empty]
G |- t : Type x not in dom G
------------------------------- [G-Type]
G, x:t |- ok
G |- k ok a not in dom G
--------------------------- [G-Kind]
G, a:k |- ok
--------------------------------------------------------------------------------
Heap typing (G |- H)
We use ldom(G) to denote the set of locations that have binding in G.
ldom(G) = .
------------- [TH-Emp]
G |- .
G = G', l : ref t, G''
G', G'' |- H
G |- v : M t wp
---------------------- [TH-Ind]
G |- l -> v, H
--------------------------------------------------------------------------------
Derived typing rules
Fixpoints
Note: The encoding for fix needs to be done by translating typing
derivations, because it relies on types that are not present in the syntax.
let rec (f^d:t) x = e
=def
fix_pure_tx_t'_t'' wp d (fun (x:tx) ->
fun (f: (y:tx -> PURE t'' (up_PURE (precedes (d y) (d x))
/\_PURE (wp y)))) -> e)
G |- t : Type
G |- d : Tot (x:tx -> Tot t')
t = y:tx -> PURE t'' wp
G, x:tx, f: (y:tx -> PURE t'' (up_PURE (precedes (d y) (d x)) /\_PURE wp))
|- e : (PURE t'' wp[x/y])
---------------------------------------------------------------- [T-Fix]
G |- let rec (f^d:t) x = e : Tot t
let rec (f:t) x = e
=def
fix_omega_tx_t' wp (fun (x:tx) -> (fun f:(y:tx -> ALL (t' y) (wp y)) -> e))
G |- t : Type
t = y:tx -> ALL t' wp
G, x:tx, f:t |- e : (ALL t' wp[x/y])
------------------------------------ [T-FixOmega]
G |- let rec (f:t) x = e : Tot t
(H, (let rec (f^d:t) x = e) v) ~>*
(H, e[v/x][(let rec (f^d:t) x = e)/f]) [IS-LetRec]
--------------------------------------------------------------------------------
Derived validity rules
G, x:t, G' |- ok
---------------- [V-Assume]
G, x:t, G' |= t
G |= e1 = e2
G |= e2 = e3
-------------- [V-EqTranE]
G |= e1 = e3
G |= e1 = e2
-------------- [V-EqSymE]
G |= e2 = e1
G |= t1 =_k t2
G |= t2 =_k t3
-------------- [V-EqTranT]
G |= t1 =_k t3
G |= t1 =_k t2
-------------- [V-EqSymT]
G |= t2 =_k t1
G |- ok
--------- [V-True]
G |= true
G, x:t1 |= t2
G |- t1 ==> t2 : Type
---------------------- [V-ImplIntro]
G |= t1 ==> t2
G |= t1 ==> t2
G |= t1
-------------- [V-ImplElim]
G |= t2
G |= t1
G |- t2 : Type
-------------- [V-OrIntro1]
G |= t1 \/ t2
G |= t2
G |- t1 : Type
-------------- [V-OrIntro2]
G |= t1 \/ t2
G |= t1 \/ t2
G, x:t1 |= t3
G, x:t2 |= t3
G |- t3 : Type
-------------- [V-OrElim]
G |= t3
Deriving [V-OrElim] from [V-ExMiddle]:
------- premise
G |= ~t1 ==> t2 G, x:t2 |= t3 G |- t3 : Type
--------assume -----------weakening ----------------------- V-ImplIntro
G,~t1 |= ~t1 G,~t1 |= ~t1 ==> t2 G |= t2 ==> t3
----------------------------- V-ImplElim ------------------ weakening
G,~t1 |= t2 G,~t1 |= t2 ==> t3
------premise ------------------------------------------- ------- premise
G, x:t1 |= t3 G, x:~t1 |= t3 G |- t3 : Type
------------------------------------------------------------------ V-ExMiddle'
G |= t3
G |- t : Type
------------- [V-ExMiddle']
G |= t \/ ~t
================================================================================
Proofs:
Notation: When we want to focus on the typing environment for all
judgments we use the notation G |- J. Formally, this stands
for any of the 8 judgments of our type system:
G |- e : M t wp,
G |- M' t' wp' <: M t wp,
G |- t' <: t,
G |- t : k,
G |- k <: k'
G |- k ok
G |= phi
G |- ok
let app_M wp1 wp2 wp = bind_M wp1 (fun f -> bind_M wp2 wp)
let tot_PURE t = fun p -> forall (x:t). p x
let tot_ALL t = lift_PURE_ALL (tot_PURE t) = fun p h -> forall (x:t). p x h
let tot t = tot_PURE t
let ret_PURE e = return_PURE e
let ret_ALL e = lift_PURE_ALL (ret_PURE e)
--------------------------------------------------------------------------------
Constant's kinds/types:
forall G,
(1) forall type constants T. G |- K_T ok
(2) forall expression constants c. G |- T_c : Type
Proof. Immediate by inspection.
--------------------------------------------------------------------------------
========================
Lemma: Derived judgments:
========================
(1) G |- e : M t wp ==> G |- t : Type /\ G |- wp : K_M(t) /\ G |= monotonic_M t wp /\ G |- ok
(2) G |- M' t' wp' <: M t wp
==> G |- t : Type /\ G |- wp : K_M(t)
/\ G |- t' : Type /\ G |- wp' : K_M(t') /\ G |- ok
(3) G |- t' <: t
==> G |- t : Type /\ G |- t' : Type /\ G |- ok
(4) G |- t : k ==> G |- k ok /\ G |- ok
(5) G |- k <: k' ==> G |- k ok /\ G |- k' ok /\ G |- ok
(6) G |- k : ok ==> G |- ok
(7) G |= t ==> G |- t : Type /\ G |- ok
Proof. By mutual induction on judgments.
For (1) we use the constant's types lemma for rule (T-Const). For rule
(T-Sub) we use part (2) of the IH. Rules (T-Var), (T-Abs), (T-Fix),
(T-FixOmega), and (T-App) have explicit preconditions for making this
true. For monotonicity, we rely on the monotonicity of every WP in G
via K-Arr, in S-Comp, and by showing that every WP-combinator
preserves monotonicity.
For (2) rule (S-Comp) has an explicit precondition to make the 2nd
conjunct true.
For (4) we use the constant's kinds lemma for (K-Const). Rules
(K-Var), (K-TLam), (K-ELam), (K-TApp) and (K-EApp) have explicit
side-conditions for making this true.
--------------------------------------------------------------------------------
====================================
Lemma: Commutation-of-lift-down-==>
====================================
M <= M'
/\ G |= down_M (wp ==>_M (lift_M'_M wp')
/\ G |= down_M' (wp' ==>_M' wp'')
==> G |= down_M (wp ==>_M (lift_M'_M wp'')
Proof: Straightforward from morphisms and modus ponens.
--------------------------------------------------------------------------------
================================
Lemma: Totality-and-monotonicity
================================
G |- e : PURE t wp (H0)
/\ G |= wp post (H1)
==> G |- e : Tot t
Proof:
We use H0 with T-Sub.
The main sub-goal is to show:
G |= forall q. (forall x. q x) ==> wp q
Introducing, with V-ForallTypIntro, and V-ForallIntro, we have:
G |= (forall x. q x) (I1)
and the goal is G |= wp q
From Lemma Derived-judgments (1), we have that wp is monotonic.
So, we use H1 and monotonicity, where the main sub-goal is to show:
G |- forall x. post x ==> q x,
Which is easy trivial, using I1.
--------------------------------------------------------------------------------
===============
Lemma Weakening:
===============
G, G' |- J /\ G, b, G' |- ok ==> G, b, G' |- J
where b stands for x:t or a:k
--------------------------------------------------------------------------------
=============================
Lemma Reduction substitutive:
=============================
We need to require that v is a value below.
This lemma does not hold for non-values.
(1) e1 ~> e2 ==> e1[e/x] ~> e2[e/x]
(2) t1 ~> t2 ==> t1[e/x] ~> t2[e/x]
Proof: By mutual induction on the reduction relations
for pure expressions and types.
(PS-Beta) (fun (y:t) -> e'') e' ~> e''[e'/y]
By PS-Beta: (fun (y:t[e/x]) -> e''[e/x]) e'[e/x] ~> (e''[e/x])((e'[e/x])/y)
We swapping the two substitutions, using the fact that y is
chosen fresh (in particular y not in fe'(e)):
(fun (y:t[e/x]) -> e''[e/x]) e'[e/x] ~> (e''[e'/y])[e/x]
(PS-LetRec) similar to (PS-Beta)
(PS-If0) and (PS-IfS) trivial
All the context rules follow directly from IH.
The cases for t1~>t2 are analogous.
--------------------------------------------------------------------------------
===========================
Lemma: Inversion-for-values
===========================
G |- e : M t wp0 (H1)
/\ (e is a value \/ e is a variable)
==> G |- e : PURE t (ret_PURE e) (C1)
/\ G |= down_M (wp0 ==> lift_PURE_M (ret_PURE e)) (C2)
Proof: Induction on H1.
The cases applicable are: T-Var, T-Const, T-Abs, T-Ret, T-Sub
Cases (T-Var, T-Const, T-Abs):
We have:
G |- e : Tot t
For C1, we use T-Ret.
For C2, we need to show G |= forall post. (forall x. post x) ==> post e
which is a tautology.
Case (T-Ret):
We have
G |- e : Pure t (ret_PURE e)
Which suffices for C1 and C2 is a tautology.
Case (T-Sub):
We have
G |- e : M t wp
Inverting, we have
G |- e : M' t' wp' (I1)
G |- M' t' wp' <: M t wp (I2)
G |- t' <: t (I2')
From the IH we have:
(IH1) G |- e : Pure t' (ret_PURE e)
(IH2) G |- down_M' (wp' ==> lift_PURE_M' (ret_PURE e))
For (C1), we use IH1 with I2' and T-Sub.
For (C2), we use IH2 with I21 and the
commutation-of-lift-with-down-==> Lemma.
--------------------------------------------------------------------------------
=========================
Lemma: Variable inversion
=========================
G |- x : M t wp
==> G |= down_M (wp ==>_M return_M x)
Proof: A special case of inversion for values.
--------------------------------------------------------------------------------
===================
Lemma: Substitution
===================
forall G, tx, e'.
G |- e' : Tot tx
==>
(1) forall x, G', e, t, wp.
G, x:tx, G' |- e : M t wp
==> G, G'[e'/x] |- e[e'/x] : (M t wp)[e'/x]
/\ (2) forall x, G', k.
G, x:tx, G' |- k ok
==> G, G'[e'/x] |- k[e'/x] ok
/\ (3) forall x, G', t, wp, t', wp', phi.
G, x:tx, G' |- M t wp <: M' t' wp'
==> G, G'[e'/x] |- M t[e'/x] wp[e'/x] <: M' t'[e'/x] wp'[e'/x]
/\ (4) forall x, G', t, k.
G, x:tx, G' |- t : k
==> G, G'[e'/x] |- t[e'/x] : k[e'/x]
/\ (5) forall x, G', t, k1, k2.
G, x:tx, G' |- k1 <: k2
==> G, G'[e'/x] |- k1[e'/x] <: k[e'/x]
/\ (6) forall x, G', t, t', phi.
G, x:tx, G' |- t <: t'
==> G, G'[e'/x] |- t[e'/x] <: t'[e'/x]
/\ (7) forall x, G', phi.
G, x:tx, G' |= phi
==> G, G'[e'/x] |= phi[e'/x]
/\ (8) forall x, G',
G, x:tx, G' |- ok
==> G, G'[e'/x] |- ok
Proof: By mutual induction on the 8 judgments (G, x:tx, G'|- J).
Cases of (1)
(T-Var): y=x
Have:
tx = t
so also G |- e' : Tot t (H)
G |- t : Type
since x not dom(G) also x not in fv(t), so t[e'/x]=t
By variable inversion lemma on the original judgment:
G, x:tx, G' |= down_M (wp ==>_M return_M x) (H')
Show:
G, G'[e'/x] |- e' : M t wp[e'/x]
By repeatedly applying weakening to H we obtain:
G, G'[e'/x] |- e' : Tot t
By (T-Return) we obtain:
G, G'[e'/x] |- e' : PURE t (return_PURE e')
By (T-Sub) we still have to show:
G, G'[e'/x] |- PURE t (return_PURE e') <: M t wp[e'/x]
By (S-Comp) still to show:
G, G'[e'/x] |- t <: t' -- immediate from Sub-Conv
G, G'[e'/x] |= down_M (wp[e'/x] ==>_M (lift_PURE_M (return_PURE e')))
By a lift+return rule, still to show:
G, G'[e'/x] |= down_M (wp[e'/x] ==>_M (return_M e'))
By applying the IH (part 7) in H' we obtain what we need.
(T-Var): y<>x
Sub-case: y in dom(G)
Have: G = G1, y:t, G2
G1, y:t, G2, x:tx, G' |- y : Tot t
G1, y:t, G2, x:tx, G' |- ok (H1)
G1 |- t : Type (H2)
By derived judgment
y not in dom(G2) U {x} U dom(G')
x not in fv(t)
so also x not in fv(t)
which means that t[e'/x] = t
By IH (part 8) to H1 we get:
G1, y:t, G2, G'[e'/x] |- ok
From this and (H2), by T-Var we conclude that
G1, y:t, G2, G'[e'/x] |- y : Tot t
Sub-case: y in dom (G')
Have: G' = G1', y:t, G2'
G1, x:tx, G1', y:t, G2' |- y : Tot t
G1, x:tx, G1', y:t, G2' |- ok (H1)
G1, x:tx, G1' |- t : Type (H2)
By applying IH (part 8) to H1 we obtain:
G1, G1'[e'/x], y:t[e'/x], G2'[e'/x] |- ok (H1')
By applying IH (part 4) to H2 we obtain:
G1, G1'[e'/x] |- t[e'/x] : Type (H2')
From (H1') and (H2') by T-Var we conclude that:
G1, G1'[e'/x], y:t[e'/x], G2'[e'/x] |- y : Tot t[e'/x]
(T-Const): trivial, constants are not affected by substitution and have
fixed closed types.
(T-Abs):
Have:
e = fun (x:t1) -> e1 t = (x:t1 -> M t2 wp) M = Tot
(H1) G, x:tx, G' |- t1 : Type (H2) G, x:tx, G', y:t1 |- e1 : M t2 wp
By applying the induction hypothesis to (H1) and (H2) we obtain:
(H1') G, G'[e'/x] |- t1[e'/x] : Type
(H2') G, G'[e'/x], y:t1[e'/x] |- e1[e'/x] : M t2[e'/x] wp[e'/x]
By (T-Abs)
G, G'[e'/x] |- fun (y:t1) -> e1[e'/x]
: Tot (y:t1[e'/x] -> M t2[e'/x] wp[e'/x])
(T-Fix):
Have:
e = let rec (f^d:t) z = e t = y:tx -> PURE t'' wp M = Tot
(H1) G, x:tx, G' |- t : Type (H2) G, x:tx, G' |- d : Tot (z:tx -> Tot t')
(H3) G, x:tx, G', z:tx, f: (y:tx -> PURE t'' (up_PURE (d y << d z) /\_PURE wp))
|- e : (PURE t'' wp[z/y])
By IH:
(H1') G, G'[e'/x] |- t[e'/x] : Type
(H2') G, G'[e'/x] |- d[e'/x] : Tot (z:tx[e'/x] -> Tot t'[e'/x])
(H3') G, G'[e'/x], z:tx[e'/x],
f: (y:tx[e'/x] -> PURE t''[e'/x]
(up_PURE (d[e'/x] y << d[e'/x] z) /\_PURE wp[e'/x]))
|- e[e'/x] : (PURE t''[e'/x] wp[z/y][e'/x])
Since we assumed x, y, and z distinct
and z \not\in fv(e') from G |- e' : Tot tx and z \not in dom(G)
we have wp[z/y][e'/x] = wp[e'/x][z/y]
By (T-Fix) we conclude that
G, G'[e'/x] |- let rec (f^d[e'/x]:t[e'/x]) z = e[e'/x] : Tot t[e'/x]
(T-FixOmega) similar to the case above, just simpler
(T-Ret) trivial
(T-If) trivial
(T-App)
Have:
e = e1 e2 t = (t'[e_2/y])
wp = (bind_M wp1 (fun f -> bind_M wp2 (fun y -> wp')))
(H1) G, x:tx, G' |- e1 : M (y:t'' -> M t' wp) wp1
(H2) G, x:tx, G' |- e2 : M t'' wp2
(H3) G, x:tx, G' |- t'[e2/y] : Type
By IH:
(H1') G, G'[e'/x] |- e1 : M (y:t''[e'/x] -> M t'[e'/x] wp'[e'/x]) wp1[e'/x]
(H2') G, G'[e'/x] |- e2 : M t''[e'/x] wp2[e'/x]
(H3') G, G'[e'/x] |- t'[e2/y][e'/x] : Type
Since y not in dom G and G |- e' : Tot tx we have y not in fv e'
x not in dom G, G' and G, x:tx, G' |- e2 : M t'' wp2 we have x not fv e2
So we can freely swap the two substitutions: t'[e2/y][e'/x] = t'[e'/x][e2/y]
By (T-App)
G, G'[e'/x] |- e1[e'/x] e2[e'/x] : M (t'[e'/x][e_2/x])
(bind_M wp1[e'/x] (fun f -> bind_M wp2[e'/x] (fun x -> wp'[e'/x])))
(T-Sub)
Have: (H1) G, x:tx, G' |- e : M' t' wp'
(H2) G, x:tx, G' |- M' t' wp' <: M t wp
By IH: (H1') G, G'[e'/x] |- e[e'/x] : M' t'[e'/x] wp'[e'/x]
By IH (part 3):
(H2') G, G'[e'/x] |- M' t'[e'/x] wp'[e'/x] <: M t[e'/x] wp[e'/x]
By (T-Sub)
G, G'[e'/x] |- e[e'/x] : M t[e'/x] wp[e'/x]
The cases for parts (2) and (3) are all immediate.
The cases for part (4) kinding are immediate, we only list one explicitly:
(K-EApp)
Have t = t1 e1 k = k1[e1/x1]
(H1) G, x:tx, G' |- t1 : (x1:t1 -> k1)
(H2) G, x:tx, G' |- e1 : Tot t1
By IH:
(H1') G, G'[e'/x] |- t1[e'/x] : (x1:t1[e'/x] -> k1[e'/x])
(H2') G, G'[e'/x] |- e1[e'/x] : Tot t1[e'/x]
By (K-EApp)
G, G'[e'/x] |- t1[e'/x] e1[e'/x] : Tot k1[e'/x][e1/x1]
Since x not in free(e') and x1 not in free(e')
k1[e'/x][e1/x1] = k1[e1/x1][e'/x]
and with this we can conclude
The cases for kind well-formedness and subkinding (parts 5 and 6) are trivial.
Proof of part 7 validity:
The most interesting cases are (E'-RedE), (E'-RedT).
We also check (E'-Assume) since it used to be interesting.
(E'-RedE):
Have: e=(e1=e2) where e1 ~> e2
By reduction substitutive lemma above (part 1) e1[e'/x] ~> e2[e'/x]
Which allows us to show by (E'-RedE) that G,G'[e'/x] |= e1[e'/x] = e2[e'/x]
(E'-RedT): By part (2) of reduction substitutive lemma.
(E'-Assume): this is now trivial
G, x:tx, G' |- e : Tot t
------------------------
G, x:tx, G' |= t
By IH: G, G'[e'/x] |- e[e'/x] : t[e'/x]
By (E'-Assume'): G, G'[e'/x] |= t[e'/x]
--------------------------------------------------------------------------------
==================================================
Lemma: Reduction substitutive (type substitution):
==================================================
(1) e1 ~> e2 ==> e1[t/a] ~> e2[t/a]
(2) t1 ~> t2 ==> t1[t/a] ~> t2[t/a]
--------------------------------------------------------------------------------
========================
Type substitution lemma:
========================
forall G, s, ks.
G |- s : ks
==>
(1) forall a, G', e, t, wp.
G, s:ks, G' |- e : M t wp
==> G, G'[s/a] |- e[s/a] : (M t wp)[s/a]
/\ (2) forall a, G', k.
G, s:ks, G' |- k ok
==> G, G'[s/a] |- k[s/a] ok
/\ (3) forall a, G', t, wp, t', wp'.
G, s:ks, G' |- M t wp <: M' t' wp'
==> G, G'[s/a] |- M t[s/a] wp[s/a] <: M' t'[s/a] wp'[s/a]
/\ (4) forall a, G', t, k.
G, s:ks, G' |- t : k
==> G, G'[s/a] |- t[s/a] : k[s/a]
/\ (5) forall a, G', t, k1, k2.
G, s:ks, G' |- k1 <: k2
==> G, G'[s/a] |- k1[s/a] <: k[s/a]
/\ (6) forall a, G', t, t'.
G, s:ks, G' |- t <: t'
==> G, G'[s/a] |- t[s/a] <: t'[s/a]
/\ (7) forall a, G', phi.
G, s:ks, G' |= phi
==> G, G'[s/a] |= phi[s/a]
/\ (8) forall a, G'.
G, s:ks, G' |- ok
==> G, G'[s/a] |- ok
Proof. Analogous to term substitution.
--------------------------------------------------------------------------------
======================
Lemma Bound reduction:
======================
forall G t1 t2 G' J.
G, x:t1, G' |- J
/\ t1 ~> t2
/\ G |- t2 : Type
==> G, x:t2, G' |- J
Proof: By mutual induction on derivations. The only rules that use
expression variable bindings are (T-Var), (V-Assume), and
(G-Type):
(T-Var):
Subcase x = y:
Have:
G, x:t1, G' |- ok
G |- t1 : Type
By IH (J = ok part) we have that
G, x:t2, G' |- ok
Also we have this explicit premise:
G |- t2 : Type
From the previous two we obtain that:
G, x:t2, G' |- x : Tot t2
By (T-Sub), (S-Comp), (Sub-Conv), (V-RedT) and (V-EqSym) we conclude that:
G, x:t2, G' |- x : Tot t1
Subcase x <> y: trivial
(V-Assume)
Have:
G, x:t1, G' |- ok
G |- t1 : Type
By IH (J = ok part) we have that
G, x:t2, G' |- ok
Also we have this explicit premise:
G |- t2 : Type
Form the previous two we obtain that:
G, x:t2, G' |= t2
By (V-RedT) and (V-EqSym) we conclude that:
G, x:t2, G' |= t1
(G-Type)
Have: G' = . (empty environment)
G |- t1 : Type x not in dom G
We as an explicit premise that :
G |- t2 : Type
This allows us to conclude that:
G, x:t2 |- ok
The other cases are just applications of the induction hypotheses.
--------------------------------------------------------------------------------
====================================================
Lemma Reflexivity of sub-typing and sub-computation:
====================================================
(1) G |- t : Type ==> G |- t <: t
(2) G |- t : Type /\ G |- wp : K_M(t) /\ G |= monotonic_M t wp
==> G |- M t wp <: M t wp
Proof.
Part (1) is trivial from (Sub-Conv) and (V-EqReflT).
Part (2):
By part (1):
G |- t <: t
From (V-ForallIntro), (V-ImplIntro) and (V-Assume):
G |= down_M (wp ==>_M wp)
By (S-Comp):
G |- M t wp <: M t wp
--------------------------------------------------------------------------------
======================================
Lemma: Transitivity-of-sub-computation
======================================
G |- M t wp <: M' t' wp' (H1)
/\ G |- M' t' wp' <: M'' t'' wp'' (H2)
==> G |- M t wp <: M'' t'' wp''
Proof:
Since (H1) can only be obtained by (S-Comp):
M <= M' (G11)
G |- t <: t' (G12)
G |- wp' : K_M(t') (G13)
G |= monotonic_M t' wp'
G |= down_M (wp' ==>_M (lift_M_M' wp)) (G15)
Since (H2) can only be obtained by (S-Comp):
M' <= M'' (G21)
G |- t' <: t'' (G22)
G |- wp'' : K_M(t'') (G23)
G |= monotonic_M t'' wp'' (G24)
G |= down_M (wp'' ==>_M' (lift_M'_M'' wp')) (G25)
From (G11) and (G21) by transitivity of <= we get:
M <= M'' (G1)
From (G12) and (G22) by (Sub-Trans):
G |- t <: t'' (G2)
From (G15) and (G25) by some logical reasoning:
G |= down_M (wp'' ==>_M'' (lift_M_M'' wp)) (G5)
From (G1), (G2), (G23), (G24), and (G5) by (S-Comp):
G |- M t wp <: M'' t'' wp''
--------------------------------------------------------------------------------
==========================
Lemma: Bound-strengthening:
==========================
G, x:t, G' |- J
/\ G |- t' <: t
==> G, x:t', G' |- J
Proof: by mutual induction on the 8 judgments.
--------------------------------------------------------------------------------
===========================================================
Lemma Supertyping-arrow-leads-to-arrow (up to conversion!):
===========================================================
G |- x:t1 -> M t2 wp : Type (G1)
G |= t =_Type (x:t1 -> M t2 wp) (G2)
G |- t <: t' (G3)
G |/= false (G4)
==> exists t1', t2', M', wp'.
G |= t' =_Type (x:t1' -> M' t2' wp') (C1)
/\ G |- t1' <: t1 (C2)
/\ G, x:t1' |- M t2 wp <: M' t2' wp' (C3)
Proof:
By Induction on the sub-typing judgment (G3):
(Sub-Conv)
Have:
G |= t = t'
By (V-EqSymT) and (V-EqTranT) we get
G |= t' =_Type (x:t1 -> M t2 wp)
By reflexivity of subtyping and sub-computation:
G |- t1 <: t1
G |- M t2 wp <: M t2 wp
(Sub-Fun)
Have:
t = (x:t1'' -> M'' t2'' wp'')
t' = (x:t1' -> M' t2' wp' )
G |- t1' <: t1'' (H1)
G, x:t' |- M'' t2'' wp'' <: M' t2' wp' (H2)
From reflexivity we show:
G |= t' =_Type (x:t1' -> M' t2' wp') (C1)
If M <> M'' then we use (V-DistinctTH) and (G4) to obtain a contradiction
If M = M'' then we use (V-InjTH) in (G2) to obtain that
G |= t1 = t1'' (G21)
G |= t2 = t2'' (G22)
G |= wp = wp'' (G23)
From (G21) and (H1) by (Sub-Conv) and (Sub-Trans) we get
G |- t1' <: t1 (C2)
From (G22), (G23), and (H2), by unfolding and folding S-Comp we get
G, x:t1' |- M t2 wp <: M' t2' wp' (C3)
(Sub-Trans)
G |- t <: t'' (H1)
G |- t'' <: t' (H2)
From (H1) and hypotheses by IH we obtain t1'', t2'', M'', wp''.
G |= t'' =_Type (x:t1'' -> M'' t2'' wp'') (H11)
G |- t1'' <: t1 (H12)
G, x:t1'' |- M t2 wp <: M'' t2'' wp'' (H13)
From (H2) and (H11) by IH we obtain t1', t2', M', wp'.
G |= t' =_Type (x:t1' -> M' t2' wp') (C1)
G |- t1' <: t1'' (H22)
G, x:t1' |- M'' t2'' wp'' <: M' t2' wp' (H23)
From (H22) and (H12) by transitivity of subtyping:
G |- t1' <: t1 (C2)
From (H13) and (H22) by bound strengthening:
G, x:t1' |- M t2 wp <: M'' t2'' wp'' (H13')
From (H13') and (H23) by transitivity of sub-computation:
G, x:t1' |- M t2 wp <: M' t2' wp' (C3)
--------------------------------------------------------------------------------
====================================
Lemma Subtyping-arrow-leads-to-arrow
====================================
G |= t =_Type (x:t1 -> M t2 wp) (G2)
G |- t' <: t (G3)
G |/= false (G4)
==> exists t1', t2', M', wp'.
G |= t' =_Type (x:t1' -> M' t2' wp')
/\ G |- t1 <: t1'
/\ G, x:t1 |- M' t2' wp' <: M t2 wp
Proof: Symmetric to Supertyping-arrow-leads-to-arrow above
--------------------------------------------------------------------------------
====================================
Lemma: Subtyping-inversion-for-arrow
====================================
forall G t1 s1 wp1 t2 s2 wp2.
G |- r1 <: r2
G |= r1 = (x:t1 -> M1 s1 wp1)
G |= r2 = (x:t2 -> M2 s2 wp2)
/\ G |/= false
==> G |- t2 <: t1
/\ G, x:t2 |- M1 s1 wp1 <: M2 s2 wp2
Proof: By induction on the subtyping judgment:
(Sub-Fun)
Have:
G |- t2 <: t1
G, x:t2 |- M1 s1 wp1 <: M2 s2 wp2
(Sub-Conv)
Have:
G |= (x:t1 -> M1 s1 wp1) = (x:t2 -> M2 s2 wp2)
Subcase M1 = M2:
Because <= is reflexive:
M1 <= M2
By (V-InjTH):
G |= t1 = t2
G |= s1 = s2
G |= wp1 = wp2
From (V-ImplIntro), (V-Assume), and (V-SubstT).
G |= down_M1 (wp2 ==>_M1 (lift_M1_M1 wp1))
By (Sub-Conv)
G |= t2 <: t1
G |= s1 <: s2
By weakening:
G, x:t2 |= s1 <: s2
We conclude by (S-Comp):
G, x:t2 |- M1 s1 wp1 <: M2 s2 wp2
Subcase M1 <> M2:
By (V-DistinctTH):
G |= ~((x:t1 -> M1 s1 wp1) = (x:t2 -> M2 s2 wp2))
By (V-ImplElim):
G |= false -- contradiction
(Sub-Trans)
Have:
G |- r1 <: r3 (G1)
G |- r3 <: r2 (G2)
From (G1) by Supertyping-arrow-leads-to-arrow we get t3 M3 s3 wp3:
G |= r3 =_Type (x:t1 -> M t3 wp)
By IH in (G1):
G |- t2 <: t1 (G11)
G, x:t2 |- M1 s1 wp1 <: M2 s2 wp2 (G12)
By IH in (G2):
G |- t3 <: t2 (G21)
G, x:t3 |- M2 s2 wp2 <: M3 s3 wp3 (G22)
From (G21) and (G11) by (Sub-Trans):
G |- t3 <: t1
From (G12) and (G21) by bound strengthening:
G, x:t3 |- M1 s1 wp1 <: M2 s2 wp2 <== psi12 (G12')
From (G12') and (G22) by the transitivity of the sub-computation judgment:
G, x:t3 |- M1 s1 wp1 <: M2 s3 wp3
--------------------------------------------------------------------------------
================================
Lemma: Inversion-for-abstraction:
================================
let expression f = fun x:s1 -> e
G |- f : M s wp (H1)
==> exists t1 M' t2 wp'.
G |= s =_Type (x:t1 -> M' t2 wp') (C1)
/\ G |- s1 : Type (C2)
/\ G |- t1 <: s1 (C3)
/\ G |= down_M (wp ==>_M lift_PURE_M (ret_PURE f)) (C5)
/\ G,x:t1 |- e : M' t2 wp' (C6)
/\ exists M0, t0, wp0,
G, x:s1 |- e : M0 t0 wp0 (C7)
/\ G, x:t1 |- M0 t0 wp0 <: M' t2 wp (C8)
Proof: By induction on the typing derivation (H1):
Case (T-Abs)
Have:
M = PURE,
wp = tot s
s = (x:s1 -> M'' s2 wp''') (I1)
G |- s1 : Type (I2)
G, x:s1 |- e : M'' s2 wp''' (I3)
C1: Reflexivity;
C2: from I1
C3: Reflexivity;
C5: Need to show G |= down_PURE (tot s ==>_PURE (ret_PURE f)),
which is a tautology.
C6: From I3.
C7+C8: we take (M0, t0, wp0) = (M'', s1, wp'')
Case (T-Ret):
Have:
M = PURE
wp = ret_PURE f
G |- f : PURE s (tot s) (I1)
By IH, we get:
exists t1 M' t2 wp'.
G |- s =_Type (x:t1 -> M' t2 wp') (IH1)
/\ G |- s1 : Type (IH2)
/\ G |- t1 <: s1 (IH3)
/\ G |= down_PURE (tot_PURE s ==>_PURE (tot_PURE s)) (IH5)
/\ G,x:t1 |- e : M' t2 wp' (IH6)
/\ G,x:s1 |- e : M0 t0 wp0 (IH7)
/\ G,x:t1 |- M0 t0 wp0 <: M' t2 wp' (IH8)
IH1--IH4 and IH6--IH9 are exact for C1--C4 and C6--C9.
We need to show C5:
G |= down_PURE (ret_PURE f ==>_PURE (ret_PURE f))
Again, a tautology.
Case (T-Sub):
Have:
G |- f : M'' t'' wp'' (I1)
G |- M'' t'' wp'' <: M s wp (I2)
From IH, we get:
G |- t'' =_Type (x:t1 -> M' t2 wp') (IH1)
/\ G |- s1 : Type (IH2)
/\ G |- t1 <: s1 (IH3)
/\ G |= down_M'' (wp'' ==>_M'' lift (ret_PURE f)) (IH5)
/\ G,x:t1 |- e : M' t2 wp' (IH6)
/\ G,x:s1 |- e : M0 t0 wp0 (IH7)
/\ G,x:t1 |- M0 t0 wp0 <: M' t2 wp' (IH8)
By inverting (I2)/(S-Comp):
M'' <= M (I21)
G |- t'' <: s (I22)
G |= down_M (wp ==>_M (lift_M''_M wp'')) (I24)
From (I22) and Lemma (supertyping-arrow-leads-to-arrow), we get
G |= s =_Type (x:t1' -> M'' t2' wp''') (L0)
G |- t1' <: t1 (L1)
For Goal C1, we have L0.
For Goal C2, we have IH2.
For Goal C3, we have L1 and IH3, and we conclude with Sub-Trans.
For Goal C5, we need to show
G |= down_M (wp ==>_M lift (ret_PURE f)) (goal)
From I2 and I3, we have:
G |= down_M (wp ==>_M (lift_M''_M wp'')) (J1)
Using G1 and Lemma commutation-of-lift-with-down_M-==>, we get our goal.
For Goal C6, we need to show:
G, x:t1' |- e : M'' t2' wp'''
We have I22, and using lemma subtyping-inversion-for-arrow, we get
G, x:t1' |- M' t2 wp <: M'' t2' wp'' (I22.1)
G |- t1' <: t1 (I22.2)
We use IH6, Lemma bound strengthening with I22.2, I22.1 and
T-Sub to conclude.
For Goal C7, we use IH7.
For Goal C8, we need to show:
G,x:t1' |- M0 t0 wp0 <: M'' t2' wp''
We use a variant of Lemma Bound-strengtening for subtyping with
IH8, I22.1 and transitivity of sub-computation to get C8.
--------------------------------------------------------------------------------
================================
Lemma: Inversion-for-application
================================
G |- e1 e2 : M t wp0
==> exists t1, t2, wp, wp1, wp2.
(C1) /\ G |- e1 : M (x:t1 -> M t2 wp) wp1
(C2) /\ G |- e2 : M t1 wp2
(C3) /\ G |- t2[e2/x] <: t
(C5) /\ G |- t2[e2/x] : Type
(C6) /\ (G |= down_M (wp0 ==>_M app_M wp1 wp2 (fun x -> wp)) (C6.L) //reason about e1 e2 by its type
\/ (G |= down_M (tot_M t ==>_M app_M wp1 wp2 (fun x -> wp)) (C6.R) //reason by its definition, if e1 e2 is total
/\ G |- e1 e2 : Tot t
/\ G |= down_M (wp0 ==>_M ret_M (e1 e2))))
Proof: by induction on the typing derivation; there are 3 rules that
can apply to an application: (T-App), (T-Ret) or (T-Sub)
Case (T-App)
Have:
G |- e1 : M (x:t -> M t' wp) wp1 (C1)
G |- e2 : M t wp2 (C2)
G |- t'[e2/x] : Type (C5)
wp0 = app_M wp1 wp2 (fun x -> wp)
By reflexivity of subtyping we show:
G |- t'[e2/x] <: t'[e2/x] (C3)
By (V-AndIntro)
G |= true (C4)
For C6, we prove (C6.L):
By (V-ForallIntro), (V-ImplIntro), (V-Assume):
G |= down_M (wp0 ==> wp0)
Case (T-Ret)
Have:
M = PURE
wp0 = (return_PURE (e1 e2))
(H1) G |- e1 e2 : Tot t where Tot t = PURE t (tot t)
By IH:
G |- e1 : M (x:t1 -> M t2 wp) wp1 (IH1)
G |- e2 : M t1 wp2 (IH2)
G |- t2[e2/x] <: t (IH3)
G |- t2[e2/x] : Type (IH5)
(IH6)
(G |= down_PURE (tot t ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (IH6.L)
\/ (G |= down_PURE (tot t ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (IH6.R)
/\ G |- e1 e2 : Tot t
/\ G |= down_M (tot t ==>_PURE ret_PURE (e1 e2))))
Simplifying (IH6):
G |= down_PURE (tot t ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (IH6.S)
Still to show:
(G |= down_PURE (ret_PURE (e1 e2) ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (C6.L)
\/ (G |= down_PURE (tot t ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (C6.R)
/\ G |- e1 e2 : Tot t
/\ G |= down_M (ret_PURE (e1 e2) ==>_PURE ret_PURE (e1 e2))))
We prove (C6.R):
The first conjunct is (IH6.S)
The second conjunct (H1)
The third conjunct is a tautology.
Case (T-Sub):
Have:
G |- e1 e2 : M' t' wp0' (H1)
G |- M' t' wp0' <: M t wp0 (H2)
By applying IH in (H1) we get that
G |- e1 : M' (x:t1 -> M' t2 wp') wp1' (IH1)
G |- e2 : M' t1 wp2' (IH2)
G |- t2[e2/x] <: t' (IH3)
G |- t2[e2/x] : Type (IH5)
(IH6)
(G |= down_M' (wp0' ==>_M' app_M' wp1' wp2' (fun x -> wp')) (IH6.L)
\/ (G |= down_M' (tot_M' t' ==>_M' app_M' wp1' wp2' (fun x -> wp')) (IH6.R) (IH6.R.1)
/\ G |- e1 e2 : Tot t' (IH6.R.2)
/\ G |= down_M' (wp0' ==>_M' ret_M' (e1 e2)))) (IH6.R.3)
For the goal, we instantiate:
wp1=lift_M'_M wp1',
wp2=lift_M'_M wp2'
wp=lift_M'_M wp'
By inversion in (H2) using (S-Comp) we get:
G |- t' <: t
M' <= M
G |= down_M (wp0 ==>_M (lift_M'_M wp0'))
To prove G1 and G2:
if M'=M, then lift_M'_M = id, and we simply use IH1 and IH2
Otherwise, we have M < M': so, we apply T-Sub with IH1 and IH2,
and the generated logical guards are tautologies.
From (IH3) by the transitivity of subtyping we obtain that:
G |- t2[e2/x] <: t (G3)
By inversion in (H2)
G |= down_M (wp0 ==>_M (lift_M'_M wp0')) (WP0)
Before we can put together (IH1), (IH2), (G3), and (IH5) and
conclude we still need to show (C6):
(G |= down_M (wp0 ==>_M app_M wp1 wp2 (fun x -> wp)) (C6.L)
\/ (G |= down_M (tot_M t ==>_M app_M wp1 wp2 (fun x -> wp)) (C6.R) (C6.R.1)
/\ G |- e1 e2 : Tot t (C6.R.2)
/\ G |= down_M (wp0 ==>_M ret_M (e1 e2)))) (C6.R.3)
We do this by an additional case analysis, writing lift for lift_M'_M:
Splitting (IH6):
Sub-case (IH6.L): We aim for (C6.L)
G |= down_M' (wp0' ==>_M' app_M' wp1' wp2' (fun x -> wp')) (IH6.L)
Our goal is:
G |= down_M (wp0 ==>_M app_M (lift wp1') (lift wp2') (fun x -> (lift wp'))) (C6.L)
From WP0, we have G |= down_M (wp0 ==>_M (lift wp0'))
Since the lifts are monad morphisms, and app_M is a sequence of binds,
G |= app_M (lift wp1') (lift wp2) (fun x -> (lift wp'))
=
lift (app_M' wp1' wp2' (fun x -> wp'))
Our goal is now:
G |= down_M (wp0 ==>_M lift (app_M' wp1' wp2' (fun x -> wp')))
We use Lemma (commutation of lifts, down, and op_M), with WP0 and IH6.L to conclude.
Sub-case (IH6.R): We aim for (C6.R)
Note that we have t' <: t, from an inversion of H2.
To prove (C6.R.1):
Our goal is:
G |= down_M (tot_M t ==>_M app_M (lift wp1') (lift wp2') (fun x -> (lift wp'))) (C6.R.1)
Rewriting, using the monad morphism law,
G |= down_M (tot_M t ==>_M lift (app_M' wp1' wp2' (fun x -> wp'))) (Goal)
We have from IH6.R.1:
G |= down_M' (tot_M' t' ==>_M' app_M' wp1' wp2' (fun x -> wp')) (IH6.R.1)
Given t' <: t, we have
G |= down_M (tot_M t ==>_M tot_M t')
rewriting
G |= down_M (tot_M t ==>_M (lift (tot_M' t'))) (TotImp)
We use Lemma (commutation of lifts, down, and ==>_M), with TotImp and IH6.R.1 to conclude.
To prove (C6.R.2): To prove (C6.R.2), we use (IH6.R.2) and with inversion of H2.
To prove (C6.R.3):
Our goal is:
G |= down_M (wp0 ==> ret_M (e1 e2)) (Goal)
We have:
G |= down_M' (wp0' ==>_M' ret_M' (e1 e2)) (IH6.R.3)
and G |= down_M (wp0 ==>_M lift wp0') (WP0)
We conclude using the commutations of lifts, down, and ==>_M lemma.
--------------------------------------------------------------------------------
=======================
Lemma: Inversion-for-if
=======================
let e = if e0 then e1 else e2
G |- e : M t wp (H1)
==> exists wp0.
(C1) G |- e0 : M int wp0
(C2) /\ G |- e1 : M t wp1
(C3) /\ G |- e2 : M t wp2
(C4) /\ (G |= downM (wp ==>M ite_M wp0 wp1 wp2) (C4.L)
\/ (G |- e : Tot t (C4.R.1)
/\ G |= downM (tot_M t ==>M ite_M wp0 wp1 wp2) (C4.R.2)
/\ G |= downM (wp ==>M ret_M e))) (C4.R.3)
Proof: By induction on H1.
The applicable cases are (T-If), (T-Ret), and (T-Sub).
The proof is analogous to Lemma Inversion-for-application.
--------------------------------------------------------------------------------
=======================================
Lemma: Inversion-for-constants
=======================================
G |- c : M t wp
==> c = l ==> G = G', l:t_l, G''
/\ for t' = t_l if c = l, t_c otherwise
G |- t' <: t
/\ G |- c : Tot t'
/\ G |= down_M (wp ==>_M ret_M c)
Proof: Easy induction on the typing judgment.
--------------------------------------------------------------------------------
==================================================
Lemma: Preservation-of-typing-on-pure-reduction
and Preservation-of-kinding-on-type-reduction
==================================================
(1) forall G, e, t, wp, post.
G |- e : PURE t wp (H0)
/\ e ~> e' (H1)
[ /\ G |= wp post (H2)
==> G |- e' : PURE t wp (C1)
(2) forall G t t' k, (H3)
G |- t : k (H4)
/\ t ~> t' (H5)
==> G |- t' : k (C3)
Proof: By mutual induction on pure and type reduction relations
Part 1:
Case (PS-LamT):
e = fun (x:s1) -> e1
e' = fun (x:s1') -> e1
G |- e : PURE t wp (H0)
G |- e ~> e' (H1)
Inverting, PS-LamT, we also have:
s1 ~> s2 (I1)
For goal (C1), we aim to show:
G |- e' : PURE t wp
Applying Lemma inversion-for-abstraction to H0, we get:
G |= t =_Type x:t1 -> M' t2 wp' (G31)
G, x:t1 |- e1 : M' t2 wp'' (G32)
G |- t1 <: s1 (G33)
G |= down_PURE (wp ==>_PURE ret_PURE e1) (G35)
...
G, x:s1 |- e1 : M0 t0 wp0 (G37)
G, x:t1 |- M0 t0 wp0 <: M' t2' wp' (G38)
To get (C1), we use T-Abs, we have two sub-goals:
Subgoal 1: G |- s1' : Type
We get this from the mutual induction hypothesis.
Subgoal 2:
G, x:s1' |- e1 : M0 t0 wp0
We use (G37) and Lemma Bound-strengthening, noting that G |- s1 =Type s1'.
So, we have G |- e' : Tot (x:s1 -> M0 t0 wp0) (J1)
Using (J1), with (G38), (G33) and T-Sub, we get:
G |- e1' : Tot t (J2)
Using (T-Ret), we get
G |- e1' : Pure t (ret_PURE e1') (J3)
To conclude, we need to show
G |= down_PURE (wp ==>_PURE ret_PURE e1')
But, we have G |= e1 = e1' , since they are related by reduction.
So, we use G35 and V-SubstE to conclude.
Case (PS-RecT): Similar to PS-LamT.
Case (PS-AppE1):
e = e1 e2
e' = e1' e2
We have:
G |- e1 e2 : PURE t wp0 (H0)
G |- e1 ~> e1' (H1)
Applying Lemma inversion-for-application:
(I1) G |- e1 : PURE (x:t1 -> PURE t2 wp) wp1
(I2) /\ G |- e2 : PURE t1 wp2
(I3) /\ G |- t2[e2/x] <: t
(I5) /\ G |- t2[e2/x] : Type
(I6) /\ (G |= down_PURE (wp0 ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (I6.L)
\/ (G |= down_PURE (tot t ==>_M app_M wp1 wp2 (fun x -> wp)) (I6.R)
/\ G |- e1 e2 : Tot t
/\ G |= down_PURE (wp0 ==>_M ret_M (e1 e2))))
From the induction hypothesis, we get:
(IH1) G |- e1' : PURE (x:t1 -> PURE t2 wp) wp1
Next, we build:
(C1') G |- e1' e2 : PURE t wp0'
Using IH1 and I2, with T-App and get
wp0' = app_PURE wp1 wp2 (fun x -> wp)
We need to show G |- e1' e2 : PURE t wp0
meaning we need G |= down_PURE (wp0 ==>PURE wp0') (GOAL)
So, split on the cases of (I6):
sub-case (I6.L): We have what we need, immediately.
sub-case (I6.R):
We use I6.R.1, C1' and T-Sub to build:
G |- e1' e2 : Tot t (J1)
Then, we use J1 and T-Ret to build:
G |- e1' e2 : PURE t (ret (e1' e2)) (J3)
Then, using I6.R.3 and V-SubstE, we build (GOAL).
Case (PS-AppE2, PS-LetRecD, PS-If0E0):
all context rules, which are similar to PS-AppE1.
Case (PS-Beta):
e = f v
f = fun (x:s1) -> e1
e' = e1[v/x]
G |- e : PURE t wp0 (H0)
G |- e ~> e' (H1)
Applying Lemma inversion-for-application:
(I1) G |- f : PURE (x:t1 -> PURE t2 wp) wp1
(I2) /\ G |- v : PURE t1 wp2
(I3) /\ G |- t2[v/x] <: t
(I5) /\ G |- t2[v/x] : Type
(I6) /\ (G |= down_PURE (wp0 ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (I6.L)
\/ (G |= down_PURE (tot t ==>_PURE app_PURE wp1 wp2 (fun x -> wp)) (I6.R)
/\ G |- f v : Tot t
/\ G |= down_M (wp0 ==>_PURE ret_PURE (f v))))
Applying Lemma inversion-for-abstraction to (I1), we get:
G |- s1 : Type (J1)
/\ G |- t1 <: s1 (J2)
/\ G |= down_PURE (wp1 ==>_M ret_PURE f) (J4)
/\ G,x:t1 |- e1 : PURE t2 wp (J5)
/\ G, x:s1 |- e1 : M0 t0 wp0 (J6)
/\ G, x:t1 |- M0 t0 wp0 <: PURE t2 wp (J7)
---- First, we build;
G |- v : PURE t1 (ret v) (S1)
and G |= down (wp2 ==> (ret v)) (V-Ret)
by using the Lemma inversion-for-values with (I2).
----- Next, we build :
G |- v : Tot t1 (V-Tot)
We use T-Sub with S1 to build (V-Tot), so long as we can show
G |= downPURE (tot t ==> ret v)
which is a tautology.
----- Next, we build : G |- e1[v/x] : (PURE t2 wp)[v/x] (Reduct-typed)
We use (V-Tot) and (J5) with the substitution lemma.
----- To conclude, we need to show that G |- e1[v/x] : PURE t wp0
We first use T-Sub with (Reduct-typed), using t2[v/x] <: t from I3. to build
G |- e1[v/x] : PURE t (wp[v/x]) (R)
We split the cases of (I6):
Sub-case (I6.L):
We use (R) with T-Sub and have to show
We show G |= down (wp0 ==> wp[v/x])
From Lemma inversion-of-values, from V-Ret, an from I6.L, we have
G |= down (wp0 ==> app (ret f) (ret v) (fun x -> wp))
unfolding ..
G |= wp0 ==> wp[v/x] which is our goal.
Sub-case (I6.R)
From Lemma inversion-of-values, from V-Ret, an from I6.R.1, we have
G |= down (tot t ==> app (ret f) (ret v) (fun x -> wp))
unfolding ...
G |= down (tot t ==> wp[v/x]) (KK1)
We also have from I6.R.3:
G |= down (wp0 ==>_PURE ret_PURE (f v)) (KK2)
So, we use (R), (KK1) and T-Sub to build:
G |- e1[v/x] : Tot t
Using T-Ret, we build
G |- e1[v/x] : PURE t (ret_PURE (e1[v/x]))
Using T-Sub, we rely on f v ~> e1[v/x]
to derive G |= e1[v/x] = f v, and build
G |- e1[v/x] : PURE t (ret_PURE (f v))
We use KK2 with T-Sub to build
G |- e1[v/x] : PURE t wp0 ... which is our goal.
Case (PS-LetRec):
We have vf = let rec (f^d:t) x = e
and (vf v ~> e[v/x][vf/f])
This case is analogous to two applications of PS-Beta.
The main novelty is in the use of the substitution lemma to show that
if e0 then e1 else e2
given t = y:tx -> PURE t'' wp
and G |- vf : Tot t
we can also derive
G |- vf : y:tx -> PURE t'' (up_PURE (d y << d v /\_PURE wp))
This amounts to showing:
G |= down_PURE (up_PURE (d y << d v /\_PURE wp) ==>PURE wp)
Unfolding definitions, it is easy to see that this is a tautology.
Case (PS-If0):
e=if0 0 then e1 else e2
e ~> e1
We have G |- e : Pure t wp
From Lemma inversion-for-if, we have:
(C1) G |- 0 : PURE int wp0
(C2) /\ G |- e1 : PURE t wp1
(C3) /\ G |- e2 : PURE t wp2
(C4) /\ (G |= downPURE (wp ==>M ite_PURE wp0 wp1 wp2) (C4.L)
\/ (G |- e : Tot t (C4.R.1)
/\ G |= downPURE (tot t ==>PURE ite_PURE wp0 wp1 wp2) (C4.R.2)
/\ G |= downPURE (wp ==>PURE ret e))) (C4.R.3)
Splitting on cases of (C4):
Leaving M implicit everywhere, since it is always PURE.
Sub-case (C4.L):
G |= down (wp ==> ite wp0 wp1 wp2) (C4.L)
We use (C2) and get G |- e1 : PURE t wp1
We need to show G |= down (wp ==> wp1) (GOAL)
unfolding C4.L, we have
G |= down (wp ==> bind wp0 (fun x -> up (x=0) ==> wp1
/\ up (x<>0) ==> wp2))
From value inversion on C1, we have
G |= down (wp0 ==> ret_ 0)
Using it with (C4.l), we get:
G |= down (wp ==> (up (0=0) ==> wp1
/\ up (0<>0) ==> wp2))
Which simplifies easily to (GOAL).
Sub-case (C4.R):
Our main-sub-goal is to show:
G |- e1 : Tot t (E1-Tot)
Given (E1-Tot), we use (T-Ret) to build:
G |- e1 : Pure t (ret e1) (E1-Ret)
Then, we use (T-Sub) to build
G |- e1 : Pure t (ret e) (E1-Ret')
since e ~> e1, we have that the two are definitionally equal.
And finally, we use T-Sub with C4.R.3 to build
G |- e1 : Pure t wp, as required.
Now, to show (E1-Tot):
We have (C4.R.1)
G |= downPURE (tot t)
==> (ite_PURE wp0 wp1 wp2)
From value inversion, we know that downPURE (wp0 ==>PURE ret 0)
G |= down (tot t
==> ((up_PURE (0=0) ==>PURE wp1
/\ up_PURE (0<>0) ==>PURE wp2)))
Simplifying, we get
G |= down (tot t ==>PURE wp1) (Tot-Imp)
For the goal, we use C2 with T-Sub and Tot-Imp to build (E1-Tot), as needed.
Case (PS-IfS): Symmetric to PS-If0.
Part 2:
(K-Var) and (K-Const): contradiction, type variables and constants do not reduce
(K-Arr)
Case analysis on the last type reduction rule, the only rule that
applies is (TS-TCtx)
Subcase E = x:o -> M t2 wp : by bound reduction and induction hypothesis
Subcase E = x:t1 -> M o wp : by induction hypothesis
Subcase E = x:t1 -> M t2 o : by induction hypothesis
(K-TLam) and (K-ELam) by bound reduction and induction hypothesis
(K-TApp)
Have: t = t1 t2 k = k'[t/a]
G |- t1 : a:k'' -> k'
G |- t2 : k''
Show: G |- t' : k'[t/a]
Case analysis on the last type reduction rule:
(TS-TBeta) (fun (a:k) -> t') t ~> t'[t/a]
By an easy inversion, we have that:
1. G, a:k |- t' : k'
2. G |- t : k
We use the type-substitution lemma to conclude.
(TS-TCtx): by induction hypothesis
(K-EApp)
Have: t = t1 e k = k'[e/x]
G |- t1 : x:t2 -> k'
G |- e : Tot t'
Show: G |- t' : k'[e/x]
Case analysis on the last type reduction rule:
(TS-EBeta) (fun (x:t) -> t') v ~> t'[e/x]
By an easy inversion, we have that:
1. G, x:t |- t' : k'
2. G |- e : Tot t
We use the substitution lemma for types to conclude.
(TS-TCtx): by induction hypothesis
(TS-ECtx): e ~> e'
We use the mutual induction hypothesis to get
G |- e' : Tot t'.
--------------------------------------------------------------------------------
=========================================================
Lemma: Pure-CBV-reductions-are-included-in-pure-reduction
=========================================================
(H,e) ~> (H',e') (H1)
/\ G |- e : PURE t wp (H2)
/\ G |/= false (H4)
==> e ~> e' /\ H = H'
Proof. By induction on the derivation of (H1):
Case (IS-Read)
Have: e = (!_t) l
By application inversion in H2:
G |- !_t : PURE (x:t'' -> PURE t' wp') wp1
Let !_t be typed as x:ref t -> M t wp and we require M > PURE.
By Lemma inversion-for-constants, we get
G |- x:ref t -> M t wp
<:
x:t'' -> PURE t' wp'
Using Lemma Subtyping-inversion-for-arrow, and then inverting return
type consequent with S-Comp, we get M <= PURE ... a contradiction.
Case (IS-Write):
Similar to IS-Read.
All other IS-* rules, have corresponding PS-* rules.
For (IS-Beta), (IS-LetRec), (IS-If0), and (IS-IfS) it is immediate
that H = H'.
For the remaining rules (IS-AppE1), (IS-AppE2), (IS-If0E0) we need to
first apply an inversion lemma on the typing judgment and then
induction hypothesis before we can conclude.
--------------------------------------------------------------------------------
Note: considering open reductions for terms is not strictly necessary
for programs, since we only care about reducing closed programs. But
proving S.R. for open terms is not substantially more complicated---so
we keep it for generality.
--------------------------------------------------------------------------------
=================================================
Definition: Isomorphism of memory model and heap
=================================================
Let mem be a memory model. Then m is isomorphic to h under G,
written as G |- m ~ h
iff
G |- m : mem
/\ G |- h : heap
/\ G |= forall l. mcontains m l = contains h l /\ msel m l = sel h l
--------------------------------------------------------------------------------
======================================
Lemma: Upd-commutes-with-isomorphism
======================================
Let mem be a memory model. Then,
G |- l : M (ref t) _
/\ G |- v : M t _
/\ G |- m ~ h (H)
==> G |- mupd m l v ~ upd h l v
Proof:
We get G |- mupd m l v : mem and G |- upd h l v : heap from types of mupd and upd.
let m' = mupd m l v and h' = upd h l v
We need to prove that G |= forall l'. mcontains m' l' = contains h' l' /\
msel m' l' = sel h' l'
We can prove:
G, l':ref t, _:(l' = l) |= mcontains m' l' = contains h' l' /\
msel m' l' = sel h' h'
and that
G, l':ref t, _: ~(l' = l) |= mcontains m' l' = contains h' l' /\
msel m' l' = sel h' h'
(using hypothesis H)
and then use V-ExMiddle to get our proof.
---------------------------------------------------------------------------------
======================================
Lemma: Value-respects-location-typing
======================================
G |- H
/\ G |- l : M (ref t) wp
==> G |- H(l) : M t wp'
---------------------------------------------------------------------------------
====================================
Lemma: Location-typing-is-invariant
====================================
G |- l : M (ref t) wp
==> G = G', l:ref t, G''
---------------------------------------------------------------------------------
===============================================
Lemma: Preservation-of-typing-for-CBV-reduction
===============================================
forall G, H, e, H', e', t, wp, m.
G |- e : M t wp (H1)
(H, e) ~> (H', e') (H2)
G |- H (H6)
==> forall post.
/\ G |- post : Post_ALL(t) (H3)
/\ G |= (lift_M_ALL wp) post m (H4)
/\ G |- m ~ (asHeap H) (H5)
==> exists G' = G, G'' , wp', m'.
G' |- e' : M t wp' (C1)
/\ G' |= (lift_M_ALL wp') post m' (C2)
/\ G' |- m' ~ (asHeap H') (C3)
/\ G' |- H' (C4)
---------------------------------------------------------------------------------
Proof:
The proof is by by induction on (H2).
Case: G |= false
This case is an easy---goal (C2) is clearly trivial.
For goal (C1), we do an easy induction on the top-level rule in
(H2). The main non-trivial goals are to show that every
type-annotation in e' is well-kinded (since the kind of a type does
not depend on the (now trivialized) validity judgment). However,
since (H2) never does any type-reduction, and since every
type-annotation in e is well-kinded, every annotation in e' is also
well-kinded. Goals (C3) and (C4) can be derived similar to
corresponding cases in G |/= false.
Case: G |/= false
We proceed by induction on (H2).
The main interesting cases are:
==============
Case (IS-Beta)
==============
let f = (fun (x:t) -> e)
Hypothesis (H1): G |- f v : M t wp
(H2): (H, f v) ~> (H, e[v/x])
(H4): G |= (lift_M_ALL wp) post m
(H5): G |- m ~ (asHeap H)
We use Lemma inversion-for-application on (H1) to get:
(C1) /\ G |- f : M (x:t1 -> M t2 wp') wp1
(C2) /\ G |- v : M t1 wp2
(C3) /\ G |- t2[v/x] <: t
(C5) /\ G |- t2[v/x] : Type
(C6.L) /\ G |= down_M (wp ==>_M app_M wp1 wp2 (fun x -> wp'))
Note, we consider (C6.R) later.
Using Lemma inversion-for-values on f and v, on C6.L, we get
(I1) G |= down_M (wp ==>_M app_M (lift (ret f)) (lift (ret v)) (fun x -> wp'))
(I2) G |- v : Tot t1
By reduction, we get
(I3) G |= down_M (wp ==>_M wp' [v/x])
Using Lemma inversion-for-abstractions on (C1), we get
(I4) G, x:t1 |- e : M t2 wp'
Using the substitution lemma, we get
(C1') G |- e[v/x] : M (t2[v/x]) (wp'[v/x])
Choose G' = G. Then:
Using (C1'), (C3) and (C4) with (T-Sub), we get goal (C1).
Choose m' = m.
For (C2), we need to show G |- (lift_M_ALL wp'[v/x]) post m
But, this follows from (I3) and (H4), (V-ForallTypElim), (V-ForallElim) and V-ImplElim.
(C3) follows from (H5).
(C4) follows from (H6) (G' = G and H' = H).
--
Now let's consider case (C6.R). We have (C1), (C2), (C3), (C5), and
(C6.R) G |= down_M (tot_M ==>_M app_M wp1 wp2 (fun x -> wp'))
/\ G |- f v : Tot t
/\ G |= down_M (wp ==>_M ret_M (f v))
We have f v ~> e[v/x] using PS-Beta, and G |- f v : Tot t
Hence we can apply Lemma Preservation-of-typing-on-pure-reduction to get:
(K1) G |- e[v/x] : Tot t
Further,
(K2) G |= f v = e[v/x] (using V-RedE)
Using T-Ret with (K1):
(K3) G |- e[v/x] : ret_Pure e[v/x]
Lift to M:
(K4) G |- e[v/x] : ret_M e[v/x]
Choose G' = G and wp' = ret_M e[v/x]. This gives us (C1).
Then, manipulating third premise of (C6.R):
G |= down_M (wp ==>_M ret_M (e[v/x])) (using K2)
G |= down_ALL (lift_M_ALL wp ==>_ALL ret_ALL e[v/x]) (lift to ALL) (K5)
Choose m' = m.
Instantiate (K5) with post and m and use with (H4) to get goal:
G |= (ret_ALL e[v/x]) post m.
(C3) and (C4) are trivial since m' = m, G' = G, and H' = H.
===============
Case (IS-Read):
===============
Hypothesis (H1): G |- (!_t') l : M t wp
(H2): (H, l) ~> (H, H(l))
(H4) : G |= (lift_M_ALL wp) post m
From Lemma Inversion-for-application on (H1):
G |- !_t' : M (x:t1' -> M t wp1) wp2 (C1)
G |- l : M t1' wp3 (C2)
G |= down_M (wp ==>_M app_M wp2 wp3 (fun x -> wp1)) (C3)
Let !_t' be typed as x:ref t' -> M' t' wp1'. Then from monad morphism:
x:ref t' |= down_ALL (lift_M'_ALL wp1' ==>_ALL (fun p h -> p (msel h x) h)) (M1) (In fact, morphism gives us <==>_M, but here we need just this direction)
Then, by Lemma Inversion-for-constants on (C1):
G |- x:ref t' -> M' t' wp1' <: x:t1' -> M t wp1 (C4)
G |= down_M (wp2 ==>_M (ret_M !_t')) (C5)
By Subtyping-inversion-for-arrow on (C4) (we know G |\= false from case split at the beginning of the proof):
G |- t1' <: ref t', use this with (C2) to get: G |- l : M (ref t') wp3
G, x:ref t' |- M' t' wp1' <: M t wp1 (C6)
Inverting S-Comp on (C6):
G, x:ref t' |= down_M (wp1 ==>_M (lift_M'_M wp1')) (C7)
G, x:ref t' |= t' <: t, which implies
G |- t' <: t (S1) (Since x notin FV(t) and x notin FV(t'))
From Lemma Inversion-for-constants on (C2):
G |= down_M (wp3 ==>_M (ret_M l)) (C8)
Using (C5), replace wp2 by (ret_M !_t') in (C3) to get:
G |= down_M (wp ==>_M app_M (ret_M !_t') wp3 (fun x -> wp1))
= G |= down_M (wp ==>_M app_M wp3 (fun x -> wp1)) (C3')
Using (C8), replace wp3 by (ret_M l) in (C3') to get:
G |= down_M (wp ==>_M app_M (ret_M l) (fun x -> wp1))
= G |= down_M (wp ==>_M wp1[l/x]) (C3'')
In (C7) instantiate x with l and lift to ALL to get:
G |= down_ALL ((lift_M_ALL wp1[l/x]) ==>_ALL (lift_M'_M_ALL wp1'[l/x]))
= G |= down_ALL (lift_M_ALL wp1[l/x] ==>_ALL (lift_M'_ALL wp1'[l/x])) (C3''')
From lift of (C3'') to ALL, (C3'''), and instantiation of (M1) with x = l:
G |= down_ALL (lift_M_ALL wp ==>_ALL (fun p h -> p (msel h l) h))
Thus:
(I2) G |= down_ALL (lift_M_ALL wp ==>_ALL (fun p h -> p (msel h l) h))
which can be expanded to
G |= forall p h. (lift_M_ALL wp) p h ==> p (msel h l) h
And we have 4 subgoals:
find G', wp', m' such that:
1. G' |- H(l) : M t wp'
2. G' |= (lift_M_ALL wp') post m'
3. G' |- m' ~ (asHeap H)
4. G' |- H
Pick G' = G.
To show sub-goal 1:
G |- H(l) : Tot t1' (by Lemma Value-respects-location-typing)
G |- H(l) : Tot t (By T-Sub with S1)
G |- H(l) : PURE t (return_PURE t H(l)) (by T-Ret)
G |- H(l) : M t (return_M t H(l)) (by T-Sub)
To show sub-goal 2, choose m' = m.
Need: G |= (lift_M_ALL (return_M t H(l))) post m
= G |= (return_ALL t H(l)) post m
By definition of return_ALL, to show:
G |= post H(l) m
From (I2), (H4), (V-ForallTypElim), (V-ForallElim) and V-ImplElim,
we get:
G |= post (msel m l) m (V)
Since G |- m ~ (asHeap H):
G |= post (sel (asHeap H) l) m (V1)
From PS-Sel and V-SubstE applied to (V1) we get our second goal.
Third goal is immediate from (H5) since m' = m and H' = H.
Fourth goal is immediate from (H6) similarly.
================
Case (IS-Write):
================
Hypothesis (H1): G |- l :=_t' i : M t wp
(H2): (H, l := i) ~> (H', ()) where H'=H[l->i]
(H4) : G |= (lift_M_ALL wp) post m
We now go very similar to case IS-Read above:
From Lemma Inversion-for-application on (H1):
G |- :=_t' : M (x:t1' -> y:t2' -> M t wp1) wp2 (C1)
G |- l : M t1' wp3 (C2)
G |- i : M t2' wp4 (C3)
G |= down_M (wp ==>_M app_M wp2 wp3 wp4 (fun x y -> wp1)) (C4)
Let :=_t' : x:ref t' -> y:t' -> M' unit wp1', by monad morphism:
x:ref t', y:t' |= down_ALL (lift_M'_ALL wp1' <==>_M (fun p h -> p () (mupd h x y))) (M1)
From Lemma Inversion-for-constants on (C1):
G |- x:ref t' -> y:t' -> M' unit wp1' <: x:t1' -> y:t2' -> M t wp1 (C5)
G |- down_M (wp2 ==_M (ret_M :=_t')) (C6)
Subtyping-inversion-for-arrow on (C5):
G |- t1' <: ref t', use this with (C2) to get: G |- l : M (ref t') wp3 (C2')
G, x:ref t' |- t2' <: t', use this with (C3) to get: G |- i : M t' wp4 (C3')
G |- unit <: t (C7')
G, x:ref t', y:t' |= down_M (wp1 ==>_M lift_M'_M wp1') (C7)
Lemma Inversion-for-constants on (C2) and (C3):
G |= down_M (wp3 ==>_M (ret_M l)) (C8)
G |= down_M (wp4 ==>_M (ret_M i)) (C9)
Using (C6), (C8), and (C9), (C4) can be reduced to:
G |= down_M (wp ==>_M wp1[l/x][i/y]) (C10)
Using (C10) with (C7) (after instantiating x and y):
G |= down_M (wp ==>_M lift_M'_M wp1'[l/x][i/y]) (C11)
Lift (C11) to ALL, and combine with (M1) to get (I2) below:
Thus:
(I1) t = unit
(I2) G |= forall p h. (lift_M_ALL wp) p h ==> p () (mupd h l i)
And we have 4 subgoals:
find G', wp', m' such that:
1. G |- () : M t wp'
2. G |= (lift_M_ALL wp') post m'
3. G' |- m' ~ (asHeap H')
4. G' |- H'
Choose G' = G.
To show sub-goal 1:
G |- () : Tot unit (by T-Const)
G |- () : Tot t (By T-Sub and (C7'))
G |- () : PURE t (return unit ()) (by T-Ret)
G |- () : M t (return_M unit ()) (by T-Sub)
To show sub-goal 2, choose m' = mupd m l i
Need: G |= lift_M_ALL (return_M unit ()) post m'
= G |= (return_ALL unit ()) post m'
= G |= post () m'
From (I2), (H4), (V-ForallTypElim), (V-ForallElim) and V-ImplElim,
we get
G |= post () (mupd m l i)
which is our second goal.
For third goal, we need G |- m' ~ (asHeap H')
Using (PS-Upd) and (V-SubstE) we get
G |= asHeap H' = upd (asHeap H) l i
So now we need to show:
G |- mupd m l i ~ upd (asHeap H) l i
We already have G |- m ~ (asHeap H) from (H5). Use Lemma Upd-commutes-with-isomorphism to get (C3).
For (C4), we need to show that G |- H[l -> i]
Follows from (C2'), (C3'), and rule TH-Ind (lemma Location-typing-is-invariant).
===============
Case (IS-AppE2):
===============
We have
(H1) G |- (v e1) : M t wp
(H2) (H, (v e1)) ~> (H', (v e1'))
(H21) (H, e1) ~> (H', e1')
(H4) G |= (lift_M_ALL wp) post m
Using inversion-for-application: (consider C6.R case later)
G |- v : M t wp0 (I0)
G |- e1 : M t1 wp1 (I1)
G |- down_M (wp ==>_M app_M wp0 wp1 (fun x -> wp_f)) (I2)
From Lemma value-inversion on (I0) applied to (I2), we get:
G |- down_M (wp ==>_M app_M (ret_M v) wp1 (fun x -> wp_f)) (I3)
Simplifying
G |- down_M (wp ==>_M bind_M wp1 (fun x -> wp_f)) (H3)
From the IH, we have G' |- e1' : M t1 wp1' and G' |- m'' ~ (asHeap H') and G' |- H' (H4)
Next, we rebuild:
G' |- (v e1') : M t wp'
where wp' = app_M (ret_M v) wp1' (fun x -> wp_f)
which simplifies again to
wp' = bind_M wp1' (fun x -> wp_f)
(We rely on weakening lemma for typing v in G', which by induction
hypothesis (H4) is G, G'')
From the IH we have:
forall q. G' |= (lift_M_ALL wp1) q m ==> (lift_M_ALL wp1') q m'' (G1)
We choose m' = m''. Third goal G' |- m' ~ (asHeap H') is immediate from I.H. (H4) above.
Also, fourth goal carries over from (H4).
Our second goal is:
G |= (lift_M_all wp') post m''
Substituting wp', our goal becomes:
G |= (bind_ALL (lift_M_ALL wp1') (fun x -> lift_M_ALL wp_f)) post m''
Expanding, our goal becomes:
G |= lift_M_ALL wp1' (fun x h2 -> ((lift_M_ALL wp_f) x) post h2) m'' (G2)
Lift (H3) to ALL:
G |= down_ALL (lift_M_ALL wp ==>_ALL bind_ALL (lift_M_ALL wp1) (fun x -> lift_M_ALL wp_f))
Using (H4) (instantiate down_ALL with post and m):
G |= (bind_ALL (lift_M_ALL wp1) (fun x -> lift_M_ALL wp_f)) post m
Expanding:
G |= (lift_M_ALL wp1) (fun x h2 -> (lift_M_ALL wp_f x) post h2) m
Instantiate (G1) with q = (fun x h2 -> (lift_M_ALL wp_f x) post h2) and apply modus ponens to get our goal (G2).
--
Now consider C6.R case. We have:
G |- v : M t wp0 (I0)
G |- e1 : M t1 wp1 (I1)
G |= down_M (wp ==>_M ret_M (v e1)) (I2)
G |= v e1 : Tot t
With I2, use Lemma Preservation-of-typing-on-pure-reduction to get:
G |- v e1' : Tot t
and G |= v e1 = v e1' (similar to the proof of beta case)
Choose wp' = ret_ALL (v e1')
Proof now follows similar to proof of beta case above.
==============
Case IS-Alloc
==============
We have:
G |- alloc_t' v1 v2 : M t wp (H1)
H, alloc_t' v1 v2 ~> H[l -> v2], l (H2)
l notin dom(H) /\ meta l = v1 (H2')
G |= (lift_M_ALL wp) post m (H4)
From Lemma inversion-for-application on (H1)
G |- alloc_t' : M (q:meta_data -> x:t1' -> M t wp1) wp2 (C1)
G |- v1 : M meta_data wp3 (C2)
G |- v2 : M t1' wp4 (C3)
G |= down_M (wp ==>_M app_M wp2 wp3 wp4 (fun x y -> wp1)) (C4)
Let alloc_t' : M' (q:meta_data -> x:t' -> M (ref t') wp1'). Then by morphism:
x:t', q:meta_data |= down_ALL (lift_M'_ALL wp1' ==>_ALL (fun p h ->
forall l. not (mcontains h l) /\ meta l = q
==> p l (mupd h l x)) (M1)
Using Lemma Inversion-for-constants on (C1), (C2), and (C3):
G |- q:meta_data -> x:t' -> M' (ref t') wp1' <: q:meta_data -> x:t1' -> M t wp1 (C5)
G |= down_M (wp2 ==>_M (ret_M alloc)) (C6)
G |= down_M (wp3 ==>_M (ret_M v1)) (C7)
G |= down_M (wp4 ==>_M (ret_M v2)) (C8)
Using (C6), (C7), and (C8), (C4) can be reduced to:
G |= down_M (wp ==>_M wp1[v1/q][v2/x]) (C9)
Using Subtyping-inversion-for-arrow on (C5):
G |- t1' <: t', use this with (C2) to get: G |- v2 : M t' wp4 (C10')
G, q:meta_data, x:t' |- ref t' <: t, implying G |- ref t' <: t (since q and x are not free in either) (C10'')
G, x:t', q:meta_data |= down_M (wp1 ==>_M lift_M_M' wp1') (C10)
Instatiate with x = v2 and q = v1:
G |= down_M (wp1[v1/q][v2/x] ==>_M lift_M_M' wp1'[v1/q][v2/x]) (C11)
Modus-ponens with (C9) and (C11):
G |= down_M (wp ==>_M lift_M_M' wp1'[v1/q][v2/x]) (C12)
Lift (C12) to ALL and use modus ponens with (M1) to get:
G |= forall p m. (lift_M_ALL wp) p m ==>_ALL forall l. not (mcontains m l) /\ meta l = v1
==> p l (mupd m l v2) (C13)
Modus-ponens with (H4):
G |= forall l'. not (mcontains m l') /\ meta l' = v1 ==> post l' (mupd m l' v2) (C14)
We now prove our 4 goals:
Choose G' = G, l : ref t' and wp' = ret_M l
Then we use T-Var, T-Ret, with a lift to M to show our first goal G' |- l : M (ref t') wp'. Use T-Sub with (C10'') to get the goal.
Second, we have to prove:
G' |= lift_M_ALL wp' post m'
Choose m' = mupd m l v2 and expand our second goal to get:
G' |= post l (mupd m l v2)
From (C14) we have (after weakening G to G'):
G' |= forall l'. not (mcontains m l') /\ meta l' = v1 ==> post l' (mupd m l' v2) (C15)
Instantiate with l' = l
G' |= not (mcontains m l) /\ meta l = v1 ==> post l (mupd m l v2) (C16)
We have meta l = v1 from (H2')
To prove not (mcontains m l), we have from (H2'):
l notin dom(H) = true
Using PS-Contains with V-RedE
G |= contains (asHeap H) l = false
But since G |- m ~ (asHeap H), we get G |= mcontains m l = false. Use Modus-ponens with (C16) to get second goal.
For third goal, we need to prove:
G' |- (mupd m l v2) ~ (asHeap (H[l -> v2]))
Using PS-Upd, we need to show:
G' |- (mupd m l v2) ~ upd (asHeap H) l v2 which follows from Lemma Upd-commutes-with-isomorphism.
For fourth goal, we need to show G' |- H'. Follows from TH-Ind and (C10').
=======================
Case IS-AppE1, IS-If0E0
=======================
Both are context rules, and the reasoning is analogous to IS-AppE2
==============
Case IS-LetRec
==============
The reasoning is essentially two applications of IS-Beta, with a
subtyping proof as in the reasoning in the case of PS-LetRec, in case
the fix point is pure but the argument is not.
======================
Case IS-If0 and IS-IfS
======================
Identical to the reasoning in PS-If0 and PS-IfS, except simpler.
Since, in the inversion-for-if, we do not need to consider the C4.R
case.
--------------------------------------------------------------------------------
=======================
Lemma: Progress for ALL:
=======================
forall H, e, M, t, wp.
|- e : M t wp
==> (H, e) ~> (H', e')
\/ e is a value
Proof: Progress for Tiny-F* is not very interesting, since simple
typing ensures it.
This is an easy induction over the typing judgment, using each
inversion lemma as needed. A canonical forms lemma for function
types and integer constants is also trivial.
--------------------------------------------------------------------------------
====================================
Theorem (Partial Correctness for ALL)
====================================
We write S for type environments G having only location bindings.
(Remark: S is the store typing Sigma in the paper)
If
(H1) S |- e : M t wp
(H2) S |- p : K_Post_ALL(t)
(H3) S |= (lift_M_ALL wp) p m
(H4) S |- m ~ (asHeap H)
(H5) S |- H
then
either e is a value and S |= p e m,
or exists S', H', e', wp', m' s.t.
(a) (H, e) -> (H', e')
(b) S' |- e' : M t wp'
(c) S' |= (lift_M_ALL wp') p m'
(d) S' |- m' ~ (asHeap H')
(e) S' |- H'
Proof:
------
Case (e is a value):
We use Lemma inversion-for-values on (H1) to derive:
S |= down_M (wp ==>_M lift_M (ret_PURE e))
or
S |= down_ALL (lift_M_ALL wp ==>_ALL lift_ALL (ret_Pure e))
or
S |= forall q h. (lift_M_ALL wp) q h ==> q e h
We instantiate q and h with p and m respectively to get
S |= (lift_M_ALL wp) p (asHeap H) ==> p e m
and use (H3) and (V-ImplElim) to complete the proof.
Case (e is not a value):
Using Progress with (1), we get (a).
We then use Lemma Preservation-of-typing-for-CBV-reduction, to get (b) and (c).
--------------------------------------------------------------------------------
====================================
Theorem (Total Correctness for PURE)
====================================
If
(1) . |- e : Pure t wp
(2) . |- p : K_Post_Pure t
(3) . |= wp p
then forall H, exists v s.t.
(a) (H, e) ~>* (H, v)
(b) . |= p v
Proof:
-------
(a) follows from the normalization theorem (see pico-fstar.txt).
For (b), we use
Pure-CBV-reductions-are-included-in-pure-reduction to show that
(I1) e ~>* v
Next, we use Lemma Preservation-of-typing-on-pure-reduction to show
that . |- v : Pure t wp
Then, we use the Lemma inversion-for-values to show:
. |= downPURE (wp ==>PURE ret v)
Or . |= forall post. wp post ==> post v
which we insantiate with p for the goal.
--------------------------------------------------------------------------------