Executable binary32 transcendental approximations.
The functions in this file provide deterministic exp, log, and related operations for the
IEEE32 executable model. Stronger libm-style correctness claims live outside this layer.
fixedScale as an Int.
Instances For
Fixed-point encoding of $1$ at scale fixedScale (that is, $2^{\mathtt{fixedScale}}$).
Instances For
Integer power of two: $\mathtt{pow2Int}(k)=2^k$, represented as an Int.
Instances For
Round an integer quotient $\mathtt{num}/\mathtt{den}$ to the nearest integer, ties-to-even.
Assumes $\mathtt{den}>0$.
Instances For
Divide by $2^{\mathtt{shift}}$, rounding to nearest with ties-to-even.
Instances For
Shift by a power of two: multiply when $k\ge 0$, divide when $k<0$.
Division uses ties-to-even rounding.
Instances For
Fixed-point multiplication at scale fixedScale (ties-to-even).
Instances For
Fixed-point division at scale fixedScale (ties-to-even).
If a and b are fixed-point at scale fixedScale, the result is at the same scale.
Instances For
Divide by a natural number, rounding to nearest with ties-to-even.
Instances For
Convert a dyadic number to a signed fixed-point integer at scale fixedScale.
Instances For
Convert a signed fixed-point integer at scale fixedScale to a dyadic number.
Instances For
Fixed-point approximation to $\log 2$ at scale fixedScale.
Instances For
Fixed-point approximation to $1/\log 2$ at scale fixedScale.
Instances For
Fixed-point Taylor coefficients (highest degree first) for $2^x$ on $[-\tfrac12,\tfrac12]$.
Instances For
Evaluate the fixed-point $2^x$ polynomial approximation using Horner’s method.
Instances For
Deterministic tanh without host Float delegation.
For $|x|\le\tfrac14$, the degree-nine Taylor polynomial
$$ \frac{x\left(2835-945x^2+378x^4-153x^6+62x^8\right)}{2835} $$
is evaluated as one exact dyadic rational and rounded only at the end. This avoids cancellation and
preserves every tiny binary32 input, including the minimum subnormal. Larger finite inputs use the
bounded identity 1 - 2/(exp(2|x|)+1). The outer branch is clamped to the shared boundary value
because the two independently rounded approximations can otherwise reverse adjacent outputs at the
switch.
Instances For
Deterministic sin/cos #
Unlike exp/log, sin and cos are used by the runtime FFT layer (NN.Runtime.*.Fft) to build
twiddle factors. Delegating to the host Float implementation makes results platform-dependent.
We implement sin/cos purely inside Lean:
- reduce the exact binary32 input by a 256-bit fixed-point approximation of
pi/2, obtaining a quadrant and a remainder in approximately[-pi/4, pi/4], - approximate the sine and cosine of that remainder by exact Taylor partial sums (degree 13 / 12),
- restore the quadrant using exact sign changes and swaps.
This is deterministic and uses only the IEEE32Exec kernel ops (roundRatToIEEE32, add/mul/sub,
etc.). We do not claim correctly-rounded libm behavior; reproducible execution is the contract.
Instances For
Dyadic 1.
Instances For
Round the exact rational $d/\mathtt{den}$ to binary32, where $d$ is the exact dyadic $\mathtt{mant}\,2^{\mathtt{exp}}$.
We package the dyadic exponent into a rational numerator/denominator and call roundRatToIEEE32.
Instances For
Taylor partial sums on |y| < 1/2 #
We encode the partial sums using a common factorial denominator so the coefficients are exact integers, not approximations.
For $z=y^2$:
$\displaystyle \sin y=\sum_{i=0}^{6}\frac{(-1)^i y^{2i+1}}{(2i+1)!}+R_7(y)$, where the polynomial part can be written as $\displaystyle \frac{y}{13!}\sum_{i=0}^{6}(-1)^i\frac{13!}{(2i+1)!}z^i$.
$\displaystyle \cos y=\sum_{i=0}^{6}\frac{(-1)^i y^{2i}}{(2i)!}+R'_7(y)$, whose polynomial part is $\displaystyle \frac1{12!}\sum_{i=0}^{6}(-1)^i\frac{12!}{(2i)!}z^i$.
Instances For
Precision used for trigonometric argument reduction. It exceeds the binary32 exponent range.
Instances For
reductionScale as an integer.
Instances For
$\operatorname{round}((\pi/2)2^{256})$, used for deterministic Payne–Hanek-style quadrant reduction.
Instances For
Exact conversion of any binary32 dyadic to the trigonometric fixed-point scale.
Instances For
Convert a signed trigonometric fixed-point remainder back to a dyadic.
Instances For
Reduce an exact finite binary32 dyadic to one quadrant and evaluate the small-angle kernels.
Instances For
Public sin / cos #
We expose sin/cos as executable ops on IEEE32Exec using the deterministic implementation
above, together with standard IEEE special-case conventions.
Deterministic sin for IEEE32Exec.
Instances For
Deterministic cos for IEEE32Exec.