Bug in Constraint Gen with Result?

[ranjitjhala]

The following code

#![feature(register_tool)]
#![register_tool(flux)]

```rust
#[flux::sig(fn (x:u32) -> Result<{Box : x < 100}, bool>)]
pub fn foo(x: u32) -> Result<Box, bool> {
    if x >= 100 {
        return Err(false);
    }
    Ok(Box(1))
}

#[flux::sig(fn (x:u32) -> Result<{i32: x < 100}, bool>)]
pub fn bar(x: u32) -> Result<i32, bool> {
    if x >= 100 {
        return Err(false);
    }
    Ok(1)
}

produces an error

error[FLUX]: postcondition might not hold
 --> flux-tests/tests/todo/result01.rs:9:16
  |
9 |         return Err(false);
  |                ^^^^^^^^^^

Drilling in, the constraint generated is:

∀ a0: int.
  (a0 ≥ 0) =>
    ¬(a0 ≥ 100) =>
      (a0 < 100) ~ RetAt(11:5: 11:15)
      ∀ a1: bool.
        $k0(a1) => true
    (a0 ≥ 100) =>
      $k1(false) ~ Call(9:16: 9:26)
      (a0 < 100) ~ RetAt(9:16: 9:26) // seems bogus; why constrain the `Ok` case here?
      ∀ a1: bool.
        $k1(a1) => true

Note that the bar variant -- which uses an i32 instead of a Box does the right thing. Any ideas?

[nilehmann]

Oh, this is annoying, but it's working as expected. We need to adjust subtyping to make it work.

So, in bar you have to prove

Result<i32{ν: $k0(ν)}, bool{v: $k1(ν)}> <: Result<{i32{ν: true} : x > 0}, bool{ν: true}>

for the result type inside the if, where $k0 and $k1 are the fresh kvars in the instantiation for the call Err(false). The derivation tree looks like

                                    ⋮
                     -------------------------------
$k0(a) ⊧ x < 100     $k0(a) ⊢ i32[a] <: i32{ν: true}  
-------------------------------------------
$k0(a) ⊢ i32[a] <: {i32{ν: true} : x < 100}                      ⋮
--------------------------------------------     ----------------------------------
⊢ i32{ν: $k0(v)} <: {i32{ν: true} : x < 100}     ⊢ bool{ν: $k1(v)} <: bool{ν: true}
------------------------------------------------------------------------------------------
⊢ Result<i32{ν: $k0(ν)}, bool{ν: $k1(ν)}> <: Result<{i32{ν: true} : x > 0}, bool{ν: true}>

Since $k0 is not further constrained, it resolves to false, and $k0(a) ⊧ x < 100 is valid.

For foo the derivation looks like

                                  ⋮
                    ------------------------------
                    i32{ν: $k0(ν)} <: i32{ν: true}
                ----------------------------------------
⊧ x < 100       Box<i32{ν: $k0(ν)}> <: Box<i32{ν: true}>
--------------------------------------------------------
⊢ Box<i32{ν: $k0(v)}> <: {Box<i32{ν: true}> : x < 100}          ⋮
-------------------------------------------------------------------------
⊢ Result<Box<i32{ν: $k0(ν)}, …> <: Result<{Box<i32{ν: true}> : x > 0}, …>

Given the order in which the rules are applied we don't get to assume $k0 and we fail to prove x < 100.
If we push the constraint inside the box everything works out

#[flux::sig(fn(x:u32) -> Result<Box<{i32 : x < 100}>, bool>)]

We have a rule for unpacking existentials, but it is shallow:

Γ,p(a) ⊢ B[a] <: T   fresh a
---------------------------- [t-unpack]
    Γ ⊢ B{ν: p(ν)} <: T

We could generalize that to look inside boxes.

[nilehmann]

More concretely, I'm saying that the following rule should be admissible

$k0(a) ⊢ Box<i32[a]> <: {Box<i32{ν: true}> : x < 100}      fresh a
-------------------------------------------------------------------
⊢ Box<i32{ν: $k0(v)}> <: {Box<i32{ν: true}> : x < 100}  

[ranjitjhala]

Hmm, I think I'm getting the general drift here -- in the bar case you get to use the $k0 (which is false) but somehow this is not "available" in the foo case.

The use of Box may be giving the wrong idea btw -- I didn't mean the rust Box just some random opaque type which has no associated indices and lets say, has no associated type params so you can't really push the constraint "into" the i32 in foo. So lets call Bob and suppose I had

struct Bob();
 
#[flux::sig(fn (x:u32) -> Result<{Bob : x < 100}, bool>)]
pub fn foo(x: u32) -> Result<Bob, bool> {
    if x >= 100 {
        return Err(false);
    }
    Ok(Bob())
}

Now,

1. Is it possible to rewrite the spec so that it verifies currently ?
2. Does your proposed fix still apply?

Or do we need to have indexed Bob by something in order to get the k0 machinery to work?

[ranjitjhala]

For reference, this comes up here:

    // #[ensures(result.is_ok() ==> old(v_fd) < MAX_SBOX_FDS)]
    #[flux::sig(fn (&FdMap, v_fd: SboxFd) -> Result<HostFd{v: v_fd < MAX_SBOX_FDS}, RuntimeError>)]
    pub fn fd_to_native(&self, v_fd: SboxFd) -> Result<HostFd, RuntimeError> {
        if v_fd >= MAX_SBOX_FDS {
            return Err(Ebadf);
        }
        self.m[v_fd as usize]
    }

where HostFd is defined as

#[derive(Clone, Copy, PartialEq, Eq)]
pub struct HostFd(usize);

[ranjitjhala]

In fact, I'm a bit puzzled as to why HostFd{v: v_fd < MAX_SBOX_FDS} parsed in the first place as HostFd has no index? But assuming some default -- say int valued index is slapped on, then it's puzzling as to why this should behave differently than the i32 case...

[ranjitjhala]

Returning to the example -- I was expecting the thing to check precisely because of the $k0$ and false thing -- and was trying to stick the "constraint" x < 100 at the same place as the $k0 would appear, and now am wondering maybe the problem in the Bob example above -- to avoid confusion with Box -- is that there is no $k0 as there is no index?

[nilehmann]

Oh interesting. There's a difference between being unrefinable (e.g. an &T or a type parameter) and having zero indices (a struct without a refined_by). You can understand a struct with zero indices as being refined by unit, so HostFd{v: v_fd < MAX_SBOX_FDS} is perfectly fine, it's just that v has sort unit (technically it desugars to an empty list of identifiers). On the other hand, if T is a type parameter, then T{v: p(v)} is not even well-formed because type parameters are unrefinable (for now). There's some code that coerces a B{v : true} into a B[] (empty list of indices) when B has zero indices and I think it's being incorrectly applied even if the refinement is not true, so the example with Bob is dropping the $k0

That being said, it's a bit unsatisfying that the verification relies on generating an uninhabited type, e.g. it won't work for unrefinable types.