		Search-engine friendly clone of the ACL2 documentation.

Definterface-hmac-infop

Information about a definterface-hmac interface, recorded as a pair's value in the definterface-hmac table.

(definterface-hmac-infop x) is a std::defaggregate of the following fields.

key-size-limit — The limit on the key size in bytes, equal to the :input-size-limit input, divided by 8, of the definterface-hash referenced by the definterface-hmac.
Invariant (maybe-posp key-size-limit).
block-size — The :block-size input.
Invariant (maybe-posp block-size).
output-size — The size of the output in bytes, equal to the :output-size input, divided by 8, of the definterface-hash referenced by the definterface-hmac.
Invariant (posp output-size).

Source link: definterface-hmac-infop

The name of the interface is the key of the pair in the table.

Definterface-hmac-info: Raw constructor for definterface-hmac-infop structures.
Make-definterface-hmac-info: Constructor macro for definterface-hmac-infop structures.
Change-definterface-hmac-info: A copying macro that lets you create new definterface-hmac-infop structures, based on existing structures.
Make-honsed-definterface-hmac-info: Constructor macro for honsed definterface-hmac-infop structures.
Honsed-definterface-hmac-info: Raw constructor for honsed definterface-hmac-infop structures.
Definterface-hmac-info->output-size: Access the output-size field of a definterface-hmac-infop structure.
Definterface-hmac-info->key-size-limit: Access the key-size-limit field of a definterface-hmac-infop structure.
Definterface-hmac-info->block-size: Access the block-size field of a definterface-hmac-infop structure.