flux-rs / flux Goto Github PK

It would be really convenient to allow signatures like

#[flux::sig(fn() -> Option<_>))
fn foo() -> Option<Option<i32>> { ... }

which automatically fill in the hole with the relevant rustc thing (here, Option<i32>) but I think the current split with resolver and zip_ty makes rather difficult...

The code below fails

pub struct Bob {
    #[flux::field(RVec<i32>{n:n>0})]
    elems: RVec<i32>,
}

fails with

  |
9 |     #[flux::field(RVec<i32>{n:n>0})]
  |                             ^ expected 0 arguments, found 1

Is this a bug? Or is there some reason we can't have existentials in struct fields?

We currently accept the following definition

#[flux::refined_by(b: bool)]
enum E<T> {
    #[flux::((T) -> E<i32>[b])]
    A(T)
}

We should report this as an error because we can only "generalize" the ADT on the index and not the type parameter.

The following code panics

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

pub struct S<T> {
    v: T,
}

#[flux::sig(fn(S) -> ())]
pub fn test(bob: S<i32>) {}

with

thread 'rustc' panicked at 'assertion failed: has_default', flux-middle/src/ty/conv.rs:301:29
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

We should catch the error here https://github.com/liquid-rust/flux/blob/8e6348f18863ca79e6a843ea8e9f9d9b7dd21158/flux-desugar/src/zip_resolver.rs#200, and report the error gracefully.

My initial reaction was that indexing arrays by the length would cause inconsistencies as you could write an array where the indexed length is different than the const length

#[flux::sig(fn([i32; _][2]))]
fn myarr(a: [i32; 1]) {
    a[1]
}

But if array literal are the only way to construct arrays then I think this should be ok and it just declaring an inhabited type. However, not connecting both lengths makes code cumbersome. For example, it makes it impossible to use the result of a function like https://doc.rust-lang.org/std/primitive.u32.html#method.to_be_bytes without explicitly checking the length, even though you already know the length is 4. Ideally, arrays shouldn’t be indexed but rather we the const length should be automatically reflected into the logic when needed, i.e., the typing rule for Len should be something like

|- a: [T; n]         reflect(n) = a
———————————————————————————--———-——-
          |- Len(a): usize[a]

I’m ok with leaving the implementation like this for now as doing this reflection requires further design.

Originally posted by @nilehmann in #252 (review)

Doesn't i32 overflow after the max value - or am I reading the specification wrong?

First off- Thanks for this effort! I've been having a blast working through the code and attempting to port parts of the CBCAST stuff.

I'm curious if the following is intended behavior or user error.
Given:

#[flux::alias(type PrimeU32() = u32)]
type PrimeU32 = u32;

#[flux::constant]
const MAX_SMALL_PRIME: PrimeU32 = 97; 

#[flux::sig(fn(x: u32) -> PrimeU32{ v: v <= MAX_SMALL_PRIME })] 
pub fn a_prime(x: u32) -> PrimeU32 {
    MAX_SMALL_PRIME
}

The following error is reported:

error[FLUX]: cannot resolve `PrimeU32`
  --> /home/paul/scratch/rusttest/ver-causal/src/scratch.rs:45:27
   |
45 | #[flux::sig(fn(x: u32) -> PrimeU32{ v: v <= MAX_SMALL_PRIME })]
   |                           ^^^^^^^^

error: aborting due to previous error

This code is surprisingly hard to get to work with our current resolver pipeline.

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

type MyResult<T> = Result<T, ()>;

#[flux::sig(fn() -> MyResult<i32>)]
pub fn test() -> MyResult<i32> {
    Ok(10)
}

The trouble is that by the time we get to it, we have to resolve

• path = MyResult with args = [i32]

with what rust has (at that point in rustc_middle -- NOT at hir) namely,

• path = Result with args = [i32, ()]

Of course we do have the alias-definition (can save it in the call-chain around insert_res_for_ident)
but we actually do the zipping AFTER rustc has done the expansion which makes things very tedious AFAICT.

Ranjit asked me to post this question, although it seems rather simple (and perhaps ill-posed) to me.

I was playing around with flux and tried to extend the definition of RangeIter in range.rs to include the current index cur.

