• 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
    • Riscv
      • Semantics
      • Features
      • States
      • Decoding
        • Decode
        • Decoding-of-encoding
        • Get-fields-rtype
        • Get-fields-stype
        • Get-fields-itype
        • Get-fields-btype
        • Encoding-of-decoding
        • Get-imm-jtype
        • Get-imm-btype
        • Get-imm-utype
        • Get-fields-utype
        • Get-imm-stype
        • Get-imm-itype
        • Get-fields-jtype
        • Decoding-as-inverse
          • Encoding-validp
          • Decodei
          • Decodei-is-decode
        • Get-rs2
        • Get-rs1
        • Get-rd
        • Get-opcode
        • Get-funct7
        • Get-funct3
      • Instructions
      • Encoding
      • Reads-over-writes
      • Rv32im
      • Rv64im
      • Execution
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • 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
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Decoding-as-inverse

Encoding-validp

Check if a 32-bit word is a valid instruction encoding.

This is the case when there exists an instruction, valid for the given features, whose encoding is enc. This is a declarative definition.

Definitions and Theorems

Theorem: encoding-validp-suff

(defthm encoding-validp-suff
  (implies (and (instrp instr)
                (instr-validp instr feat)
                (equal (encode instr feat)
                       (ubyte32-fix enc)))
           (encoding-validp enc feat)))

Theorem: booleanp-of-encoding-validp

(defthm booleanp-of-encoding-validp
  (b* ((yes/no (encoding-validp enc feat)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: encoding-validp-of-ubyte32-fix-enc

(defthm encoding-validp-of-ubyte32-fix-enc
  (equal (encoding-validp (ubyte32-fix enc) feat)
         (encoding-validp enc feat)))

Theorem: encoding-validp-ubyte32-equiv-congruence-on-enc

(defthm encoding-validp-ubyte32-equiv-congruence-on-enc
  (implies (acl2::ubyte32-equiv enc enc-equiv)
           (equal (encoding-validp enc feat)
                  (encoding-validp enc-equiv feat)))
  :rule-classes :congruence)

Theorem: encoding-validp-of-feat-fix-feat

(defthm encoding-validp-of-feat-fix-feat
  (equal (encoding-validp enc (feat-fix feat))
         (encoding-validp enc feat)))

Theorem: encoding-validp-feat-equiv-congruence-on-feat

(defthm encoding-validp-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (encoding-validp enc feat)
                  (encoding-validp enc feat-equiv)))
  :rule-classes :congruence)

Theorem: instrp-of-encoding-valid-witness

(defthm instrp-of-encoding-valid-witness
  (implies (encoding-validp enc feat)
           (instrp (encoding-valid-witness enc feat))))

Theorem: instr-validp-of-encoding-valid-witness

(defthm instr-validp-of-encoding-valid-witness
  (implies (encoding-validp enc feat)
           (instr-validp (encoding-valid-witness enc feat)
                         feat)))

Theorem: encode-of-encoding-valid-witness

(defthm encode-of-encoding-valid-witness
  (implies (encoding-validp enc feat)
           (equal (encode (encoding-valid-witness enc feat)
                          feat)
                  (ubyte32-fix enc))))