System V: RDI points to `extent` mapped bytes; RSI is that extent. The
caller chooses the format by embedding one of these two routine images.
Every four-byte word is checked, including both halves of a BF16 pair.
Zero or unaligned extents and a wrapping end address fail closed. The
caller must prove the mapped span belongs to its typed staging region.
109def nativeFiniteWordsAssembly =
110 (lambda unrestricted half : Nat .
111 (finiteEmit (constructor X86NativeInstruction X86NativeTestRegister64 finiteRSI finiteRSI)
112 (finiteBranch (constructor X86NativeCondition X86NativeConditionZero) b"reject"
113 (finiteMove finiteRAX finiteRSI
114 (finiteAnd finiteRAX 3
115 (finiteBranch (constructor X86NativeCondition X86NativeConditionNotZero) b"reject"
116 (finiteMove finiteR8 finiteRDI
117 (finiteEmit (constructor X86NativeInstruction X86NativeAddRegister64 finiteRSI finiteR8)
118 (finiteEmit (constructor X86NativeInstruction X86NativeCompareRegister64 finiteRDI finiteR8)
119 (finiteBranch (constructor X86NativeCondition X86NativeConditionBelow) b"reject"
120 (finiteLabel b"scan"
121 (finiteEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64
122 finiteRAX finiteRDI (x86NativeDisplacement32FromNatural 0))
123 (finiteWordCheck half
124 (finiteEmit (constructor X86NativeInstruction X86NativeAddImmediate64 finiteRDI
125 (x86NativeImmediate32FromNatural 4))
126 (finiteEmit (constructor X86NativeInstruction X86NativeCompareRegister64 finiteR8 finiteRDI)
127 (finiteBranch (constructor X86NativeCondition X86NativeConditionZero) b"accept"
128 (finiteJump b"scan"
129 (finiteLabel b"accept"
130 (finiteEmit (constructor X86NativeInstruction X86NativeClear32 finiteRAX)
131 (finiteEmit (constructor X86NativeInstruction X86NativeReturn)
132 (finiteLabel b"reject"
133 (finiteEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 finiteRAX
134 (x86NativeImmediate32FromNatural 1))
135 (finiteEmit (constructor X86NativeInstruction X86NativeReturn)
136 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.