• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
        • R1cs
        • Interfaces
        • Sha-2
        • Keccak
        • Kdf
        • Mimc
        • Padding
        • Hmac
        • Elliptic-curves
        • Attachments
          • Secp256k1-attachment
          • Secp256k1-ecdsa-attachment
          • Pbkdf2-hmac-sha-512-attachment
          • Hmac-sha-512-attachment
          • Sha-256-attachment
          • Keccak-256-attachment
        • Elliptic-curve-digital-signature-algorithm
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Attachments

Pbkdf2-hmac-sha-512-attachment

Executable attachment for the PBKDF2-HMAC-SHA-512 interface.

We define a wrapper of the executable definition and attach the wrapper to the constrained function. The wrapper just serves to use the fixtypes for byte lists, to fix the password and salt input accordingly, and to fix the iterations and length inputs to positive integers.

Definitions and Theorems

Function: pbkdf2-hmac-sha-512-wrapper

(defun pbkdf2-hmac-sha-512-wrapper (password salt iterations length)
  (declare (xargs :guard (and (byte-listp password)
                              (byte-listp salt)
                              (posp iterations)
                              (posp length))))
  (declare (xargs :guard (and (< (len password) (expt 2 125))
                              (< (len salt) (- (expt 2 125) 132))
                              (<= length (* (1- (expt 2 32)) 64)))))
  (let ((__function__ 'pbkdf2-hmac-sha-512-wrapper))
    (declare (ignorable __function__))
    (b* ((password (mbe :logic (byte-list-fix password)
                        :exec password))
         (salt (mbe :logic (byte-list-fix salt)
                    :exec salt))
         (iterations (mbe :logic (pos-fix iterations)
                          :exec iterations))
         (length (mbe :logic (pos-fix length)
                      :exec length)))
      (kdf::pbkdf2-hmac-sha-512 password salt iterations length))))

Theorem: byte-listp-of-pbkdf2-hmac-sha-512-wrapper

(defthm byte-listp-of-pbkdf2-hmac-sha-512-wrapper
 (b*
  ((result
     (pbkdf2-hmac-sha-512-wrapper password salt iterations length)))
  (byte-listp result))
 :rule-classes :rewrite)

Theorem: len-of-pbkdf2-hmac-sha-512-wrapper

(defthm len-of-pbkdf2-hmac-sha-512-wrapper
 (equal
  (len
      (pbkdf2-hmac-sha-512-wrapper password salt iterations length))
  (pos-fix length)))

Theorem: pbkdf2-hmac-sha-512-wrapper-of-byte-list-fix-password

(defthm pbkdf2-hmac-sha-512-wrapper-of-byte-list-fix-password
 (equal
     (pbkdf2-hmac-sha-512-wrapper (byte-list-fix password)
                                  salt iterations length)
     (pbkdf2-hmac-sha-512-wrapper password salt iterations length)))

Theorem: pbkdf2-hmac-sha-512-wrapper-byte-list-equiv-congruence-on-password

(defthm
 pbkdf2-hmac-sha-512-wrapper-byte-list-equiv-congruence-on-password
 (implies
  (byte-list-equiv password password-equiv)
  (equal
       (pbkdf2-hmac-sha-512-wrapper password salt iterations length)
       (pbkdf2-hmac-sha-512-wrapper
            password-equiv salt iterations length)))
 :rule-classes :congruence)

Theorem: pbkdf2-hmac-sha-512-wrapper-of-byte-list-fix-salt

(defthm pbkdf2-hmac-sha-512-wrapper-of-byte-list-fix-salt
 (equal
     (pbkdf2-hmac-sha-512-wrapper password (byte-list-fix salt)
                                  iterations length)
     (pbkdf2-hmac-sha-512-wrapper password salt iterations length)))

Theorem: pbkdf2-hmac-sha-512-wrapper-byte-list-equiv-congruence-on-salt

(defthm
     pbkdf2-hmac-sha-512-wrapper-byte-list-equiv-congruence-on-salt
 (implies
  (byte-list-equiv salt salt-equiv)
  (equal
       (pbkdf2-hmac-sha-512-wrapper password salt iterations length)
       (pbkdf2-hmac-sha-512-wrapper
            password salt-equiv iterations length)))
 :rule-classes :congruence)

Theorem: pbkdf2-hmac-sha-512-wrapper-of-pos-fix-iterations

(defthm pbkdf2-hmac-sha-512-wrapper-of-pos-fix-iterations
 (equal
     (pbkdf2-hmac-sha-512-wrapper password salt (pos-fix iterations)
                                  length)
     (pbkdf2-hmac-sha-512-wrapper password salt iterations length)))

Theorem: pbkdf2-hmac-sha-512-wrapper-pos-equiv-congruence-on-iterations

(defthm
     pbkdf2-hmac-sha-512-wrapper-pos-equiv-congruence-on-iterations
 (implies
  (acl2::pos-equiv iterations iterations-equiv)
  (equal
       (pbkdf2-hmac-sha-512-wrapper password salt iterations length)
       (pbkdf2-hmac-sha-512-wrapper
            password salt iterations-equiv length)))
 :rule-classes :congruence)

Theorem: pbkdf2-hmac-sha-512-wrapper-of-pos-fix-length

(defthm pbkdf2-hmac-sha-512-wrapper-of-pos-fix-length
 (equal
     (pbkdf2-hmac-sha-512-wrapper password
                                  salt iterations (pos-fix length))
     (pbkdf2-hmac-sha-512-wrapper password salt iterations length)))

Theorem: pbkdf2-hmac-sha-512-wrapper-pos-equiv-congruence-on-length

(defthm pbkdf2-hmac-sha-512-wrapper-pos-equiv-congruence-on-length
 (implies
  (acl2::pos-equiv length length-equiv)
  (equal
       (pbkdf2-hmac-sha-512-wrapper password salt iterations length)
       (pbkdf2-hmac-sha-512-wrapper
            password salt iterations length-equiv)))
 :rule-classes :congruence)