make proofs generic in `config_ARM_PA_SIZE_BITS_40`

seL4 / l4v

seL4 specification and proofs

https://sel4.systems

Other

504 stars 105 forks source link

make proofs generic in `config_ARM_PA_SIZE_BITS_40` #774

Closed lsf37 closed 2 months ago

lsf37 commented 3 months ago

This needed only very minor tweaks, and interestingly only involved more unfolding of Kernel_Config.config_ARM_PA_SIZE_BITS_40_def.

Most of the unfoldings involved goals where concrete vmlevel numbers now overflow earlier (3 = 0 for config_ARM_PA_SIZE_BITS_40, instead of 4 = 0).

Together with the maxIRQ pull request #773, this enables the proof to work for the zynqmp (zcu102) and bcm2711 (rpi4) platforms. See also seL4/seL4#1290.

lsf37 commented 3 months ago

Have added solves in the missing cases and added a few more comments for unfoldings.