search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
123 stars 20 forks source link

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

Open fshaked opened 3 years ago

fshaked commented 3 years ago

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 commented 3 years ago

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

https://github.com/project-oak/silveroak/commit/72a0eb76a9b36eec7ae73ef6fd3ef280c6bf90a0

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 commented 2 years ago

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.: https://github.com/project-oak/silveroak/blob/db7486778505bcce4ad7824dfa0d6826efe1cd74/silveroak-opentitan/hmac/hw/Sha256Properties.v#L394-L397

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.