module Runtime.NativeWordDigest import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Runtime.WordDigest import Std.Natural -- Shared x86-64 instruction selection for block hashing and its consumers. def digestImm32 = x86NativeImmediate32FromNatural def digestDisp = x86NativeDisplacement32FromNatural def digestImm8 = (lambda unrestricted n : Nat . (constructor X86NativeImmediate8 X86NativeImmediate8Value (nat-to-byte n))) def digestRAX = (constructor X86NativeRegister64 X86NativeRAX) def digestRBX = (constructor X86NativeRegister64 X86NativeRBX) def digestRCX = (constructor X86NativeRegister64 X86NativeRCX) def digestRDX = (constructor X86NativeRegister64 X86NativeRDX) def digestRSI = (constructor X86NativeRegister64 X86NativeRSI) def digestRDI = (constructor X86NativeRegister64 X86NativeRDI) def digestRBP = (constructor X86NativeRegister64 X86NativeRBP) def digestR8 = (constructor X86NativeRegister64 X86NativeR8) def digestR9 = (constructor X86NativeRegister64 X86NativeR9) def digestR10 = (constructor X86NativeRegister64 X86NativeR10) def digestR11 = (constructor X86NativeRegister64 X86NativeR11) def digestR12 = (constructor X86NativeRegister64 X86NativeR12) def digestR13 = (constructor X86NativeRegister64 X86NativeR13) def digestR14 = (constructor X86NativeRegister64 X86NativeR14) def digestR15 = (constructor X86NativeRegister64 X86NativeR15) def digestEmit = (lambda unrestricted instruction : (family X86NativeInstruction) . (lambda unrestricted rest : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyEmit instruction rest))) def digestLoad32 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (digestEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 d base (digestDisp at)))))) def digestLoad64 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (digestEmit (constructor X86NativeInstruction X86NativeLoadMemory64 d base (digestDisp at)))))) def digestLoad8 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (digestEmit (constructor X86NativeInstruction X86NativeLoadMemory8ZeroExtend64 d base (digestDisp at)))))) def digestStore32 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeStoreMemory32 base (digestDisp at) s))))) def digestStore64 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeStoreMemory64 base (digestDisp at) s))))) def digestStore8 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeStoreMemory8 base (digestDisp at) s))))) def digestMov = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeMoveRegister64 s d)))) def digestAdd = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeAddRegister64 s d)))) def digestAnd = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeAndRegister64 s d)))) def digestOr = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeOrRegister64 s d)))) def digestXor = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeXorRegister64 s d)))) def digestShl = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeShiftLeftImmediate64 d (digestImm8 n))))) def digestShr = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeShiftRightImmediate64 d (digestImm8 n))))) def digestMovImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 d (digestImm32 n))))) def digestAddImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeAddImmediate64 d (digestImm32 n))))) def digestAndImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeAndImmediate64 d (digestImm32 n))))) def digestCmpImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 d (digestImm32 n))))) def digestMulImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (digestEmit (constructor X86NativeInstruction X86NativeMultiplyImmediate64 d (digestImm32 n))))) def digestLabel = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyLabel name rest))) def digestJumpIf = (lambda unrestricted condition : (family X86NativeCondition) . (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name rest)))) def digestReturn = (lambda unrestricted rest : (family X86NativeAssembly) . (digestEmit (constructor X86NativeInstruction X86NativeReturn) rest)) def digestEnd : (family X86NativeAssembly) = (constructor X86NativeAssembly X86NativeAssemblyEnd) def digestBackendJump = (lambda unrestricted condition : (family WordDigestCondition) . (eliminate WordDigestCondition (lambda unrestricted current : (family WordDigestCondition) . (pi unrestricted name : Bytes . (pi unrestricted rest : (family X86NativeAssembly) . (family X86NativeAssembly)))) condition (branch WordDigestBelow . (digestJumpIf (constructor X86NativeCondition X86NativeConditionBelow))) (branch WordDigestNotZero . (digestJumpIf (constructor X86NativeCondition X86NativeConditionNotZero))) (branch WordDigestZero . (digestJumpIf (constructor X86NativeCondition X86NativeConditionZero))) (branch WordDigestNegative . (digestJumpIf (constructor X86NativeCondition X86NativeConditionSign))))) def digestX86Backend : (family WordDigestBackend (family X86NativeAssembly) (family X86NativeRegister64)) = (constructor WordDigestBackend WordDigestBackendValue (family X86NativeAssembly) (family X86NativeRegister64) digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestBackendJump digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15) def nativeWordDigestAssembly = (wordDigestAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) digestX86Backend) def nativeWordDigestRoutine = (compiler-native-encode (family X86NativeAssembly) nativeWordDigestAssembly) -- Hash a runtime-length byte string in an admitted writable buffer. RDI is -- the input followed by two writable SHA blocks; RSI is a u32 byte count; -- RDX and R9 retain the block routine's output and work-area arguments. Only -- the suffix is changed. Two blocks cover the longest SHA padding, including -- the length word. This entry point admits Linux user pointers, rejects error -- pointers and oversized lengths before touching memory, and returns zero on -- refusal. Allocation, extent and disjointness remain the caller's contract. -- Padding uses caller-saved R10: RBX belongs to the native host result-slot -- table and must reach the block routine unchanged so its save/restore works. -- The compression equations have one owner in WordDigest; this adds padding, -- never a second hash implementation or a dependency on kernel crypto policy. def nativeByteDigestPaddingBytes : Nat = byteDigestPaddingBytes def nativeByteDigestPaddingAssembly = (wordDigestBytePaddingFor (family X86NativeAssembly) (family X86NativeRegister64) digestX86Backend digestRSI nativeWordDigestAssembly) -- The initial jump skips the refusal return. Both paths share one typed -- assembly, so label resolution still belongs to the compiler's encoder. def nativeByteDigestRoutine = (compiler-native-encode (family X86NativeAssembly) (constructor X86NativeAssembly X86NativeAssemblyJump b"byte-digest-entry" (digestLabel b"byte-digest-refused" (digestMovImm digestRAX 0 (digestReturn (digestLabel b"byte-digest-entry" nativeByteDigestPaddingAssembly)))))) -- Streaming preserves the same caller-save boundary as the one-shot routine. def nativeWordDigestContinueRoutine = (compiler-native-encode (family X86NativeAssembly) (wordDigestContinueAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) digestX86Backend)) def nativeByteDigestStreamStartRoutine = (compiler-native-encode (family X86NativeAssembly) (wordDigestStreamStartFor (family X86NativeAssembly) (family X86NativeRegister64) digestX86Backend)) def nativeByteDigestStreamFinishRoutine = (compiler-native-encode (family X86NativeAssembly) (constructor X86NativeAssembly X86NativeAssemblyJump b"byte-digest-entry" (digestLabel b"byte-digest-refused" (digestMovImm digestRAX 0 (digestReturn (digestLabel b"byte-digest-entry" (wordDigestStreamFinishFor (family X86NativeAssembly) (family X86NativeRegister64) digestX86Backend)))))))