Preliminary support for Const Generics in refinements

[ranjitjhala]

The following works now, but I'd like to get some feedback on simplifying etc. before moving to the actual use case of array lengths.

The main changes are these:

Checking Definitions

1. Generate fresh-singleton-names for each Const-Generic (e.g. a0)
2. Extend the TypeEnv to track a map pub struct ConstGenericArgs(FxHashMap<u32, Expr>) that maps each N to the singleton expr,
3. Use the names to do the substitution (before doing the type checking).
4. Use the TypeEnv to give occurrences of GenericParam the corresponding singleton-indexed type (e.g. usize[a0])

So given fn foo<N: usize>() -> usize{v: N < v} { N + 1 }

STEP 1. Get a name a0 STEP 2. Substitute the sig to get fn() -> usize{v: a0 < v} STEP 3. Extend the TypeEnv to track N -> a0 STEP 4. Type check using TypeEnv to get the constraint forall a0. a0 < a0 + 1

Checking Calls

Similar to the above, except that when we instantiate the generic_args we again build up a ConstGenericArgs to substitute all the generic params in the refinements with the appropriate constants e.g. 3 or the corresponding a0 singleton name at the callsite (using the caller's TypeEnv), as done in call_const_generic_args.

//-------------------------------------------------------------------------------

pub fn test000<const N: usize>() -> i32 {
    0
}

pub fn test00_client() {
    test000::<3>();
}

pub fn test001<const N: usize>() -> usize {
    N
}

//-------------------------------------------------------------------------------

#[flux::sig(fn(x:A) -> usize[N+2])]
pub fn test002<A, const N: usize>(_x: A) -> usize {
    N + 2
}

#[flux::sig(fn(x:A) -> usize[N+2])]
pub fn test002_bad<A, const N: usize>(_x: A) -> usize {
    N + 1 //~ ERROR refinement type
}

#[flux::sig(fn() -> usize[5])]
pub fn test002_client_a() -> usize {
    test002::<bool, 3>(true)
}

#[flux::sig(fn() -> usize[5])]
pub fn test002_client_a_bad() -> usize {
    test002::<bool, 30>(true) //~ ERROR refinement type
}

#[flux::sig(fn() -> usize[M+2])]
pub fn test002_client_b<const M: usize>() -> usize {
    test002::<bool, M>(true)
}

#[flux::sig(fn() -> usize[M+3])]
pub fn test002_client_b_bad<const M: usize>() -> usize {
    test002::<bool, M>(true) //~ ERROR refinement type
}

//-------------------------------------------------------------------------------

#[flux::sig(fn(x:A) -> usize{v:N < v})]
pub fn test003<A, const N: usize>(_x: A) -> usize {
    N + 2
}

#[flux::sig(fn(x:A) -> usize{v:N < v})]
pub fn test003_bad<A, const N: usize>(_x: A) -> usize {
    N //~ ERROR refinement type
}

#[flux::sig(fn() -> usize{v:3 < v})]
pub fn test003_client_a() -> usize {
    test003::<bool, 3>(true)
}

#[flux::sig(fn() -> usize{v:3 < v})]
pub fn test003_client_a_bad() -> usize {
    test003::<bool, 2>(true) //~ ERROR refinement type
}

#[flux::sig(fn() -> usize{v:M < v})]
pub fn test003_client_b_bad<const M: usize>() -> usize {
    test003::<bool, 2>(true) //~ ERROR refinement type
}

//-------------------------------------------------------------------------------

#[flux::sig(fn() -> usize{v: 10 < v})]
pub fn test004<const N: usize>() -> usize {
    if 10 < N {
        N
    } else {
        15
    }
}

#[flux::sig(fn() -> usize{v: 10 < v})]
pub fn test004_bad<const N: usize>() -> usize {
    if 9 < N {
        N //~ ERROR refinement type
    } else {
        15
    }
}

#[flux::sig(fn() -> usize{v:10 < v})]
pub fn test004_client_a() -> usize {
    test004::<3>()
}

#[flux::sig(fn() -> usize{v:10 < v})]
pub fn test004_client_b<const M: usize>() -> usize {
    test004::<M>()
}

#[flux::sig(fn() -> usize{v:100 < v})]
pub fn test004_client_a_bad() -> usize {
    test004::<3>() //~ ERROR refinement type
}

#[flux::sig(fn() -> usize{v:100 < v})]
pub fn test004_client_b_bad<const M: usize>() -> usize {
    test004::<M>() //~ ERROR refinement type
}

[ranjitjhala]

hang on, let me merge first...

[ranjitjhala]

@nilehmann -- the above is ready for review. One annoying thing is the addition of the &ConstGenericArgs::empty() to all the instantiate_* calls, maybe you can think of something cleaner?

[ranjitjhala]

Added the stuff for arrays too, so this works:

pub fn test01<const N: usize>(arr: &[i32; N]) -> i32 {
    arr[0] //~ ERROR assertion might fail
}

pub fn test02<const N: usize>(arr: &[i32; N]) -> i32 {
    if N > 0 {
        arr[0]
    } else {
        99
    }
}

[nilehmann]

This implementation is trickier than I thought because you need to pass the list of generated vars to every call to instantiate not just instantiate_identity. So, after writing the review, I feel more in favor of the alternative strategy we discussed, i.e., add the list of generics as a node to the RefineTree. I have a proof of concept of this alternative strategy for (early) refinement parameters https://github.com/flux-rs/flux/compare/a6baf287b074c60663ef95d3d4e2cdb0562f06fa..77cccecec759072bdf12aec4e414f7aac6ca6cbb#diff-29db6f382c499c956b208bc768e6f78db625b7a8a9c529c0487ce9b9700a219a. I ended up not merging it because of some issues with function sorts that wouldn't be a problem for const generics.

[ranjitjhala]

But how does that address the kvar / scope issue?

On Mon, Jun 17, 2024 at 11:53 AM Nico Lehmann @.***> wrote:

This implementation is trickier than I thought because you need to pass the list of generated vars to every call to instantiate not just instantiate_identity. So, after writing the review, I feel more in favor of the alternative strategy we discussed, i.e., add the list of generics as a node to the RefineTree. I have a proof of concept of this alternative strategy for (early) refinement parameters https://github.com/flux-rs/flux/compare/a6baf287b074c60663ef95d3d4e2cdb0562f06fa..77cccecec759072bdf12aec4e414f7aac6ca6cbb#diff-29db6f382c499c956b208bc768e6f78db625b7a8a9c529c0487ce9b9700a219a https://urldefense.com/v3/__https://github.com/flux-rs/flux/compare/a6baf287b074c60663ef95d3d4e2cdb0562f06fa..77cccecec759072bdf12aec4e414f7aac6ca6cbb*diff-29db6f382c499c956b208bc768e6f78db625b7a8a9c529c0487ce9b9700a219a__;Iw!!Mih3wA!B_33qdAIfM5xkUozvinPOANf7gtGq7CyCT9-9-JtOvYolOtgnpWHASjzKi1nrIPhkGmA21qLnfM55dHNEvA0MFhN$. I ended up not merging it because of some issues with function sorts that wouldn't be a problem for const generics.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/flux-rs/flux/pull/637*issuecomment-2174204034__;Iw!!Mih3wA!B_33qdAIfM5xkUozvinPOANf7gtGq7CyCT9-9-JtOvYolOtgnpWHASjzKi1nrIPhkGmA21qLnfM55dHNEt44OekF$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGZ2SGSNRZUUXH6YXLZH4WBFAVCNFSM6AAAAABJKR5UMSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNZUGIYDIMBTGQ__;!!Mih3wA!B_33qdAIfM5xkUozvinPOANf7gtGq7CyCT9-9-JtOvYolOtgnpWHASjzKi1nrIPhkGmA21qLnfM55dHNEhFnX7JO$ . You are receiving this because you were mentioned.Message ID: @.***>

--

• Ranjit.

[nilehmann]

But how does that address the kvar / scope issue?

We modify Scope::iter to also return the const generics https://github.com/flux-rs/flux/compare/a6baf287b074c60663ef95d3d4e2cdb0562f06fa..77cccecec759072bdf12aec4e414f7aac6ca6cbb#diff-29db6f382c499c956b208bc768e6f78db625b7a8a9c529c0487ce9b9700a219aR105.

[ranjitjhala]

@nilehmann -- I made the changes so all the stuff is in Root and the ConstGeneric is carried along to fixpoint...

[ranjitjhala]

The one tedious thing is you have to pass tcx into instantiate as we need tcx to convert the GenericArg corresponding to a number e.g. 3 to the actual u128 ...

[ranjitjhala]

Have made all the changes except the ParamConst thing, see discussion above -- will take a look with fresh eyes!

[ranjitjhala]

ok I believe I addressed all comments -- in particular made all the ParamConst back into DefId.

Will merge if CI is green!