I need to know that BitVec's are bounded by 2^n.

[fshaked]

I need the following information about the representation of BitVec.

Axiom denote_bv_max : forall (n : N) (m : denote_type (BitVec (N.to_nat n))),
      m < 2 ^ n.

I need this axiom to prove the land_shiftr lemma, which I use in the proof of step_tlul_adapter_reg in CavaIncrementDevice.v.

[blaxill]

This is not currently derivable, but it should be fine to require this as a precondition:

72a0eb7

All the primitive operations effectively have such implicit preconditions and should be closed under this precondition (given inputs satisfy the correct bounds, output from a primitive should satisfy the correct bounds). e.g. BinBitVecAddU BinBitVecSubU UnBitVecShiftLeft are all defined _ mod [relevant bound].

An alternative could be to use coqutil's word or similar, but it would be a big change at this point.

[jadephilipoom]

Another strategy I've found helpful, especially if you want to avoid the precondition, is to just truncate the number in the spec, e.g.:

silveroak/silveroak-opentitan/hmac/hw/Sha256Properties.v

Lines 394 to 397 in db74867

	Lemma step_bvconcat {n m} (x : denote_type (BitVec n)) (y : denote_type (BitVec m)) :
	step (bvconcat (n:=n) (m:=m)) tt (x, (y, tt))
	= (tt, N.lor (N.shiftl (N.land x (N.ones (N.of_nat n))) (N.of_nat m))
	(N.land y (N.ones (N.of_nat (n + m))))).

Might be hard to read here because it's in terms of bitwise operations, but N.land x (N.ones n) is exactly the same as x mod 2 ^ n; both input bit-vectors are truncated to the expected size. You can easily rewrite this as the identity if you can prove in your context that x < 2 ^ n.