• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Riscv
        • Semantics
        • Features
        • States
        • Decoding
        • Instructions
        • Encoding
          • Encode
          • Decoding-of-encoding
            • Decode-of-encode-of-instr
            • Get-opcode-of-encode-of-instr
            • Get-funct3-of-encode-of-instr
            • Get-rd-of-encode-of-instr
            • Get-rs1-of-encode-of-instr
            • Get-fields-itype-of-encode-of-instr
            • Get-imm-itype-of-encode-of-instr
            • Get-rs2-of-encode-of-instr
            • Get-fields-rtype-of-encode-of-instr
            • Encode-injective
              • Get-funct7-of-encode-of-instr
              • Get-fields-utype-of-encode-of-instr
              • Decode-of-encode
              • Get-imm-utype-of-encode-of-instr
              • Get-fields-stype-of-encode-of-instr
              • Get-fields-btype-of-encode-of-instr
              • Get-imm-stype-of-encode-of-instr
              • Get-imm-jtype-of-encode-of-instr
              • Get-imm-btype-of-encode-of-instr
              • Get-fields-jtype-of-encode-of-instr
            • Encode-load-funct
            • Encode-store-funct
            • Encode-op-imms-32-funct
            • Encode-op-funct
            • Encode-op-32-funct
            • Encode-op-imms64-funct
            • Encode-op-imms32-funct
            • Encoding-of-decoding
            • Encode-op-imm-funct
            • Encode-op-imm-32-funct
            • Encode-branch-funct
          • 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-of-encoding

    Encode-injective

    Injectivity of encoding.

    Different valid instructions are encoded differently. This is a direct consequence of decode-of-encode: if two different instructions were encoded in the same way, the decoder would be unable to restore both at the same time.

    Definitions and Theorems

    Theorem: encode-injective

    (defthm encode-injective
      (implies (and (instr-validp instr1 feat)
                    (instr-validp instr2 feat))
               (equal (equal (encode instr1 feat)
                             (encode instr2 feat))
                      (equal (instr-fix instr1)
                             (instr-fix instr2)))))