Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Use generated CONFIG_L1_CACHE_LINE_SIZE_BITS as source of truth for
the value of cacheLineBits

The requirements for cacheLineBits are numeric: we need more than 1 and
less than or equal to ptBits, which is only available as a constant
after ExecSpec.

1 is excluded, because we want to be able to fold the value of
cacheLineBits inside C cache operations, and 1 is mentioned as index
increment. No other numerals conflict in these functions.

The only observed values for cacheLineBits are 5 and 6 on Arm, but
there is no need to be more restrictive than cacheLineBits_sanity.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

None of the unfoldings of cacheLineBits turn out to be necessary.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

addrFromPPtr_mask and ptrFromPAddr_mask are only needed for masking with
cacheLineBits in CRefine. Move to CRefine where the rest of the
cacheLineBits infrastructure is.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

On AArch64 we have so far only seen cacheLineBits = 6 in the kernel.

To be future-proof, bring AArch64 proofs into line with AArch32 anyway,
rename cacheLineSize to cacheLineBits to stay consistent, and make proof
generic in cacheLineBits.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>