• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Pfcs
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
    • Bitcoin
    • Des
    • Ethereum
      • Mmp-trees
      • Semaphore
      • Database
      • Cryptography
      • Rlp
        • Rlp-tree
        • Rlp-decoding-executable
          • Rlp-error
          • Rlp-parse-tree
          • Rlp-decodex-tree
          • Maybe-rlp-error
          • Rlp-decodex-bytes
          • Rlp-decodex-scalar
        • Rlp-decodability
        • Rlp-encoding
        • Rlp-decoding-declarative
        • Rlp-big-endian-representations
      • Transactions
      • Hex-prefix
      • Basics
      • Addresses
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Rlp-decoding-executable

Rlp-decodex-scalar

Executable RLP decoding of a scalar.

Signature

(rlp-decodex-scalar encoding) → (mv error? scalar)

Arguments

encoding — Guard (byte-listp encoding).

Returns

error? — Type (maybe-rlp-error-p error?).

scalar — Type (natp scalar).

This has the same form as the alternative definition rule of rlp-decode-scalar in terms of rlp-decode-bytes. As such, it is immediate to prove equal (i.e. correct with respect) to rlp-decode-scalar, using the correctness theorem of rlp-decodex-bytes.

Definitions and Theorems

Function: rlp-decodex-scalar

(defun rlp-decodex-scalar (encoding)
  (declare (xargs :guard (byte-listp encoding)))
  (let ((__function__ 'rlp-decodex-scalar))
    (declare (ignorable __function__))
    (b* (((mv error? bytes)
          (rlp-decodex-bytes encoding))
         ((when error?) (mv error? 0))
         ((unless (equal (trim-bendian* bytes) bytes))
          (mv (rlp-error-leading-zeros-in-scalar bytes)
              0))
         (scalar (bebytes=>nat bytes)))
      (mv nil scalar))))

Theorem: maybe-rlp-error-p-of-rlp-decodex-scalar.error?

(defthm maybe-rlp-error-p-of-rlp-decodex-scalar.error?
  (b* (((mv ?error? ?scalar)
        (rlp-decodex-scalar encoding)))
    (maybe-rlp-error-p error?))
  :rule-classes :rewrite)

Theorem: natp-of-rlp-decodex-scalar.scalar

(defthm natp-of-rlp-decodex-scalar.scalar
  (b* (((mv ?error? ?scalar)
        (rlp-decodex-scalar encoding)))
    (natp scalar))
  :rule-classes :rewrite)

Theorem: rlp-decode-scalar-is-rlp-decodex-scalar

(defthm rlp-decode-scalar-is-rlp-decodex-scalar
  (and (iff (mv-nth 0 (rlp-decode-scalar encoding))
            (mv-nth 0 (rlp-decodex-scalar encoding)))
       (equal (mv-nth 1 (rlp-decode-scalar encoding))
              (mv-nth 1 (rlp-decodex-scalar encoding)))))

Theorem: rlp-decodex-scalar-of-byte-list-fix-encoding

(defthm rlp-decodex-scalar-of-byte-list-fix-encoding
  (equal (rlp-decodex-scalar (byte-list-fix encoding))
         (rlp-decodex-scalar encoding)))

Theorem: rlp-decodex-scalar-byte-list-equiv-congruence-on-encoding

(defthm rlp-decodex-scalar-byte-list-equiv-congruence-on-encoding
  (implies (byte-list-equiv encoding encoding-equiv)
           (equal (rlp-decodex-scalar encoding)
                  (rlp-decodex-scalar encoding-equiv)))
  :rule-classes :congruence)