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]

@ranjitjhala First round of comments.

About the proliferation of ConstGenericArgs::empty(), I'm not entirely sure what's the best strategy, but here is my thinking.

Right now we have two functions to eliminate an EarlyBinder, instantiate and instantiate_identity.

• instantiate: This one is meant to be used when calling/using an item external to the function being checked.
• instantiate_identity: This one is meant to be used when going inside an item (function, adt, ...) to signal that all parameters are now "free" (i.e., universally quantified). In rustc, this is a no-op because (early) bound parameters are represented the same as free parameters.

Since we need to make the "freeing" of refinement parameters explict, I propose we separate this into three functions

• instantiate: This remains the same
• enter_forall (not sure about the name): This is used when going inside an item. We should use this in all the places where we are currently calling instantiate_identity with refine_params and const_generic_args.
• instantiate_identity: This becomes a no-op and should be used in places where we enter an item (and we are technically freeing parameters) but the thing we are doing doesn't depend on refinements. I think the only place that qualifies for this is compare_impl_item where we manipulate sorts, which should not depend on refinements. The worst that can happen if we call this function by mistake instead of enter_forall is that we free parameters implicitly causing a crash when encoding into fixpoint.

Next, I'd make instantiate take the ConstGenericArgs and make the computation in call_const_generic_args inside instantiate. This will make it evident that some places are missing the instantiation of const generics (e.g. place_ty). To make this more manageable, we could put refine_params and geneneric_arg_consts in the same struct (refine_params is already being passed around)

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

[nilehmann]

@ranjitjhala Looks good. There are still some comments from the first review that need attention. I also added a couple of extra small comments.

It is unfortunate that we have to pass tcx to instantiate, but we almost always have access to it so it shouldn't be too bad.

[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!