Original code:
https://github.com/liquid-rust/flux/blob/4e440050fe87c8edbd22271a761378eae3ca683e/flux-tests/tests/lib/range.rs#L7-L8

My change:

     #[flux::field({i32[@cur]:lo <= cur && cur <= hi})]
     cur: i32,

There are some other changes too, which I can post if desired.

What I ran into was an issue of not knowing how to express myself.
For the type signature of the function next I wanted to add an ensures clause that reflects the fact that in the updated RangeIter, the new cur is now either equal to cur + 1 or hi.

Original code:
https://github.com/liquid-rust/flux/blob/4e440050fe87c8edbd22271a761378eae3ca683e/flux-tests/tests/lib/range.rs#L36

My attempted change:

     #[flux::sig(fn(self: &strg RngIter[@lo, @hi, @cur]) -> Option<i32{v:lo <= v && v < hi && v == cur}> ensures self: {RngIter[lo, hi, x]: x == (cur + 1) || x == hi})]

Flux says this is wrong because x is unbound, which makes sense to me. But I can't seem to figure out how to introduce an existential like it.

I can think of three explanations:

1. I don't know the right syntax.
2. The right syntax doesn't exist, but could.
3. The right syntax doesn't exist, and this shouldn't be possible.

#[flux::sig(fn(i32[@n]) -> bool[0 < n])]
fn is_positive(x: i32) -> bool {
    match x {
        ..=0 => false,
        1.. => true,
    }
}

Flux is able to verify the function is_positive matches its signature. But if I replace the 1.. in the second match arm with _ then is says the postcondition might not hold. It seems like Flux isn't able to deduce what reaching the second match arm means about x.

I should note that I came up with the above example while trying to isolate the error I got with the following code. My apologies if I've conflated two different issues.

#[flux::refined_by(l: int)]
#[flux::invariant(l >= 0)]
pub enum List {
    #[flux::variant(List[0])]
    Nil,
    #[flux::variant((i32, Box<List[@n]>) -> List[n+1])]
    Cons(i32, Box<List>),
}

impl List {
    #[flux::sig(fn(&List[@l]) -> usize[l])]
    fn len_const_memory(&self) -> usize {
        let mut result = 0;
        let mut this: &Self = self;
        while let Self::Cons(_, tail) = this {
            result += 1;
            this = tail;
        }
        result // error: postcondition might not hold
    }
}

Right now if we annotate a function with #[flux::assume], it shouldn't check the inner body. However, it currently does. The known workaround is to annotate the function with #[flux::sig].

This appears to be a regression.

Sooner rather than later we will want to allow "assuming" types for functions from other crates /stdlib that are not part of flux. For example, we want to allow some refined signature for arr.len() that lets us check the code.

pub fn bar(arr: &[i32]) -> i32 {
    let n = arr.len();
    if 0 < n {
        arr[0]
    } else {
        0
    }
}

The following code

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

#[path = "../../lib/rvec.rs"]
mod rvec;

use rvec::RVec;

#[flux::refined_by(size:int)]
pub struct Bob {
    #[flux::field(RVec<i32>[@size])]
    elems: RVec<i32>,
}

#[flux::sig(fn(&mut Bob) -> ())]
pub fn test(bob: &mut Bob) {
    bob.elems[0] = 5;
}

Panics with

panicked at 'internal error: entered unreachable code: Field(field[0]) Bob{}', flux-typeck/src/type_env/paths_tree.rs:377:22

These two signatures panic too following work (or panic too)

// PANIC
#[flux::sig(fn(&mut Bob) -> ())]

// PANIC
#[flux::sig(fn(&mut { Bob[@n] : n > 0} ) -> ())]

But oddly, the below work as expected

// UNSAFE
#[flux::sig(fn(&mut Bob[@n]) -> ())]

// SAFE
#[flux::sig(fn(&mut Bob[@n] ) -> () requires n > 0)]

Indices on ADT sometimes have implied constraints. For example, we know by its definition that the length of a list is always non-negative. These constraints are sometimes necessary to prove the safety of a program, for example, in the following function we can only prove n != 0 in the second branch if we know the length of the tail is non-negative (n >=0 => n + 1 != 0):

