Binary semantics forms a critical infrastructure for proving the correctness of Just-In-Time (JIT) compilation, an advanced technique to optimize runtime execution by translating the source bytecode of a program into target machine code. This paper presents a formal model of x86-64 binary semantics in Isabelle/HOL, as the foundation to verify the eBPF x86-64 JIT correctness for the Solana blockchain. First, we formalize a significant subset of x86-64 semantics, covering all the x86-64 instructions used in the Solana JIT. Second, we develop an encoder and decoder to establish a precise bidirectional mapping between assembly and binary code. Furthermore, we demonstrate the equivalence property of the x86-64 encoder-decoder pair, significantly simplifying the correctness proof of the Solana JIT compiler verification.