# Closure notes
## 10-06-2022
TODO
- specification entailments
-- support for other function type expressions (function expression, method expressions (including interfaces with call refinement))
- call descriptions
-- invesigating examples:
--- what is hard to handle without call descriptions
---- side effects only (how to observe that closure was called in postcondition of hof)
---- unknown number of calls
--- what can we handle without call descriptions and how
---- pretty (easy to support, impressive examples that are easy to support)
---- bad (can be supported, but requires a lot of overhead)
---- what cannot be handled and why
-- how is our current appraoch stronger than no call descriptions
- pure closures
-- consolidate design
Wed: 10, 15
Mon: 15
pure f function()
motivations
- first-class pure functions
- pure heap-independent functions
- pure function types callable in spec
possible pure functions
- similar to first-class predicates
- callable spec
- callable closures
observations
- interfaces are strong enough to encode first-class functions
```
ensures y == x+1
spec f(x int) (y int)
requires c implements f
func hof(c func(x int) int) (r int) {
r := c(42) as f
}
func main() {
c := func(y int) { return y+1 }
hof(c)
}
```
```
pred mem(x, y *int) { acc(x) && acc(y) }
requires p(y)
ensures acc(p(y), 1/2)
func foo(p pred(*int), y *int) {
...
}
func main() {
x@, y@ := 0, 1
fold mem{&x}(&y)
foo(mem{&x}, &y)
}
--------
type X struct { x *int }
pred (self X) inv(y *int) { acc(self.x) && acc(y) }
requires p.inv(y)
ensures acc(p.inv(y), 1/2)
func foo(ghost p interface { pred inv(*int) }, y *int) {
...
}
func main() {
x@, y@ := 0, 1
fold X{&x}(&y)
foo(X{&x}, &y)
}
---------------------------------------------------
requires acc(x, _) && acc(y, _)
pure func f(x, y *int) int { return *x + *y }
requires g(y) == 5
func foo(g pure func(*int) int, y *int) (r int) {
...
}
func main() {
x@, y@ := 0, 1
foo(f{&x}, &y)
}
---------------------------------------------------
type PCall interface{
requires P
call(arg) res
}
requires P
ensures Q && i.call(arg) == res
spec pspec(ghost i PCall, arg) (res)
// c implements pspec{...}
----------------------
ensures res == call(arg)
spec s
requires f implements s && call(..)
func hof(f func(int) int) (r int) {
r := f(42)
}
func main() {
}
```
## older
## Question
- After writing down the encoding you currently intend, think about the following questions:
-- Can the precondition of a spec use parameters
-- Can the precondition of a spec use state variables
-- CAn the invariant of a spec use state variables
- For what / when do you need `cl is spec`? Can it be removed?
## Current Proposal
<style>
.r { color: Red }
.o { color: Orange }
.g { color: Green }
.a { color: #669ac4}
</style>
# Closures
## Language
### Closure Specification
<pre>
<span class="a">cl_spec(args, res, params, statevars) ::=</span>
requires P
invariant I
ensures Q
</pre>
- `args` and `res` are the arguments and result variables of the closure being specified. `args` can be referenced in P and Q, `res` only in Q.
- `params` are 'visible' captured variables, known to be used by the closure. They can be referenced in I and Q.
- `statevars` are values depending on the hidden state of the closure. They are heap-dependent (i.e. can be used in old()). They cannot be mentioned in access predicates. They can be referenced in Q.
- I is a single-state invariant mentioning properties that the parameters are required to satisfy whenever the closure is called and are guaranteed to satisfy at the end.
#### Closure Specification Declaration
<pre>
<span class="a">cl_spec_dec :==</span>
<span class="a">cl_spec(args, res, params, statevars)</span>
spec <span class="g">spec_name</span>[<span class="a">params</span>]<span class="r">?</span>(<span class="a">args</span>)|<span class="a">statevars</span>|<span class="r">?</span> <span class="a">res</span><span class="r">?</span>
</pre>
The closure spec declaration is placed in the outer scope (outside of other functions). `spec_name` is a new name, that must not clash with identifiers in the same scope.
#### Closure declaration
<pre>
<span class="a">cl_declaration :==</span>
closure <span class="g">spec_name</span>[<span class="a">params</span>]<span class="r">?</span> func(<span class="a">args</span><span class="r">?</span>) <span class="a">res</span><span class="r">?</span> { /* ... */ }
<span class="a">|</span>
closure spec <span class="g">new_spec_name</span>
<span class="a">cl_spec(args, res, params, _)</span>
func(<span class="a">args</span><span class="r">?</span>) <span class="a">res</span><span class="r">?</span> { /* ... */ }
</pre>
- In the first case, `spec_name` is the name of a closure specification. The `params` bind those in the specification. Normal functions can also be used as specifications.
1. If the specification is declared in the same package, in the outer scope or within the specification of the current function, it is just the spec name.
2. If the specification is declared in the same package, within the specification of another function, it is `func_name.spec_name`
3. If the specification is declared in another package, use standard package resolution.
- In the second case, `new_spec_name` is a new name, that must not clash with identifiers in the same scope. In this case, the `param` variables are determined automatically.
- No state variables are allowed in closure declarations.
#### Closure contract assertion
Each closure variable is, at all times, associated with exactly one 'proper' contract, and with potentially many 'entailed' contracts.
The proper contract of a closure is the one:
1. Specified when the closure is declared
2. Specified in the specification of the enclosing function (more on this later)
3. Obtained after assignments (i.e. after assignment `cl := cl2`, the proper contract of `cl` is the same as that of `cl2`)
The following expression evaluates to true if the current proper contract of `cl` is `spec_name`.
<pre>
cl is <span class="g">spec_name</span>
</pre>
#### Closure call
A closure can be called like normal functions, without additional annotations. The specification used is the one corresponding to its current proper contract.
<pre>
cl(<span class="a">exprs</span>)
</pre>
#### Closure spec entailment proof
<pre>
hidden invariant H
proof cl.(<span class="g">spec1</span>) implements <span class="g">spec2</span>[<span class="a">params</span>] {
<span class="a">viewshift1</span>
cl(<span class="a">args</span>)
<span class="a">viewshift2</span>
}(v1: <span class="a">exp1</span>, v2: <span class="a">exp2</span>, ..., vN: <span class="a">expN</span>)
</pre>
This is a proof that closure `cl`, with proper contract `spec1`, implements contract `spec2` in its current state. `params` bind variables captured by `cl`; the state variables of `spec2` are defined by `exp1`, ..., `expN`.
- $H$ is a single-state invariant that holds between the current state and any future state reachable without directly changing any value in the footprint of $H$ (i.e. calling `cl`, and changing variables not mentioned by $H$ between calls, is allowed). The values of the state variables can only depend on the footprint of $H$.
- Let $P_1$, $I_1$, $Q_1$ be the precondition, invariant and postcondition of `spec1`; $P_2$, $I_2$, $Q_2$ the same for `spec2`; $S$ the current state of the closure.
- `cl`, with proper contract `spec1`, implements `spec2` with the current state and hidden invariant $H$ if (the arrows represent a viewshift, which allows fold and unfold operations):
1. $S \Rightarrow H * I_2$
2. there exists $R$ such that $P_2*H*I_2 \Rightarrow R*P_1*I_1$ and $R*I_1*Q_1 \Rightarrow H*I_2*Q_2$
- `viewshift1` and `viewshift2` consist of limited operations, the same that are allowed in interface implementation proofs (e.g. fold, unfold, assert). They must preserve $H$.
- If `viewshift1` and `viewshift2` are both empty, the whole proof body (including the brackets) can be omitted. If $H$ is true, the `hidden invariant` line can be omitted.
- If `cl` is statically guaranteed to have contract `spec1`, `.(spec1)` can be omitted.
The proof remains valid until any values in the footprint of $H$ are changed.
#### Contract change
The following operation reassigns `cl` to a closure that's identical to the current one, but whose proper contract is `spec`. It can only be used if either:
- `spec` is the proper contract of `cl`. Then the operation has no effect
- there is a still-valid proof that `cl` implements `spec`
After this operation is performed, the hidden invariant $H$ specified in the implementation proof is exhaled to guarantee that `spec` continues being satisfied after this. Thus, if $H$ is non-empty, any aliases of `cl` cannot be called after this operation if they are not reassigned.
<pre>
respecify cl with <span class="g">spec</span>
</pre>
#### Closure spec assertion within HOF specification
This assertion can only be used within a function's specification, to specify the specification of a closure that it receives as an argument.
<pre>
<span class="a">cl_arg_spec :==</span>
f satisfies <span class="g">spec_name</span>[param_vars]<span class="r">?</span> stateless<span class="r">?</span>
<span class="a">|</span>
f satisfies <span class="g">new_spec_name</span>[params]<span class="r">?</span>|statevars|<span class="r">?</span> stateless<span class="r">?</span> {
<span class="a">cl_spec(args, res, params, statevars)</span>
}
</pre>
It asserts that `f` satisfies `spec_name`, where `params` must be a list of parameters that are also arguments to the higher-order function. It also asserts that there is access to the hidden state of `f`.
- If `f` is an argument of HOF, `spec` is treated as the proper contract of `f` within HOF.
- From HOF's caller's perspective, `f` satisfies `spec_name` means that either `spec_name` is the proper contract of `f`, or there is a still-valid proof that `f` implements `spec_name`.
- If `f` is among the return values of HOF, HOF guarantees that `spec_name` is the proper contract of `f`.
`stateless` means that the closure does not have a hidden state. A closure cannot be stateless if there are state variables.
#### Memory assertion
```
f.mem()
```
This assertion holds is there is access to the hidden state of `f`, which includes its state variables.
If used as a postcondition to a HOF, this means that access to `f` is preserved. From the caller's perspective, this means that the hidden invariant still holds after calling the HOF.
#### State variable access
<pre>
f.(<span class="g">spec</span>)[v]
</pre>
This expression evaluates to the current value of state variable `v` in `f`. It requires `f.mem()` and `f is spec`.
If `f` is statically guaranteed to have proper contract `spec`, `.(spec)` can be omitted.
Within the definition of `spec`, the value can simply be referenced as `v`.
## 29-04-2022
```
invariant acc(x)
ensures *x >= 0 ==> res >= 7
spec spec1[x *int]() (res int)
func main() {
y@ := 3
cl := closure spec1[&y]
func() int {
return //...
}
}
```
```
invariant acc(x)
ensures *x >= 0 ==> res >= v
spec spec1[x *int, v int]() (res int)
func main() {
y@ := 3
cl := closure spec1[&y,7]
func() int {
return //...
}
}
```
## 18-03-2022
```go=
// preserves acc(i)
// func f_spec(i *int)
//requires f satisfies f_spec
requires f satisfies f_spec(i) {
preserves acc(i)
}
requires f.inv()
func hof(f func(*int)) int {
i@ := 10
f(&i) with f_spec
return i
}
func main() {
x@ := 2
preserves acc(i)
invariant acc(&x, 1/2) && x >= 2
cl := func(i *int) {
*i = *i + x
}
/*
while (*) {
declare variables for arguments and havoc them
inhale precondition
inhale invariant
encode body
exhale invariant
exahle postcondition
}
*/
fold cl.inv()
unfold cl.inv()
x = 1
fold cl.inv() // fails
// Before using cl, check invariant still holds (obvious in this case)
proof cl satisfies /*f_spec*/ (i) {
// ...
cl(i)
// ...
} // <- can omit the proof if it's obvious (like in this case)
/*
assert cl.inv()
if (*) {
var i *int = havoc
inhale acc(i) // precondition of call specification
unfold cl.inv()
cl()
fold cl.inv()
exhale acc(i) // postcondition of call specification
assume false
}
*/
hof(cl)
// Cannot call if write access required for x
hof2(cl, &x)
x = 1
// Cannot call because the invariant was broken
hof(cl)
}
method cl_(cl: Ref, i: Ref)
requires acc(i)
requires acc(cl.x.value, 1/2) && x >= 2
requires acc(&x, 1/2) && x >= 2
ensures acc(i)
{
//...
}
method f_spec(i: Ref)
requires acc(i)
ensures acc(i)
closure:
preserves true
invariant acc(&x)
contract:
requires true
ensures exists x :: acc(&x)
method cl_$entails$f_spec(i: Ref)
requires acc(i)
ensures acc(i)
{
// ...
var cl: Ref
inhale acc(cl.x.value, 1/2) && x >= 2
cl_(cl, i)
exhale invariant
// ...
}
// exists R. P * I ⇛ P' * R and Q' * R ⇛ Q * I
// prusti: call spec pre ==> closure spec pre and old(call spec pre) ==> (closure spec post ==> call spec post)
//
// where P, Q, P', Q' is the pre and postcondition of the call specification and the pre and postcondition of the closure specification, respectily.
// And I is the invariant of the closure.
```
## 04-03-2022
```go=
package main
func main() {
count := new(int)
*count = 0
count2 := count
inc := func() int {
// invariant: old(*count) <= *count
// ensures: result == old(*count) && *count == old(*count) + 1
r := *count
*count += 1
return r
}
x := inc()
// assert x == 0
println(x)
println(*count)
// *count = 100 // fails
x = inc()
println(x)
// assert x == 1
}
```
```javascript=
domain Inc {}
function pre$inc(inc: Inc): Bool { true }
function post$inc(old_inc: Inc, inc: Inc, res: Int): Bool {
(res == inc$view$cnt(old_inc)) &&
inc$view$cnt(inc) == inc$view$cnt(old_inc) + 1
}
function hist_inv$inc(old_inc: Inc, inc: Inc): Bool {
inc$view$cnt(old_inc) <= inc$view$cnt(inc)
}
function inc$view$cnt(inc: Inc): Int
function inc$to_snapshot(inc: Ref): Inc
requires acc(inc$pred(inc), read())
ensures inc$view$cnt(result) ==
(unfolding acc(inc$pred(inc), read()) in inc.cl_capture$inc$count)
function inc2$x(cl: Inc): Int
function inc2$y(cl: Int): Bool
domain Tuple1[A] {
function create1(x: A): Tuple1[A]
function get1(t: Tuple1[A]): A
axiom { forall x: A :: {create1(x)} get1(create1(x)) == x }
axiom { forall t: Tuple1[A] :: {get1(t)} t == create1(get1(t)) }
}
domain Box[A] {
function box(x: A): Box[A]
function unbox(t: Box[A]): A
axiom { forall x: A :: {box(x)} unbox(box(x)) == x }
axiom { forall t: Box[A] :: {unbox(t)} t == box(unbox(t)) }
}
predicate intRef$count(r: Ref) {
acc(r.count) && (r.count != null ==> acc(r.count.count$val))
}
predicate inc$mem(x: Tupl1[Ref]) {
acc(get1(x).val$int)
}
predicate closure$mem(x: Tuple1[Ref])
assert acc(x.f), acc(x.g), ...
assert x == (f,g,...)
x.f = 6
field count: Ref
field count2: Ref
field count$val: Int
field val$int: Int
// main
method main()
{
// var enclosed: Ref
// count = new(int); *count = 0
var count: Ref
inhale acc(count.val$int)
count.val$int = 0
// count := new(int)
// inhale acc(intRef$count(enclosed))
// unfold intRef$count(enclosed)
// inhale enclosed.count != null
// enclosed.count.count$val := 0
// count2 := count
var count2: Ref
count2 := count
// inhale acc(enclosed.count2)
// enclosed.count2 := enclosed.count
// Encode well-formedness property of the invariants
// assume forall cl: Inc :: {hist_inv$inc(cl, cl)}
// (exists cl_: Inc :: hist_inv$inc(cl_, cl))
// ==> hist_inv$inc(cl, cl)
// assume forall cl1: Inc, cl2: Inc, cl3: Inc ::
// {hist_inv$inc(cl1, cl2), hist_inv$inc(cl1, cl3)}
// {hist_inv$inc(cl2, cl3), hist_inv$inc(cl1, cl3)}
// (hist_inv$inc(cl1, cl2) && hist_inv$inc(cl2, cl3))
// ==> hist_inv$inc(cl1, cl3)
// Encode instance creation
var inc: Tuple1[Ref] := create1(count)
fold inc$mem(inc)
var inc: Ref
// 'capture' count
inhale acc(inc$pred(inc)) && unfolding inc$pred(inc) in
inc.cl_capture$inc$count == enclosed.count.count$val
var rem_per :Perm := read()
fold intRef$count(enclosed)
exhale acc(intRef$count(enclosed), rem_per)
// Encode call
var inc_pre_snap: Inc := inc$to_snapshot(inc)
// Preconditions and invariant valid
assert pre$inc(inc_pre_snap)
&& hist_inv$inc(inc_pre_snap, inc_pre_snap)
exhale acc(inc$pred(inc))
inhale acc(inc$pred(inc))
var x: Int
var inc_post_snap: Inc := inc$to_snapshot(inc)
assume post$inc(inc_pre_snap, inc_post_snap, x)
&& hist_inv$inc(inc_pre_snap, inc_post_snap)
// inhale acc(intRef$count(enclosed), rem_per)
// unfold intRef$count(enclosed)
// unfold inc$pred(inc)
// enclosed.count.count$val := inc.cl_capture$inc$count
// fold inc$pred(inc)
// fold intRef$count(enclosed)
// exhale acc(intRef$count(enclosed), rem_per)
assert x == 0
// Update count - not allowed
// enclosed.count.count$val := 100
//enclosed.count2.count$val := 100
// Encode second call
inc_pre_snap := inc$to_snapshot(inc)
// Preconditions and invariant valid
assert pre$inc(inc_pre_snap)
&& hist_inv$inc(inc_pre_snap, inc_pre_snap)
exhale acc(inc$pred(inc))
inhale acc(inc$pred(inc))
var tmp: Int
inc_post_snap := inc$to_snapshot(inc)
assert inc$view$cnt(inc_pre_snap) == 1
assume hist_inv$inc(inc_pre_snap, inc_post_snap)
assume post$inc(inc_pre_snap, inc_post_snap, tmp)
x := tmp
assert x == 1
inhale acc(intRef$count(enclosed), rem_per)
unfold intRef$count(enclosed)
enclosed.count.count$val := 100
}
```
Sign in with Wallet
Connect another wallet