4. Module Structure

The codebase is organized into focused modules:

CoqToLeanAsm.Bits — Byte, Word, DWord, OpSize

CoqToLeanAsm.Reg — Reg, ByteReg, SegReg, VReg

CoqToLeanAsm.Instr — Instr, MemSpec, DstSrc, BinOp

CoqToLeanAsm.Mem — Memory, Flags, RegFile, ProcState

CoqToLeanAsm.Encode — encode, encodeInstr

CoqToLeanAsm.SepLogic — SPred, regIs, dwordIs

CoqToLeanAsm.Macros — ifThenElse, X86.while, proc

CoqToLeanAsm.Assembler — assemble, Program, LabelMap