#[flux::sig(fn(&List[@n]) -> bool[n == 0])]
pub fn empty(l: &List) -> bool {
    match l {
        List::Nil => true,
        List::Cons(_, _) => false,
    }
}

The current workaround is for a variant to return a constrained type. This constraint is however not verified and could introduce unsoundness. We should verify these constraints.

Pulling this remark by @nilehmann out into a separate top-level issue

#238 (comment)

Currently the following code fails with

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

#[flux::sig(fn() -> Result<i32[0], ()>)]
fn baz() -> Result<i32, ()> {
    Ok(0)
}

#[flux::sig(fn() -> Result<i32[1], ()>)]
pub fn baz_call() -> Result<i32, ()> {
    let r = baz()?;
    Ok(r + 1)
}

which fails with

error[FLUX]: unsupported type in function call
    --> flux-tests/tests/pos/surface/result00.rs:11:13
     |
11   |     let r = baz()?;
     |             ^^^^^^
     |
note: function defined here
    --> /Users/rjhala/.rustup/toolchains/nightly-2022-11-07-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs:2091:5
     |
2091 |     fn branch(self) -> ControlFlow<Self::Residual, Self::Output> {
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     = note: unsupported type `<std::result::Result<T, E> as std::ops::Try>::Residual`

error: aborting due to previous error

The following code:

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

#[flux::sig(fn(x: i32[@n]))]
fn foo(x: i32) { }

fails with

error[FLUX]: invalid alias application
 --> attic/test.rs:4:16
  |
4 | #[flux::sig(fn(x: i32[@n]))]
  |                ^

which is a confusing error since no aliases appear to be involved. The problem is that we are parsing the B[...] in x: B[...] as an alias application instead of an indexed type. I see two routes:

1. Have different syntax for alias application to avoid the confusing error.
2. Resolve aliases differently in a way that let us distinguish between an alias application and a normal indexed type. My hunch is that aliases should be resolved later anyways, so I would prefer this option.

More generally, I would like the syntax x: T to accept an arbitrary type T, and then adjust the meaning depending on what the T is. This way we could either do sugar magic or adjust error messages. For example, something that also fails to parse now is x: i32{v : v > 0}, we could either magically accept it and map x and v to the same binder in fhir or raise an error saying that existential types are not allowed in that position.

We currently accept the following definition:

#[flux::refined_by(n: int)]
struct S {
    #[flux::field(i32[n])]
    f: i32,
}

However, if we try to construct an S

fn foo() {
    let s = S { f: 1 };
}

flux will yell with

error[FLUX]: parameter inference error at function call
  --> attic/test.rs:11:13
   |
11 |     let s = S { x: 1 };
   |             ^^^^^^^^^^

The problem is that during conv, we are assuming that the parameters for the struct's single variant are the ones declared in the refined_by annotation. It is thus not necessary to declare the parameters with the @n syntax to successfully map the struct definition all the way down to rty. However, without the @ annotation we cannot instantiate the parameter when constructing the struct.

We should check that every index in the refined_by annotation has a corresponding @ annotation.

The following example

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

#[flux::refined_by(a: int, b: int)]
pub struct S {
    #[flux::field(i32[@a])]
    a: i32,
    #[flux::field(i32[@b])]
    b: i32
}

#[flux::sig(fn(S[true, 1]) -> ())]
pub fn foo(_: S) {
}

reports the following

error[FLUX]: mismatched sorts
  --> attic/test2.rs:12:18
   |
12 | #[flux::sig(fn(S[true, 1]) -> ())]
   |                  ^^^^^^^ expected `int`, found `bool`

We should point to the ill-sorted index instead of the entire list of indices.

The code below

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

#[flux::refined_by(x:int, y:int)]
pub struct Pair {
    #[flux::field(i32[@x])]
    pub x: i32,
    #[flux::field(i32[@y])]
    pub y: i32,
}

#[flux::sig(fn(Pair[@x]) -> i32)]
pub fn mytuple(p:Pair) -> i32 {
    p.x
}

just panics with

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `1`,
 right: `2`', /Users/rjhala/research/rust/flux/flux-desugar/src/desugar.rs:444:17
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

but instead we should pinpoint the offending spot.

The following currently crashes

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

pub fn mk_ten() -> Vec<i32> {
    let v = vec![1,2];
    v
}

which currently crashes with

error[FLUX]: unsupported statement
 --> flux-tests/tests/todo/vec.rs:5:13
  |
5 |     let v = vec![1,2];
  |             ^^^^^^^^^
  |
  = note: unsupported rvalue `SizeOf([i32; 2])`
  = note: this error originates in the macro `vec` (in Nightly builds, run with -Z macro-backtrace for more info)

The following

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

pub fn read_u16() -> u16 {
    let bytes: [u8; 2] = [10, 20];
    u16::from_le_bytes(bytes)
}

currently fails with

unsupported aggregate kind: `Array(u8)`

The following code

fn test() {
    let v = 42;
    let arr = [&v, &v];
}

panics with

thread 'rustc' panicked at 'internal error: entered unreachable code: `ptr(shr, _1)` <: `&{[int]. i32[^0.0] | *}` at None', flux-typeck/src/constraint_gen.rs:373:18

We should convert the ptr(shr, _1) to a shared reference as we do when checking function calls.

We often want to allow @n-binders in outputs (i.e. write signatures like

(…) -> exists n. T

for example a signature like

  fn () -> (i32[@n], Vec<i32{v: 0 <= v && v < n}>)

that says the function produces a pair of some integer and a bunch of numbers in 0..n.

Here, the function itself internally determines what the n is so we

• Can not use a forall-input that is resolved at the “caller” but
• Must use a exists-output that is generated at the call site (and of course resolved at the return site of the function body if we are checking it…)

@nilehmann any idea why the following fails with the following error

thread 'rustc' panicked at 'expcted `Node::Ty`', flux-typeck/src/type_env/paths_tree.rs:184:35

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

#[path = "../../lib/rvec.rs"]
pub mod rvec;

use rvec::RVec;

#[flux::refined_by(len: int)]
pub struct Vecs {
    #[flux::field(RVec<i32>[@len])]
    pub my: RVec<i32>,
}

#[flux::sig(fn(vecs: &strg Vecs[@n], i32) -> () ensures vecs: Vecs[n+1])]
pub fn push(vecs: &mut Vecs, value: i32) {
    vecs.my.push(value);
}

Right now we can configure the pointer with to an arbitrary integer we should restrict it to be either 32 or 64. I think we should have an enum like this

enum PointerWidth {
    W32,
    W64
}

and parse (and check) the configuration value to this enum. The advantage of the enum is that then we could have a "wildcard" width, with the semantics that the code needs to be safe for any width.

Relevant code is here https://github.com/liquid-rust/flux/blob/main/flux-common/src/config.rs#L44.

If you change the signature of get_mut in liquid-rust-tests/tests/lib/rvec.rs to

    fn<len:int>(self: RVec<T>@len; ref<self>, usize{v: 0 <= v && v < len}) -> &weak T; self: RVec<T>{v:v == len})

i.e. tweak the output from self:RVec<T>@len to self:RVec<T>{v:v == len} then a bunch of tests (that use get_mut) fail with unbound-var-in-constraint errors from fixpoint.

Triggered by the code below ...

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

#[path = "../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

#[flux::refined_by(reserve_len: int, counter: int)]
pub struct FdMap {
    #[flux::field(RVec<usize>[@reserve_len])]
    pub reserve: RVec<usize>,
}

#[flux::sig(fn (&mut FdMap[@dummy], k: usize) )]
pub fn delete(fdmap: &mut FdMap, k: usize) {
    fdmap.reserve.push(k); // triggers a crash at flux-typeck/src/constraint_gen.rs:360:18
}

which produces this

thread 'rustc' panicked at 'internal error: entered unreachable code: `&mut RVec<usize{}>[a0]` <: `ptr(mut, ?e0#0)` at Some(flux-tests/tests/todo/FdMap.rs:16:5: 16:26 (#0))', flux-typeck/src/constraint_gen.rs:360:18

The following code

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

#[flux::sig(fn (x:std::primitive::i32) -> std::primitive::i32)]
fn plop(x: std::primitive::i32) -> std::primitive::i32 {
  x + 1
}

currently crashes the parser with

error[FLUX]: syntax error: unexpected token
 --> flux-tests/tests/todo/paths.rs:4:22
  |
4 | #[flux::sig(fn (x:std::primitive::i32) -> std::primitive::i32)]
  |                      ^^

Implement support for ProjectionElem::Index. This requires a bit of refactoring to the code in https://github.com/liquid-rust/flux/blob/0520bc222f31fa9c3293f93eebe9088c5031b65f/flux-typeck/src/type_env/paths_tree.rs.

I managed to install flux and its pre-requisites. However, I cant seem to get flux

• to work outside the (flux) repo.
• nor am I able to get the VSCode + rust-analyzer integration working.

Output logs from within the the repo:

cargo test --package flux-tests
   Compiling syn v1.0.96
   Compiling log v0.4.17
   Compiling serde_derive v1.0.137
   Compiling serde v1.0.137
   Compiling serde_json v1.0.81
   Compiling rustfix v0.6.1
   Compiling compiletest_rs v0.8.0
   Compiling flux-tests v0.1.0 (/Users/nihal.pasham/devspace/rust/liquid-rust/flux/flux-tests)
    Finished test [unoptimized + debuginfo] target(s) in 6.66s
     Running tests/compiletest.rs (target/debug/deps/compiletest-9004a8be08d3093e)

running 116 tests
test [ui] pos/config/test-config.rs ... ok
test [ui] pos/config/assert_terminators/test-default.rs ... ok
test [ui] pos/config/assert_terminators/test-assume.rs ... ok
test [ui] pos/enums/invariant01.rs ... ok
test [ui] pos/casts/float_to_int.rs ... ok
test [ui] pos/casts/int_to_float.rs ... ok
test [ui] pos/enums/invariant00.rs ... ok
...
...

Outside the repo: I've added flux.sh to the $PATH path modified the $FLUX variable

#!/bin/bash

# Path to root of flux repository
FLUX=/Users/nihal.pasham/devspace/rust/liquid-rust/flux

CWD=`pwd`
cd $FLUX
TOOLCHAIN=`rustup show active-toolchain | cut -d' ' -f 1`

cd "$CWD"
rustup run "$TOOLCHAIN" cargo run --manifest-path "$FLUX/Cargo.toml" -- $@

compiling an external test project with flux.sh produces the following output

nihal.pasham@Nihals-MacBook-Pro flux-test % flux.sh ./examples/test0.rs
    Finished dev [unoptimized + debuginfo] target(s) in 0.07s
     Running `/Users/nihal.pasham/devspace/rust/liquid-rust/flux/target/debug/flux ./examples/test0.rs`
error[FLUX]: invalid flux attribute
 --> ./examples/test0.rs:4:3
  |
4 | #[flux::ty(fn(n: i32) -> i32{v: v > n})]
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to previous error

nihal.pasham@Nihals-MacBook-Pro flux-test % flux.sh ./examples/test0.rs
    Finished dev [unoptimized + debuginfo] target(s) in 0.07s
     Running `/Users/nihal.pasham/devspace/rust/liquid-rust/flux/target/debug/flux ./examples/test0.rs`
error[FLUX]: invalid alias application
  --> ./examples/test0.rs:18:17
   |
18 | #[flux::sig(fn (b:bool[true]))]
   |                 ^

error: aborting due to previous error

VSCode + rust-analyzer: compiles, even when I deliberately insert an error, which leads me to believe, something's amiss.

• added the following settings.json file to a completely new project and all I seem to get is a silent (cargo-check failed) error

{
    "rust-analyzer.checkOnSave.extraEnv": {
        "RUSTC_WRAPPER": "/Users/nihal.pasham/devspace/rust/liquid-rust/flux",
        "RUSTUP_TOOLCHAIN": "nightly-2022-11-07",
        "DYLD_FALLBACK_LIBRARY_PATH": "/Users/nihal.pasham/.rustup/toolchains/nightly-2022-11-07-aarch64-apple-darwin"
    }
}

Any pointers on what I'm doing wrong?

Some additional info:

host machine: Macbook Pro, Apple silicon

As discussed here #271 (comment)

The following triggers a parse error

#[flux::sig(fn () -> Option<Option<i32>>)]
pub fn foo() -> Option<Option<i32>> {
    None
}

but e.g. adding some random index makes it parse

#[flux::sig(fn () -> Option<Option<i32>[]>)]
pub fn foo() -> Option<Option<i32>> {
    None
}

The code for kmeans uses a cast from usize to f32. It'd be nice to add support for this. A proposed basic strategy to implement this:

1. Add a new RValue to the core ir mimicking rustc RValue::Cast. This could just initially be RValue::Cast(Operand, Ty). I don't think we need the CastKind. I'm not sure if that Ty should be a rustc_middle::ty::Ty, a liquid_rust_core::ty::Ty or maybe even a liquid-rust_core::ty::BaseTy
2. Lower rustc rvalue to core ir rvalue (here). This should be as conservative as possible only lowering casts to primitive types we know how to cast and failing otherwise.
3. Add a rule to typeck::checker::Checker::check_rvalue. There are various degrees of precision here, but in an initial implementation for a cast e as t we can forget everything we know about the type of e and just return t{v : true}. This should suffice for the use in kmeans

The following code

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

pub fn foo(z: &mut Option<i32>) -> i32 {
    match z {
        Some(n) => 1,
        None => 0,
    }
}

currently fails with at

panicked at 'expected adt at flux-tests/tests/todo/match-mut-ref.rs:5:11: 5:13 (#0)'

(I added a span on a local branch...)

Any clues on how to proceed here @nilehmann ? (I thought *z might work but it doesn't ... )

Right now the output of an annotated refined variant can be an arbitrary type.This is particularly bad if the output is a constrained types because the downcast code will asume the constraint in the output. We should check that the utput is an indexed type of the correct base type. We could enforce the output is an indexed type syntactically

Right now we fail when finding a constant we cannot "reflect" into the logic. For example, declaring

const BASE_PRIMES: [u32; 11] = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31];

fails with

error[FLUX]: invalid constant

We should instead ignore it and only fail if the constant is marked with #[flux::constant]. Relevant code https://github.com/liquid-rust/flux/blob/0520bc222f31fa9c3293f93eebe9088c5031b65f/flux-driver/src/collector.rs#L123

Right now we have a visibility setting for pretty printing kvars (https://github.com/liquid-rust/flux/blob/main/flux-middle/src/pretty.rs#L121). This setting is not very relevant now. I'd like to have three levels of visibility:

• full: print the full kvar with the self arguments and variables in scope, e.g., $k0(a0, a1, a2, [a5, a6, a7])
• only self: print only the self-arguments, e.g., $k0(a0, a1, a2)
• none: do not print any arguments, e.g. $k0

open to suggestions for the syntax in each case

@nilehmann here are a bunch of different tests that cause different panics:
adding or removing the lines as described triggers the panics.

FdMap has no indices

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

#[path = "../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

pub struct FdMap {
    #[flux::field(RVec<i32>[10])]
    pub m: RVec<i32>,
}

#[flux::refined_by(foo:int, bar:int)]
pub struct VmCtx {
    pub fdmap: FdMap,
}

impl VmCtx {
    fn m(&self) -> i32 {
        self.fdmap.m[0]
    }
}

fn fdmap_m(fdmap: &FdMap) -> i32 {
    fdmap.m[0]
}

// CRASH without [@dummy]
#[flux::sig(fn(ctx: &mut VmCtx[@dummy]) -> i32)]
pub fn testm1(ctx: &mut VmCtx) -> i32 {
    fdmap_m(&ctx.fdmap)
}

// OK
pub fn testm2(ctx: &VmCtx) -> i32 {
    fdmap_m(&ctx.fdmap)
}

// CRASH
#[flux::sig(fn(ctx: &strg VmCtx[@dummy]) -> i32 ensures ctx: VmCtx)]
pub fn test4(ctx: &mut VmCtx) -> i32 {
    // BOTH the below lines crash (same as test5)
    // fdmap_m(&ctx.fdmap) +
    // ctx.fdmap.m[0] +
    0
}

// CRASH panicked at 'called `Result::unwrap()` on an `Err` value: UnsolvedEvar { evar: ?e0#31 }', flux-typeck/src/type_env/paths_tree.rs:648:26
#[flux::sig(fn(ctx: &strg VmCtx[@dummy]) -> i32 ensures ctx: VmCtx)]
pub fn test5(ctx: &mut VmCtx) -> i32 {
    // CRASH fdmap_m(&ctx.fdmap) +
    0
}

FdMap has indices

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

#[path = "../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

#[flux::refined_by(reserve_len: int, counter: int)]
pub struct FdMap {
    #[flux::field(RVec<i32>[10])]
    pub m: RVec<i32>,
}

#[flux::refined_by(foo:int, bar:int)]
pub struct VmCtx {
    pub fdmap: FdMap,
}

impl VmCtx {
    #[flux::trusted] // COMMENT to CRASH
    fn m(&self) -> i32 {
        self.fdmap.m[0]
    }
}

// OK
fn fdmap_m(fdmap: &FdMap) -> i32 {
    fdmap.m[0]
}

// CRASH without [@dummy]
#[flux::sig(fn(ctx: &mut VmCtx[@dummy]) -> i32)]
pub fn testm1(ctx: &mut VmCtx) -> i32 {
    fdmap_m(&ctx.fdmap)
}

// OK
pub fn testm2(ctx: &VmCtx) -> i32 {
    fdmap_m(&ctx.fdmap)
}

#[flux::trusted] // COMMENT to CRASH
pub fn test0(ctx: &VmCtx) -> i32 {
    ctx.fdmap.m[0]
}

#[flux::trusted] // COMMENT to CRASH
#[flux::sig(fn(ctx: &VmCtx) -> i32)]
pub fn test1(ctx: &VmCtx) -> i32 {
    ctx.fdmap.m[0]
}

#[flux::sig(fn(ctx: &VmCtx[@dummy]) -> i32)]
pub fn test2(ctx: &VmCtx) -> i32 {
    // CRASH: ctx.fdmap.m[0] +
    fdmap_m(&ctx.fdmap) + ctx.m() + 0
}

// CRASH
#[flux::sig(fn(ctx: &mut VmCtx[@dummy]) -> i32)]
pub fn test3(ctx: &mut VmCtx) -> i32 {
    // CRASH ctx.fdmap.m[0] +
    fdmap_m(&ctx.fdmap) + 0
}

Instead of panicking when unfolding an opaque struct we should fail gracefully and report the code span that caused the unfolding.

In short, make the following test not panic with cannot find 'foo'

#![feature(register_tool)]
#![register_tool(flux)]
#![feature(custom_inner_attributes)]
#![flux::def(foo(n:int) -> bool)]
#![flux::def(bar(n:int) -> bool { foo(n) })]

#[flux::trusted]
#[flux::sig(fn(n:i32) -> bool[foo(n)])]
fn is_foo(n: i32) -> bool {
    n > 10
}

#[flux::sig(fn(n:i32) -> bool[bar(n)])]
fn is_bar(n: i32) -> bool {
    is_foo(n)
}

We should have enough support for tuples in flux-typeck, but they are not yet exposed in the surface syntax. Implementing this should require the following steps

1. Add a new Tuple variant to the surface syntax (https://github.com/liquid-rust/flux/blob/main/flux-syntax/src/surface.rs#L100).
2. Add code for desugaring the new variant (https://github.com/liquid-rust/flux/blob/main/flux-desugar/src/desugar.rs#L205).
3. Modify the parser to support tuples (https://github.com/liquid-rust/flux/blob/main/flux-syntax/src/surface_grammar.lalrpop).
4. Remove the Unit variant from surface (https://github.com/liquid-rust/flux/blob/main/flux-syntax/src/surface.rs#L121).
5. Add some pos and neg tests, e.g.,

   #[flux::sig(fn((Nat, i32)) -> Nat)]
   fn test(pair: (i32, i32)) -> i32 {
       pair.0
   }

   The support in flux-typeck should be sufficient by now, but maybe we will find some surprices and will need to fix some bugs.

We should have enough pieces in place to implement Rvalue::CheckedBinaryOp. A mildly interesting question is what type d we give to these operations. We have a couple of options. examples using add for i32

• fn(i32[@n], i32[@m]) -> exists b: bool. (bool[b], i32{v : b => v = n + m}): only say something about the result if the operation didn't overflow
• fn(i32[@n], i32[@m]) -> (bool, i32[n + m]): do not care about overflow

I added a method to rvec

    #[flux::trusted]
    #[flux::sig(fn(self: &strg RVec<T>[@n], other: &[T][@m]) -> () ensures self: RVec<T>[n + m])]
    pub fn extend_from_slice(&mut self, other: &[T])
    where
        T: Clone,
    {
        self.inner.extend_from_slice(other)
    }

but then the following code fails with Unsupported Statement

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

#[path = "../lib/rvec.rs"]
mod rvec;
use rvec::RVec;

pub fn test() {
    let mut src: RVec<u8> = rvec![1, 2, 3];
    let bytes: [u8; 2] = [4, 5];
    src.extend_from_slice(&bytes)
}

It looks like the following cast needs to be supported?

 _11 = move _12 as &[u8] (Pointer(Unsize))

as we get the error

 
error[FLUX]: unsupported statement
  --> flux-tests/tests/todo/ext00.rs:13:27
   |
13 |     src.extend_from_slice(&bytes)
   |                           ^^^^^^
   |
   = note: unsupported cast

Functions returning unit are currently supported but we have to annotate them explicitly with () as the return type. For example, we currently have to write

#[flux::sig(fn(bool[true]) -> ())]
fn assert(_b: bool) {}

but would like to write:

#[flux::sig(fn(bool[true]))]
fn assert(_b: bool) {}

Instructions:

1. Make the return type in the desugared syntax optional (https://github.com/liquid-rust/flux/blob/main/flux-middle/src/core.rs#L50) and propagate the changes.
2. Create a Ty::unit() when the return type is missing in the lowering phase (https://github.com/liquid-rust/flux/blob/main/flux-syntax/src/surface.rs#L61z).
3. Modify the surface syntax to make the return type optional (https://github.com/liquid-rust/flux/blob/main/flux-syntax/src/surface.rs#L61) and propagate changes.
4. Modify the parser (https://github.com/liquid-rust/flux/blob/main/flux-syntax/src/surface.rs#L61z) to make the return type optional. We should also support a missing return type for functions with postconditions, e.g.,

   #[flux::sig(fn(x: &strg i32[@n]) ensures x: i32[n+1])]
   fn inc(x: &mut i32) {
       *x += 1;
   }

The code below

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

#[flux::refined_by(b:bool)]
pub enum Opt<T> {
    #[flux::variant(Opt<T>[false])]
    None,
    #[flux::variant(Opt<T>[true])]
    Some(T),
}

#[flux::sig(fn(Opt<i32>[true]) -> i32)]
pub fn unwrap_i32(x: Opt<i32>) -> i32 {
    match x {
        Opt::Some(v) => v,
        Opt::None => 0,
    }
}

panics with

thread 'rustc' panicked at 'index out of bounds: the len is 0 but the index is 0', flux-typeck/src/type_env/paths_tree.rs:495:22

@nilehmann The error is in a part of paths_tree I'm unfamiliar with so would be good if you can take a look!

Code like the below should work, using just the plain rust type signatures and nothing else

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

#[lr::sig(fn() -> i32[1])]
pub fn test2() -> i32 {
   let opt = Option::Some(1);
   opt.unwrap()
}

See

1. In the example below, lr produces an error about expecting a pair (int, int) but only getting an int.

   https://github.com/liquid-rust/examples/blob/main/src/bug/mat-bug-00.rs

2. In the second example, lr just triggers some fixpoint "elaboration" crash perhaps due to some malformed sorts in the generated constraints.

   https://github.com/liquid-rust/examples/blob/main/src/bug/mat-bug-01.rs

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?

We could easily implement some basic support for these operations. For BitOr we should do the same as with BitAnd and have a refined signature for the boolean case, and an unrefined signature for the integral case. BinOp::Shl and BinOp::Shr should just have an unrefined signature for now.