Supporting const sorts that are not integers

[ranjitjhala]

Specifically, related to #886 and @vrindisbacher's #932

Summarizing the discussion on slack with @nilehmann to support the following

#![flux::defs(
    fn is_start(x:bitvec<32>) -> bool { x == BLAH }
)]

#[flux::const(Bv32[int_to_bv32(0x4567)])] 
const BLAH: Bv32 = Bv32::new(0x4567)

It sounds to me like there are three distinct things we need.

STEP 1. Use the signature of a const in other specifications (which is #932)
STEP 2. Check the signature of a const against its own (MIR) definition
STEP 3. Synthesize the signature of a const from its definition (which is #886)

For (1) we need to

• [Nico] Get the sort from the underlying rust type. We already have https://github.com/flux-rs/flux/blob/main/crates/flux-middle/src/sort_of.rs/#L31 to get the sort from a rustc_middle::ty::Ty we can use to avoid circularities
• Then extract the index to use to reflect the const BLAH into the refinement logic i.e. replace occurrences of BLAH in refinements with int_to_bv32(0x4567) ?

Specifically, get the below working

#![flux_rs::defs(
    fn is_start(x:bitvec<32>) -> bool { x == START }
)]

#[flux_rs::opaque]
#[flux_rs::refined_by(val: bitvec<32>)]
pub struct BV32(u32);

impl BV32 {
    #[flux_rs::trusted]
    #[flux_rs::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
    fn new(val: u32) -> Self {
        BV32(val)
    }
}

#[flux_rs::constant(BV32[int_to_bv32(0x4567)])]
pub const START: BV32 = BV32::new(0x4567);

// USE: get the below to be SAFE
#[flux_rs::sig(fn () -> BV32[START])]
fn test1() -> BV32 {
    BV32::new(0x4567)
}

// (1) USE: get the below to be SAFE
#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
fn test2() -> BV32 {
    BV32::new(0x4567)
}

// (2) CHECK: get the below to be UNSAFE
#[flux_rs::constant(BV32[int_to_bv32(0x456)])]
pub const BAD: BV32 = BV32::new(0x4567);

// (3) INFER: elide the `flux_rs::constant` signature...

[nilehmann]

Something else to consider is that we probably want to keep the behavior we already have for integers where we evaluate and then map the bytes, so the reflection strategy needs to change depending on the type.

Also, a couple of pointers:

1. We do "const reflection" for integers here https://github.com/flux-rs/flux/blob/main/crates/flux-infer/src/fixpoint_encoding.rs/#L1283-L1291
2. We assume consts are ints during sort checking here https://github.com/flux-rs/flux/blob/main/crates/flux-fhir-analysis/src/wf/sortck.rs/#L291-L293

[ranjitjhala]

Yes, I didn't want to break the existing stuff with integer constants, so have just added an Expr annotation that specifies the value of const with a non-integral Sort.

[nilehmann]

Moving discussion in #932 (comment) here

@ranjitjhala it's silly that we didn't anticipate this but if we write

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

we need to make sure we give START type BV32[bv_int_to_bv32(0x4567)] when used inside a function.

Right now we lower START as an opaque constant in mir bodies which we don't give a type specific enough.

concretely, the following should work

#[flux::opaque]
#[flux::refined_by(val: bitvec<32>)]
pub struct BV32(u32);

impl BV32 {
    #[flux::trusted]
    #[flux::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
    const fn new(val: u32) -> Self {
        BV32(val)
    }
}

#[flux_rs::constant(bv_int_to_bv32(0x4567))]
pub const START: BV32 = BV32::new(0x4567);

#[flux_rs::sig(fn () -> BV32[START])]
pub fn test1() -> BV32 {
    START
}

[nilehmann]

Specifically, if we type constants properly we should be able to get rid of this hack

flux/crates/flux-rustc-bridge/src/lowering.rs

Lines 615 to 621 in 744fa24

	// HACK(nilehmann) we evaluate the constant to support u32::MAX
	// we should instead lower it as is and refine its type.
	let const_ = constant
	.const_
	.eval(tcx, ParamEnv::empty(), DUMMY_SP)
	.map(|val| Const::Val(val, constant.const_.ty()))
	.unwrap_or(constant.const_);