# Associated Predicates
## Problem: Specify bounds checking for `Vec` accesses?
Suppose that `v : Vec<T>` and suppose that we want to verify `... v[i]...`, which gets translated into the MIR
```rust
let s = Deref::deref(&v);
let x = Index::index(s, i);
```
So, the "bounds check" must be specified by refinements for `Deref::deref` and `Index::index`.
### 1. Spec for `Deref` and `Index`
```rust
impl<T> Deref for Vec<T> {
type Output = [T];
#[flux::sig(fn deref(&Vec<T>[@n]) -> &[T][n])]
fn deref(&self) -> &[T] {
...
}
}
```
Sadly, `Index::index` is defined in a *generic* fashion for any `I` that implements `SliceIndex`, so the "bounds check" needs to be abstracted over any such `I`.
```rust
impl<T, I> Index<I> for [T]
where
I: SliceIndex<[T]>
{
type Output = I::Output
#[flux::sig(&[T][@n], I{v: <I as SliceIndex<[T]>>::contained(v, n)})]
fn index(&self, idx: I) -> &Self::Output {
idx.get(self)
}
}
```
### 2. Associate Predicate with Trait `SliceIndex`
Here `contained` is an **associated predicate** of the trait `SliceIndex`
```rust
#[flux::generics(Self as base)]
#[flux::predicate{contained: (Self, T) -> bool}]
pub unsafe trait SliceIndex<T as base>: Sealed where T: ?Sized { ... }
```
and we can (finally) define the bounds check by defining `contained` for the `impl` of `SliceIndex` for `usize`
```rust
#[flux::predicate{contained : |idx, n| idx < n}]
impl<T> SliceIndex<[T]> for usize {...}
```
## Sound Version: Predicate on `MyTrait`
```rust
trait MyTrait {
predicate f: (Self) -> bool
#[flux::sig({Self[@n] | <Self as MyTrait>::f(n)}) -> i32]
fn method(&self) -> i32;
}
impl MyTrait for i32 {
predicate f = |x| x > 0;
#[flux::sig({Self[@n] | <Self as MyTrait>::f(n)}) -> i32]
#[flux::sig({Self[@n] | n > 0}) -> i32]
fn method(&self) -> i32 {
0
}
}
fn test(x: i32) {
x.method() // fail because we don't know x > 0
}
```
## Unsound Version: Predicate on `impl MyTrait for i32`
```rust
trait MyTrait {
fn method(&self) -> i32;
}
impl MyTrait for i32 {
predicate f = |x| x > 0;
#[flux::sig({Self[@n] | <Self as MyTrait>::f(n)}) -> i32]
fn method(&self) -> i32 {
0
}
}
fn test(x: i32) {
x.method() // fail because we don't know x > 0
}
```
## Associated Predicates
### Step 1: Refinements on `Self`
**nico(12/28/23):** just realized this example shouldn't work as is because the signature of `test` forgets the abstract refinement and we shouldn't create a kvar for `T` because it's bounded
```rust
#[flux::generics(Self as base)]
trait MyTrait {
#[flux::sig(fn<refine p: Self -> bool>(&Self{v: p(v)}) -> Self{v: p(v)})]
fn method(&self) -> Self;
}
impl MyTrait for i32 {
#[flux::sig(fn<refine p: Self -> bool>(&Self{v: p(v)}) -> Self{v: p(v)})]
fn method(&self) -> Self {
*self
}
}
fn test<T: MyTrait>(x: T) -> T {
x.method()
}
fn client() {
assert(test(0) == 0);
}
```
**rj (12/29/23):** Ok, instead I've gotten this working.
```rust
#[flux::generics(Self as base)]
pub trait MyTrait {
#[flux::sig(fn<refine p: Self -> bool>(&Self{v: p(v)}) -> Self{v: p(v)})]
fn foo(&self) -> Self;
}
#[flux::sig(fn<T as base, refine q: T -> bool> (&T{v:q(v)}) -> T{v: q(v)})]
pub fn bar<T: MyTrait>(x: &T) -> T {
x.foo()
}
```
### Step 2: Associate Predicates with `trait`
```rust
#[flux::generics(Self as base)]
#[flux::predicate{ f : (Self) -> bool }]
trait MyTrait {
fn method(&Self) -> i32;
}
#[flux::predicate{ f : |x| { 0 < x } }]
impl MyTrait for i32 {
fn method(&Self) -> i32 { ... }
}
#[flux::sig({&T[@x] | <T as MyTrait>::f(x)})]
fn bob<T: MyTrait>(x: &T) {
x.method()
}
fn test(){
let z0 = 0;
bob(&z0); // reject!
let z1 = 1;
bob(&z1); // accept
}
```
### Step 3: Use predicates on Trait Methods
* `v1` put sig on `impl`
* `v2` put sig on `trait`
```rust
// #[flux::predicate(f: (Self) -> bool)];
//could use 'predicate' or similar, but I like the sound of 'refined_by'
#[flux::predicate{ f : (Self) -> bool }]
trait MyTrait {
// (v2) #[flux::sig({&Self[@n] | <Self as MyTrait>::f(n)}) -> i32]
fn method(&Self) -> i32;
}
#[flux::predicate{ f : |x| { 0 < x } }]
impl MyTrait for i32 {
// (v1) #[flux::sig({&Self[@n] | <Self as MyTrait>::f(n)}) -> i32]
fn method(&Self) -> i32 { ... }
}
#[flux::sig({&T[@x] | <T as MyTrait>::f(x)})]
fn bob<T: MyTrait>(x: &T) {
...
// (v2) check this call
x.method()
...
}
#[flux::sig({&i32[@x] | 0 < x})]
fn bob1(x: &i32) {
// (v1) check this call
x.method()
}
fn test(){
let z0 = 0;
bob(&z0); // (v0) reject!
let z1 = 1;
bob(&z1); // (v0) accept
}
```
## Variant: Use Associated Type (Alias)
The trouble with the associated predicate is that it pulls all of `Ty` or `RTy` into the `Expr` language if we are to properly represent `<T as MyTrait>::f(x)` as a refinement.
Instead, we might use a **type alias** like so:
```rust
#[flux::generics(Self as base)]
#[flux::alias(type MyTy)] // 1. specify an associated type MyTy (with no params)
trait MyTrait {
fn method(&Self) -> i32;
}
#[flux::alias(type MyTy = &Self{v: 0 < v})] // 2. implement the associated type
impl MyTrait for i32 {
fn method(&Self) -> i32 { ... }
}
#[flux::sig(fn (<T as MyTrait>::MyTy))] // 3. use the associated type
fn bob<T: MyTrait>(x: &T) {
x.method()
}
fn test(){
let z0 = 0;
bob(&z0); // reject!
let z1 = 1;
bob(&z1); // accept
}
```
## Vec/Index with Associated Type
**Step 1** Specify an associated type Valid (with param n:int)
```rust=
#[flux::alias(type Valid(n:int))]
pub unsafe trait SliceIndex<T>: Sealed
where
T: ?Sized,
{ ... }
```
**Step 2** Implement `Valid` for `usize` and `SliceIndex<[T]>`
```rust=
#[flux::alias(type Valid(n:int) = Self{v:v < n})]
impl<T> SliceIndex<[T]> for usize {
type Output: ?Sized;
}
```
**Step 3** Use `Valid` to specify bounds on `Index::index`
```rust
impl<T, I> Index<I> for [T]
where
I: SliceIndex<[T]>
{
type Output = I::Output
#[flux::sig(fn(&Self[@n], idx:<I as SliceIndex<[T]>::Valid(n)))] -> &Self::Output
fn index(&self, idx: I) -> &Self::Output {
idx.get(self)
}
}
```
## Associated Predicates via Abstract Refinements
### Step 0: New concrete syntax for predicate application.
In LH you can write `T<p>` to mean `T{v: p(v)}`.
This generalizes to multiple parameters too so something like
`T<p x>` which means `T{v: p(x,v)}`
What is a good syntax for this in Flux where you don't have partial application?
*Default Option* just use the same as for existential types so
T{v:<T as Trait>::p(v)}
T{v:<T as Trait>::p(x, v)}
(Lets stick with the above for now, bit verbose but whatever.)
### Step 1: Define Projection-Predicates
```rust
struct ProjPred {
trait_id: DefId,
generic_args: GenericArgs,
pred: Symbol,
}
```
So `<T as MyTrait>::f` is represented as `proj_pred` defined as
```rust
let proj_pred = ProjPred { trait_id: MyTrait, generic_args: [T], pred: "f" }
```
### Step 2: Extend `rty::TyKind` with a proj-pred-application
```rust
struct ProjApp {
base: BaseTy,
pred: ProjPred,
args: RefineArgs,
}
pub enum TyKind {
Indexed(BaseTy, Expr),
Exists(Binder<Ty>),
Constr(Expr, Ty),
App(Binder<ProjApp>),
...
}
```
So
```rust
T{v:<T as MyTrait>::p(x, v)}
```
is represented as
```rust
App(Binder(ProjApp{base: T, pred: proj_pred, args:[x, #0]}))
```
### Step 3: Pred-App instantiation
When a predicate is "instantiated" e.g. when you instantiate `T` as `i32` and you have an `impl`
```rust
#[flux::predicate{ f : |a, b| { b < a } }]
impl MyTrait for i32 {...}
```
then you instantiate the type
```rust
T{v:<T as MyTrait>::p(x, v)}
```
represented as
```rust
App(Binder(ProjApp{base: T, pred: proj_pred, args:[x, #0]}))
```
to
```rust
Exists(Binder(Constr(#0 < x, i32[#0])))
```
where the (concrete) `proj_pred` params `[a,b]` are substituted by `[x,v]`, that is
1. The `base` becomes `i32[#0]` or `Indexed(i32, #0)` and
2. The `pred`, and `args` becomes `i32::f` with substitution `[a := x, b := #0]`
### Full Example
```rust
// Step 1 : declare -------------------------------
#[flux::generics(Self as base)]
#[flux::predicate{ f : (Self) -> bool }]
trait MyTrait {
fn method(&Self) -> i32;
}
// Step 2 : abstract ------------------------------
#[flux::sig({&T[@x] | <T as MyTrait>::f(x)})]
fn bob<T: MyTrait>(x: &T) {
x.method()
}
// Step 3 : implement -----------------------------
#[flux::predicate{ f : |x| { 0 < x } }]
impl MyTrait for i32 {
fn method(&Self) -> i32 { ... }
}
// Step 4 : concretize ----------------------------
fn test(){
let z0 = 0;
bob(&z0); // reject!
let z1 = 1;
bob(&z1); // accept
}
```
## Nico(01/08/24):
I was thinking a different representation. I'd represent it like so
```rust
// This is analogous to `AliasTy` so I'd call it `AliasPred`
// instead of `ProjPred`
pub enum AliasPred {
trait_id: DefId,
name: Symbol,
generic_args: GenericArgs,
}
pub enum TyKind {
...
Constr(Pred, Ty),
...
}
pub enum Pred {
Expr(Expr),
Alias(AliasPred, RefineArgs)
}
```
Then for your example above we represent `{T[x] | <T as MyTrait>::f(x)}` as
```rust
TyKind::Constr(Pred::Alias(AliasPred { .. }, List(x)), T[x])
```
And if we know `T` is `i32` we can normalize it to
```rust
TyKind::Constr(Pred::Expr(0 < x), i32[x])
```
Alternatively, since `<T as MyTrait>::f` only ever appears applied, we do not need to represent it separate from the arguments and it can all go inside `AliasPred`, i.e.:
```rust
pub enum AliasPred {
trait_id: DefId,
name: Symbol,
generic_args: GenericArgs,
refine_args: RefineArgs,
}
pub enum TyKind {
...
Constr(Pred, Ty),
...
}
pub enum Pred {
Expr(Expr),
Alias(AliasPred)
}
```
Finally, I think we will need a type like:
```rust
pub enum AssocPred {
name: Symbol,
/// The instantiated predicate. |x| 0 < x in the example
pred: Binder<Expr>
// ... maybe more stuff
}
// Something tricky about this definition which I don't see clearly right now
// is that the `Binder<Expr>` is under the `Generics` of the trait, i.e., the
// sorts in the `Binder` may refer to these generics.
```
and a query `assoc_predicates: DefId -> List<AssocPred>` that given the `DefId` of an `impl` block returns the list of associated predicates for that instance. This is analogous to `AssocItem` with the difference that we store the instantiated predicate directly in it instead of requiring an additional query.
## Refining Iterators
```rust=
#[flux::refined_by(is_some: bool)]
enum Option<T>;
#[flux::assoc(fn step(x: Self, y: Self) -> bool]
#[flux::assoc(fn finished(x: Self) -> bool]
trait Iterator {
type Item;
#[flux::sig(
fn(self: &strg Self[@start]) -> Option<Self::Item>{v: Self::finished(start) => !v.is_some}
ensures self: Self{end: Self::step(start, end)}
)]
fn next(&mut self) -> Option<Self::Item>;
}
```
## enumerate using Iterator?
```rust
#[flux::refined_by(idx: int, inner: I)]
struct Enumerate<I>;
#[flux::assoc(
fn step(x: Self, y: Self) -> bool {
x.idx + 1 == y.idx && I::step(x.inner, y.inner)
}]
#[flux::assoc(
fn finished(x: Self) -> bool {
I::finished(x.inner)
}]
impl<I> Iterator for Enumerate<I>
where I: Iterator
{
type Item = (usize, I::Item);
#[flux::sig(
fn(self: &strg Self[@start]) -> Option<(usize[start.idx], I::Item)>{v: Self::finished(start) => !v.is_some}
ensures self: Self{end: Self::step(start, end)}
)]
fn next(&mut self) -> Option<Self::Item>;
}
```
## Wanted: DEFAULT associated refinement implementations
How about we just provide the default in the trait definition, e.g.
```rust=
#[flux::assoc(fn f(x: int) -> int { x + 1 })]
trait MyTrait {}
struct Add1;
// Can skip the next line
// #[flux::assoc(fn f(x: int) -> int { x + 1 })]
impl MyTrait for Add1 {}
struct Add2;
#[flux::assoc(fn f(x: int) -> int { x + 2 })]
impl MyTrait for Add2 {}
#[flux::sig(fn() -> i32{v: v == <Add1 as MyTrait>::f(0)})]
fn test1() -> i32 { 1 }
#[flux::sig(fn() -> i32{v: v == <Add2 as MyTrait>::f(0)})]
fn test2() -> i32 { 2 }
```
```rust
#[flux::refined_by(idx: int, fin: int)]
struct RangeIterator {
idx: i32[idx],
fin: i32[fin],
}
impl RangeIterator {
fn new(idx: i32, fin: i32) -> Self[idx, fin] {
RangeIterator { idx, fin }
}
}
#[flux::assoc(fn step(now:Self, next:Self) -> bool { true })]
#[flux::assoc(fn done(now:Self) -> bool { true })]
trait Iterator {
fn next(self: &strg Self[@now]) -> Option<Self::Item>[#b]
ensures self: Self{next: b => step(now, next)}, b || done(now)
// variant
fn next(self: &strg Self[@now]) -> Option<Self::Item>[!done(now)]
ensures self: Self{next: step(now, next)}, b || done(now)
}
impl Iterator for RangeIterator {
reft fn step(now: RangeIterator, next: RangeIterator) -> bool {
next.idx == now.idx + 1 && next.fin == now.fin
}
reft fn done(now: RangeIterator) -> bool {
now.idx == now.fin
}
type Item = i32;
fn next(self: &strg Self[@now]) -> Option<i32>[#b]
ensures self: Self{next: b => (next.idx == now.idx + 1 && next.fin == now.fin)},
b || now.idx == now.fin
{
let idx = self.idx;
let fin = self.fin;
if idx == fin {
None
} else {
self.idx = idx + 1;
Some(idx)
}
// if idx < fin {
// self.idx = idx + 1;
// Some(idx)
// } else {
// // !(idx < fin)
// // idx == fin
// None
// }
}
}
fn test(){
let mut ctr = 0;
let rng = RangeIterator(1,5);
// rng : { idx = 1, step = |(now, next)| { next.idx = now.idx + 1 && now.fin == now.fin }, done = |now| { now.idx == now.fin} }
while let Some(_) = rng.next() {
// inv(ctr = rng.idx)
ctr += 1;
}
// need rng.idx = 5 when we break out.
assert(ctr == 5)
}
```
## The trouble with default trait specifications
```rust
trait Bob {
fn foo(i32) -> i32
}
struct Evan {}
impl Bob for Evan {
fn foo(x:Pos) -> Pos {
10 / x
}
}
fn mumble<T:Bob>(x:T) {
<T as Bob>::foo(0)
}
fn mumble_with_evan() {
mumble(Evan{})
}
/*
(Nat) -> Nat <: (i32) -> i32
post1 <: post2
pre2 <: pre1
----------------------------------------------
(pre1) -> post1 <: (pre2) -> post2
*/
```
## Substitution Etc.
```rust!
#![allow(dead_code)]
#[flux::sig(fn (f: fn(nat) -> nat) -> nat {
fn foo(f: fn(i32) -> i32) -> i32 {
f(10)
}
#[flux::sig(fn (x:i32) -> i32[x+1])]
fn inc(x: i32) -> i32 {
x + 1
// if x <= 100 {
// x
// } else {
// 100
// }
}
fn baz() -> i32 {
let ptr = CAST(inc) // CAST: FnDef
foo(ptr) // CALL: inc_sig_as_ptr <: nat -> nat
}
```
```rust
// CURRENT Representation of `inc`
inc_sig := EarlyBinder(x: int, Binder(fn(int[x]) -> i32[x+1]))
inc_sig_as_ptr := EarlyBinder([], Binder(x:int, fn(int[x]) -> i32[x+1]))
```
**Option 1:**
- Just do CHECK (against unrefined sig of cast-target) as CAST site
**Option 2:**
- CAST: Convert `inc_sig` -> `inc_sig_as_ptr` (if possible, i.e. no predicates etc.)
- CALL: do the CHECK
- If `x` is mentioned in a predicate ...
Sign in with Wallet
Connect another wallet