Introduce an interface for a cryptographic hash function.
A cryptographic hash function takes as input a sequence of bits of arbitrary size or of a size bounded by a large limit, and returns a sequence of bits of a fixed size. Given an endianness convention to covert between bit and byte sequences, the hash function can be also regarded as operating on byte sequences.
This macro introduces weakly constrained ACL2 functions for a cryptographic hash function: one that operates on bits and one that operates on bytes. Both functions have guards that require the input to be bit or byte lists and its length to be bounded (if applicable). The functions are constrained to return bit or byte lists of the appropriate fixed lengths, and also to fix their inputs to bit or byte lists.
This macro also introduces a few theorems that follow from the constraints. It also introduces an XDOC topic for the generated functions, constraints, and theorems.
(definterface-hash name :input-size-limit ... :output-size ... :name-bits ... :name-bytes ... :topic ... :parents ... :short ... :long ... )
A symbol that names the hash function.
One of the following:
- A constant expression whose value is a positive integer multiple of 8. This is the limit of the input size in bits: the size of the input must be strictly less than this limit. This is for hash functions that have a bound on the size of the input.
nil , if the hash function accepts inputs of arbitrary size.
A constant expression whose value is a positive integer multiple of 8. This is the fixed size of the output, in bits.
A symbol that names the generated constrained function that operates on bits.
If not supplied, it defaults to
name followed by-bits .
A symbol that names the generated constrained function that operates on bytes.
If not supplied, it defaults to
name followed by-bytes .
A symbol that names the generated XDOC topic that surrounds the generated functions and theorems.
If not supplied, it defaults to
name followed by-interface .
These, if present, are added to the XDOC topic generated for the fixtype.
A constrained function that operates on bits.
Its guard consists of bit-listp and, if applicable, the limit on the input size specified by
:input-size-limit .The function is constrained to:
The following additional theorems are also generated:
- A type prescription rules saying that the function returns a true-listp.
- A type prescription rule saying that the function returns a consp.
A constrained function that operates on bytes.
Its guard consists of byte-listp and, if applicable, the limit on the input size specified by
:input-size-limit and divided by 8.The function is constrained to:
- Return a byte-listp of the length specified by
:output-size divided by 8.- Fix its input to a byte-listp.
The following additional theorems are also generated:
- A type prescription rules saying that the function returns a true-listp.
- A type prescription rule saying that the function returns a consp.