---
# System prepended metadata

title: Associated Predicates

---

# 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 ... 

