Compressing repeated predicates (low priority)

[enjhnsn2]

When comparing elements of fixed-size arrays in Flux, we sometimes end up repeating the same predicate many times, one for each element in the arrays.

Consider the following predicate:

flux_rs::defs! {
    fn configured_for(mpu: MPU, config: CortexMConfig) -> bool {
        map_get(mpu.regions, 0) == map_get(config.regions, 0) &&
        map_get(mpu.attrs, 0) == map_get(config.attrs, 0) &&
        map_get(mpu.regions, 1) == map_get(config.regions, 1) &&
        map_get(mpu.attrs, 1) == map_get(config.attrs, 1) &&
        map_get(mpu.regions, 2) == map_get(config.regions, 2) &&
        map_get(mpu.attrs, 2) == map_get(config.attrs, 2) &&
        map_get(mpu.regions, 3) == map_get(config.regions, 3) &&
        map_get(mpu.attrs, 3) == map_get(config.attrs, 3) &&
        map_get(mpu.regions, 4) == map_get(config.regions, 4) &&
        map_get(mpu.attrs, 4) == map_get(config.attrs, 4) &&
        map_get(mpu.regions, 5) == map_get(config.regions, 5) &&
        map_get(mpu.attrs, 5) == map_get(config.attrs, 5) &&
        map_get(mpu.regions, 6) == map_get(config.regions, 6) &&
        map_get(mpu.attrs, 6) == map_get(config.attrs, 6) &&
        map_get(mpu.regions, 7) == map_get(config.regions, 7) &&
        map_get(mpu.attrs, 7) == map_get(config.attrs, 7)
    }
}

we would instead like to write something like:

flux_rs::defs! {
    fn configured_for(mpu: MPU, config: CortexMConfig) -> bool {
        forall(idx in 0..8,
            map_get(mpu.regions, idx) == map_get(config.regions, idx) &&
            map_get(mpu.attrs, idx) == map_get(config.attrs, idx) 
        )
    }
}

I'm also open to any other concise ways to express the constraints in configured_for and similar predicates.

[nilehmann]

it'd be neat to figure out a way to rust macro this, i.e., find a way to use rust macros to generate stuff that flux can understand. That'd be way more general than anything we could implement.