// The cross-architecture determinism probe battery.
//
// Every line this program prints is a byte the platform is allowed no opinion
// about. x86-64 and AArch64 disagree natively on all of it: the two CPUs
// generate different NaN bit patterns, they trap where wasm masks, and they
// saturate differently on out-of-range float->int conversions. Wax pins one
// answer for each, so the same battery run on both must produce the same text.
//
// Two assertions ride on the output and neither substitutes for the other. The
// checked-in expectation file pins the VALUE, which one architecture alone can
// prove. Comparing two architectures' artifacts pins EQUALITY, which no single
// machine can. A battery that only agreed with itself would pass while both
// legs sat on a non-canonical answer.
//
// Nothing here may be constant-foldable, or the probe measures the compiler's
// host rather than the target's hardware. Every operand comes out of a static
// array filled by `SeedProbeState`, whose `salt` parameter is zero but arrives
// as an api-export argument -- a value no optimizer can see through, because
// the export is callable from outside the module at any time. The literal-
// operand cases are covered too, deliberately and separately, under the
// `nan.const.*` names: those exercise the const folders instead, and the
// contract requires the two families to land on the same value.

import Debug from Wax;
import Span from Wax;
import StringBuilder from Wax;
import HashBytes64 from Wax::Hash;
import WriteLE from Wax::BitConverter;
import Math from Wax;

// Operand storage for every probe that must reach real hardware. Static rather
// than local: escape analysis promotes a local array back into registers and
// folds the arithmetic to a literal, which measured the build machine instead
// of the target.
static class ProbeState {
    public static float[] f32 = new float[4];
    public static double[] f64 = new double[4];
    public static int32[] i32 = new int32[6];
    public static int64[] i64 = new int64[6];
    public static float[] f32Store = new float[4];
    public static double[] f64Store = new double[4];
    public static float32x4[] v4 = new float32x4[1];
    public static float32x4[] v4Sqrt = new float32x4[1];
    public static float[] f32Mixed = new float[8];
    public static double[] f64Mixed = new double[8];
    public static float[] f32Edge = new float[5];
    public static double[] f64Edge = new double[5];
}

fn Hex(uint64 value, int32 digits) : string {
    StringBuilder builder = new StringBuilder();
    builder.AppendUInt64Hex(value, digits, true);
    return builder.ToString();
}

// Raw little-endian byte rendering of a heap region. This is the observation
// the store canonicalization exists for: snapshot hashing, the debugger's
// object-body memcmp, and host array marshaling all read these same bytes, and
// none of them can be reached from a stdlib-level fixup.
fn HexBytes(Span<uint8> bytes) : string {
    StringBuilder builder = new StringBuilder();
    for (int32 i = 0; i < bytes.length; i++) {
        builder.AppendUInt64Hex(bytes[i] as uint64, 2, true);
    }
    return builder.ToString();
}

fn Emit(string name, string value) : void {
    Debug.Log("WAXDET ${name} ${value}");
}

fn EmitU32(string name, uint32 value) : void {
    Emit(name, Hex(value as uint64, 8));
}

fn EmitU64(string name, uint64 value) : void {
    Emit(name, Hex(value, 16));
}

fn EmitI32(string name, int32 value) : void {
    Emit(name, Hex((value as uint32) as uint64, 8));
}

fn EmitI64(string name, int64 value) : void {
    Emit(name, Hex(value as uint64, 16));
}

// Fills every opaque operand. `salt` is always zero, but it arrives as an
// api-export parameter, so the constant folders cannot reach through it and the
// arithmetic below stays on the target's FPU.
api fn SeedProbeState(int32 salt) : int32 {
    float zeroF = salt as float;
    ProbeState.f32[0] = zeroF;
    ProbeState.f32[1] = 1.0f / zeroF;
    ProbeState.f32[2] = (salt - 1) as float;
    ProbeState.f32[3] = (salt + 1) as float;

    double zeroD = salt as double;
    ProbeState.f64[0] = zeroD;
    ProbeState.f64[1] = 1.0 / zeroD;
    ProbeState.f64[2] = (salt - 1) as double;
    ProbeState.f64[3] = (salt + 1) as double;

    ProbeState.i32[0] = int32.MinValue + salt;
    ProbeState.i32[1] = salt - 1;
    ProbeState.i32[2] = salt;
    ProbeState.i32[3] = salt + 1;
    ProbeState.i32[4] = salt + 33;
    ProbeState.i32[5] = salt + 32;

    ProbeState.i64[0] = int64.MinValue + (salt as int64);
    ProbeState.i64[1] = (salt as int64) - 1L;
    ProbeState.i64[2] = salt as int64;
    ProbeState.i64[3] = (salt as int64) + 1L;
    ProbeState.i64[4] = (salt as int64) + 65L;
    ProbeState.i64[5] = (salt as int64) + 64L;

    // The stored family: each slot receives a NaN from a different generator,
    // so a fixup that covered division but not the invalid-multiply case would
    // show up as one wrong quad rather than a uniformly wrong file.
    ProbeState.f32Store[0] = ProbeState.f32[0] / ProbeState.f32[0];
    ProbeState.f32Store[1] = ProbeState.f32[1] - ProbeState.f32[1];
    ProbeState.f32Store[2] = ProbeState.f32[1] * ProbeState.f32[0];
    ProbeState.f32Store[3] = Math.Sqrt(ProbeState.f32[2]);

    ProbeState.f64Store[0] = ProbeState.f64[0] / ProbeState.f64[0];
    ProbeState.f64Store[1] = ProbeState.f64[1] - ProbeState.f64[1];
    ProbeState.f64Store[2] = ProbeState.f64[1] * ProbeState.f64[0];
    ProbeState.f64Store[3] = Math.Sqrt(ProbeState.f64[2]);

    // The NaN has to be generated BY a vector op, not inserted into a vector
    // after a scalar op produced it: an inserted NaN is already canonical, so
    // the probe would keep reading right even if lane-wise canonicalization
    // regressed entirely. Dividing (0, 1, 1, 1) by itself puts a vector-born NaN
    // in lane 0 and leaves three finite lanes, which a whole-vector splat would
    // not distinguish from a scalar fixup applied to all four.
    float32x4 quotient = new float32x4(ProbeState.f32[0], ProbeState.f32[3], ProbeState.f32[3], ProbeState.f32[3]);
    ProbeState.v4[0] = quotient / quotient;
    // The sqrt companion is the probe that caught the optimized C tier storing
    // 0xFFC00000 lanes: a host compiler may swap one NaN for another, so the
    // canonical result of a negative sqrt has to be constructed, and this row
    // is the release gate on that construction. The lanes are chosen to pin
    // the neighbors too -- finite results bit-exact, and sqrt(-0) keeping its
    // sign -- beside the canonical NaN lane.
    ProbeState.v4Sqrt[0] = new float32x4(ProbeState.f32[2], ProbeState.f32[3], -ProbeState.f32[0], ProbeState.f32[3] + ProbeState.f32[3] + ProbeState.f32[3] + ProbeState.f32[3]).Sqrt();

    // The digest inputs mix NaN with values whose bits are fully specified, so a
    // hash change localizes: if only the NaN slots moved the specified slots
    // still match their own probes above.
    ProbeState.f32Mixed[0] = ProbeState.f32[0] / ProbeState.f32[0];
    ProbeState.f32Mixed[1] = ProbeState.f32[1];
    ProbeState.f32Mixed[2] = -ProbeState.f32[1];
    ProbeState.f32Mixed[3] = ProbeState.f32[0];
    ProbeState.f32Mixed[4] = -ProbeState.f32[0];
    ProbeState.f32Mixed[5] = ProbeState.f32[3];
    ProbeState.f32Mixed[6] = -ProbeState.f32[3];
    ProbeState.f32Mixed[7] = Math.Sqrt(ProbeState.f32[2]);

    ProbeState.f64Mixed[0] = ProbeState.f64[0] / ProbeState.f64[0];
    ProbeState.f64Mixed[1] = ProbeState.f64[1];
    ProbeState.f64Mixed[2] = -ProbeState.f64[1];
    ProbeState.f64Mixed[3] = ProbeState.f64[0];
    ProbeState.f64Mixed[4] = -ProbeState.f64[0];
    ProbeState.f64Mixed[5] = ProbeState.f64[3];
    ProbeState.f64Mixed[6] = -ProbeState.f64[3];
    ProbeState.f64Mixed[7] = Math.Sqrt(ProbeState.f64[2]);

    ProbeState.f32Edge[0] = (0x00000001u + (salt as uint32)).Reinterpret<float>();
    ProbeState.f32Edge[1] = (0x00000003u + (salt as uint32)).Reinterpret<float>();
    ProbeState.f32Edge[2] = (0x007FFFFFu + (salt as uint32)).Reinterpret<float>();
    ProbeState.f32Edge[3] = (0x00800000u + (salt as uint32)).Reinterpret<float>();
    ProbeState.f32Edge[4] = (0x80000001u + (salt as uint32)).Reinterpret<float>();

    ProbeState.f64Edge[0] = (0x0000000000000001ul + (salt as uint64)).Reinterpret<double>();
    ProbeState.f64Edge[1] = (0x0000000000000003ul + (salt as uint64)).Reinterpret<double>();
    ProbeState.f64Edge[2] = (0x000FFFFFFFFFFFFFul + (salt as uint64)).Reinterpret<double>();
    ProbeState.f64Edge[3] = (0x0010000000000000ul + (salt as uint64)).Reinterpret<double>();
    ProbeState.f64Edge[4] = (0x8000000000000001ul + (salt as uint64)).Reinterpret<double>();
    return 0;
}

// NaN generation, literal operands. These reach the const folders rather than
// the hardware, and the contract requires them to agree with the opaque family
// below.
fn EmitConstNanProbes() : void {
    float f32Zero = 0.0f / 0.0f;
    EmitU32("nan.const.f32.divzero", f32Zero.Reinterpret<uint32>());
    float f32Inf = float.Infinity;
    EmitU32("nan.const.f32.infsub", (f32Inf - f32Inf).Reinterpret<uint32>());
    EmitU32("nan.const.f32.infmul", (f32Inf * 0.0f).Reinterpret<uint32>());
    EmitU32("nan.const.f32.sqrtneg", Math.Sqrt(-1.0f).Reinterpret<uint32>());

    double f64Zero = 0.0 / 0.0;
    EmitU64("nan.const.f64.divzero", f64Zero.Reinterpret<uint64>());
    double f64Inf = double.Infinity;
    EmitU64("nan.const.f64.infsub", (f64Inf - f64Inf).Reinterpret<uint64>());
    EmitU64("nan.const.f64.infmul", (f64Inf * 0.0).Reinterpret<uint64>());
    EmitU64("nan.const.f64.sqrtneg", Math.Sqrt(-1.0).Reinterpret<uint64>());
}

// NaN generation, opaque operands. These are the ones that reach the FPU on
// every tier, so they are the ones that diverge by architecture rather than by
// optimization level.
fn EmitOpaqueNanProbes() : void {
    EmitU32("nan.opaque.f32.divzero", (ProbeState.f32[0] / ProbeState.f32[0]).Reinterpret<uint32>());
    EmitU32("nan.opaque.f32.infsub", (ProbeState.f32[1] - ProbeState.f32[1]).Reinterpret<uint32>());
    EmitU32("nan.opaque.f32.infmul", (ProbeState.f32[1] * ProbeState.f32[0]).Reinterpret<uint32>());
    EmitU32("nan.opaque.f32.sqrtneg", Math.Sqrt(ProbeState.f32[2]).Reinterpret<uint32>());

    EmitU64("nan.opaque.f64.divzero", (ProbeState.f64[0] / ProbeState.f64[0]).Reinterpret<uint64>());
    EmitU64("nan.opaque.f64.infsub", (ProbeState.f64[1] - ProbeState.f64[1]).Reinterpret<uint64>());
    EmitU64("nan.opaque.f64.infmul", (ProbeState.f64[1] * ProbeState.f64[0]).Reinterpret<uint64>());
    EmitU64("nan.opaque.f64.sqrtneg", Math.Sqrt(ProbeState.f64[2]).Reinterpret<uint64>());

    // Width conversion preserves NaN-ness but not payload width, so promotion
    // and demotion are their own observation: a f32 NaN widened to f64 has to
    // land on the f64 canonical pattern, not on a zero-extended f32 one.
    float narrowNan = ProbeState.f32[0] / ProbeState.f32[0];
    double wideNan = ProbeState.f64[0] / ProbeState.f64[0];
    EmitU64("nan.opaque.promote.f32.to.f64", (narrowNan as double).Reinterpret<uint64>());
    EmitU32("nan.opaque.demote.f64.to.f32", (wideNan as float).Reinterpret<uint32>());
}

// Raw heap bytes, the observer class no stdlib-level fixup can reach.
fn EmitStoredNanProbes() : void {
    Emit("nan.store.f32.bytes", HexBytes(ProbeState.f32Store.ToSpan().AsBytes()));
    Emit("nan.store.f64.bytes", HexBytes(ProbeState.f64Store.ToSpan().AsBytes()));
    Emit("nan.store.v4.div.bytes", HexBytes(ProbeState.v4.ToSpan().AsBytes()));
    Emit("nan.store.v4.sqrt.bytes", HexBytes(ProbeState.v4Sqrt.ToSpan().AsBytes()));

    uint8[] scratch = new uint8[8];
    Span<uint8> scratchSpan = scratch.ToSpan();
    WriteLE<float>(scratchSpan, 0, ProbeState.f32Store[0]);
    Emit("nan.bitconv.f32", HexBytes(scratchSpan.Slice(0, 4)));
    WriteLE<double>(scratchSpan, 0, ProbeState.f64Store[0]);
    Emit("nan.bitconv.f64", HexBytes(scratchSpan));

    // The mixed arrays go out twice, as bytes and as a hash of the same bytes,
    // and both forms earn their place. The bytes localize a failure to a slot --
    // negative zero is in there, and a negation lowered as `0 - x` instead of a
    // sign-bit flip would move exactly one quad. The hash is the observation
    // class the snapshot machinery actually performs (a u64 over raw heap
    // bytes), and having it beside the bytes is what distinguishes "the heap
    // changed" from "the hash function changed": if the bytes still match and
    // only the digest moved, the stdlib hash was edited, not determinism.
    Emit("bytes.f32.mixed", HexBytes(ProbeState.f32Mixed.ToSpan().AsBytes()));
    Emit("bytes.f64.mixed", HexBytes(ProbeState.f64Mixed.ToSpan().AsBytes()));
    EmitU64("digest.f32.mixed", HashBytes64(ProbeState.f32Mixed.ToSpan().AsBytes()));
    EmitU64("digest.f64.mixed", HashBytes64(ProbeState.f64Mixed.ToSpan().AsBytes()));
}

// Shift counts at and past the operand width, plus negative counts. x86 masks
// to 5/6 bits, AArch64's variable shifts do not, and wasm mandates the mask --
// so an unguarded shift is a genuine three-way split, not a theoretical one.
fn EmitShiftProbes() : void {
    EmitI32("shift.i32.shl.by32", ProbeState.i32[3] << ProbeState.i32[5]);
    EmitI32("shift.i32.shl.by33", ProbeState.i32[3] << ProbeState.i32[4]);
    EmitI32("shift.i32.shl.byneg1", ProbeState.i32[3] << ProbeState.i32[1]);
    EmitI32("shift.i32.sar.by33", ProbeState.i32[0] >> ProbeState.i32[4]);
    EmitI32("shift.i32.sar.byneg1", ProbeState.i32[0] >> ProbeState.i32[1]);
    EmitU32("shift.u32.shr.by33", (ProbeState.i32[0] as uint32) >> (ProbeState.i32[4] as uint32));

    EmitI64("shift.i64.shl.by64", ProbeState.i64[3] << ProbeState.i64[5]);
    EmitI64("shift.i64.shl.by65", ProbeState.i64[3] << ProbeState.i64[4]);
    EmitI64("shift.i64.shl.byneg1", ProbeState.i64[3] << ProbeState.i64[1]);
    EmitI64("shift.i64.sar.by65", ProbeState.i64[0] >> ProbeState.i64[4]);
    EmitI64("shift.i64.sar.byneg1", ProbeState.i64[0] >> ProbeState.i64[1]);
    EmitU64("shift.u64.shr.by65", (ProbeState.i64[0] as uint64) >> (ProbeState.i64[4] as uint64));
}

// Out-of-range and NaN float->int conversions. Hardware answers differ (x86
// returns the "integer indefinite" pattern, AArch64 saturates), so the language
// pins one; these probes are what proves the guard is present on both.
fn EmitConversionProbes() : void {
    float big32 = ProbeState.f32[1];
    float nan32 = ProbeState.f32[0] / ProbeState.f32[0];
    float negBig32 = -ProbeState.f32[1];
    EmitI32("conv.f32.i32.posinf", big32 as int32);
    EmitI32("conv.f32.i32.neginf", negBig32 as int32);
    EmitI32("conv.f32.i32.nan", nan32 as int32);
    EmitU32("conv.f32.u32.posinf", big32 as uint32);
    EmitU32("conv.f32.u32.neginf", negBig32 as uint32);
    EmitU32("conv.f32.u32.nan", nan32 as uint32);

    double big64 = ProbeState.f64[1];
    double nan64 = ProbeState.f64[0] / ProbeState.f64[0];
    double negBig64 = -ProbeState.f64[1];
    EmitI64("conv.f64.i64.posinf", big64 as int64);
    EmitI64("conv.f64.i64.neginf", negBig64 as int64);
    EmitI64("conv.f64.i64.nan", nan64 as int64);
    EmitU64("conv.f64.u64.posinf", big64 as uint64);
    EmitU64("conv.f64.u64.neginf", negBig64 as uint64);
    EmitU64("conv.f64.u64.nan", nan64 as uint64);
    EmitI32("conv.f64.i32.posinf", big64 as int32);
    EmitI32("conv.f64.i32.neginf", negBig64 as int32);
    EmitI32("conv.f64.i32.nan", nan64 as int32);
    EmitU32("conv.f64.u32.posinf", big64 as uint32);
    EmitU32("conv.f64.u32.neginf", negBig64 as uint32);
    EmitU32("conv.f64.u32.nan", nan64 as uint32);

    // The exact boundary, which infinity does not reach: 2147483648.0f is the
    // first float above int32's maximum, and it is exactly representable. A
    // clamp written with the wrong comparison passes every infinity probe above
    // and fails only here.
    float justPastMax = (ProbeState.i32[3] as float) * 2147483648.0f;
    EmitI32("conv.f32.i32.maxplus1", justPastMax as int32);
    EmitU32("conv.f32.u32.maxplus1", (justPastMax * 2.0f) as uint32);
}

// Exact-bit gradual-underflow boundaries. These operands are populated by the
// externally callable seed export, so optimized native code must execute the
// arithmetic rather than answering from the compiler host's constant folder.
// The half-minimum rows also pin ties-to-even and the sign of an underflowed
// zero; the max-plus-min rows pin the carry from subnormal to normal.
fn EmitSubnormalProbes() : void {
    EmitU32("subnormal.f32.min.times.half", (ProbeState.f32Edge[0] * 0.5f).Reinterpret<uint32>());
    EmitU32("subnormal.f32.three-min.times.half", (ProbeState.f32Edge[1] * 0.5f).Reinterpret<uint32>());
    EmitU32("subnormal.f32.max.plus.min", (ProbeState.f32Edge[2] + ProbeState.f32Edge[0]).Reinterpret<uint32>());
    EmitU32("subnormal.f32.normal.minus.min", (ProbeState.f32Edge[3] - ProbeState.f32Edge[0]).Reinterpret<uint32>());
    EmitU32("subnormal.f32.normal.times.half", (ProbeState.f32Edge[3] * 0.5f).Reinterpret<uint32>());
    EmitU32("subnormal.f32.negative-min.times.half", (ProbeState.f32Edge[4] * 0.5f).Reinterpret<uint32>());

    EmitU64("subnormal.f64.min.times.half", (ProbeState.f64Edge[0] * 0.5).Reinterpret<uint64>());
    EmitU64("subnormal.f64.three-min.times.half", (ProbeState.f64Edge[1] * 0.5).Reinterpret<uint64>());
    EmitU64("subnormal.f64.max.plus.min", (ProbeState.f64Edge[2] + ProbeState.f64Edge[0]).Reinterpret<uint64>());
    EmitU64("subnormal.f64.normal.minus.min", (ProbeState.f64Edge[3] - ProbeState.f64Edge[0]).Reinterpret<uint64>());
    EmitU64("subnormal.f64.normal.times.half", (ProbeState.f64Edge[3] * 0.5).Reinterpret<uint64>());
    EmitU64("subnormal.f64.negative-min.times.half", (ProbeState.f64Edge[4] * 0.5).Reinterpret<uint64>());

    EmitU64("subnormal.convert.f32-min.to-f64", (ProbeState.f32Edge[0] as double).Reinterpret<uint64>());
    EmitU32("subnormal.convert.f64-min.to-f32", (ProbeState.f64Edge[0] as float).Reinterpret<uint32>());
    double f32MinimumAsF64 = 0x36A0000000000000ul.Reinterpret<double>() + (ProbeState.f64[0] * ProbeState.f64Edge[0]);
    EmitU32("subnormal.convert.f64-f32-min.to-f32", (f32MinimumAsF64 as float).Reinterpret<uint32>());
}

api fn RunValueProbes() : int32 {
    EmitConstNanProbes();
    EmitOpaqueNanProbes();
    EmitStoredNanProbes();
    EmitShiftProbes();
    EmitConversionProbes();
    EmitSubnormalProbes();
    return 0;
}

// The trapping edges get one export each, because a panic ends the frame: two
// in a row would report only the first. The driver runs each in its own process
// (native) or its own frame (wasm) and records the panic kind, so "it trapped"
// and "it trapped for this reason" are separate assertions.
api fn PanicDivI32MinByNegOne() : int32 {
    return ProbeState.i32[0] / ProbeState.i32[1];
}

api fn PanicDivI64MinByNegOne() : int32 {
    return (ProbeState.i64[0] / ProbeState.i64[1]) as int32;
}

api fn PanicDivI32ByZero() : int32 {
    return ProbeState.i32[3] / ProbeState.i32[2];
}

api fn PanicDivI64ByZero() : int32 {
    return (ProbeState.i64[3] / ProbeState.i64[2]) as int32;
}

api fn PanicRemI32MinByNegOne() : int32 {
    return ProbeState.i32[0] % ProbeState.i32[1];
}

api fn PanicRemI32ByZero() : int32 {
    return ProbeState.i32[3] % ProbeState.i32[2];
}

api fn PanicRemI64MinByNegOne() : int32 {
    return (ProbeState.i64[0] % ProbeState.i64[1]) as int32;
}

api fn PanicRemI64ByZero() : int32 {
    return (ProbeState.i64[3] % ProbeState.i64[2]) as int32;
}

// The native leg is a one-shot executable, so argv selects the probe. Every
// invocation passes exactly one selector, which makes `args.size - 2` a
// reliable zero for the seed regardless of which probe is being run.
api fn Main(string[] args) : int32 {
    if (args.size != 2) {
        Debug.Log("WAXDET-ERROR expected exactly one probe selector");
        return 3;
    }
    SeedProbeState(args.size - 2);
    string selector = args[1];
    if (selector == "values") { return RunValueProbes(); }
    if (selector == "panic.div.i32.min-by-neg1") { return PanicDivI32MinByNegOne(); }
    if (selector == "panic.div.i64.min-by-neg1") { return PanicDivI64MinByNegOne(); }
    if (selector == "panic.div.i32.by-zero") { return PanicDivI32ByZero(); }
    if (selector == "panic.div.i64.by-zero") { return PanicDivI64ByZero(); }
    if (selector == "panic.rem.i32.min-by-neg1") { return PanicRemI32MinByNegOne(); }
    if (selector == "panic.rem.i32.by-zero") { return PanicRemI32ByZero(); }
    if (selector == "panic.rem.i64.min-by-neg1") { return PanicRemI64MinByNegOne(); }
    if (selector == "panic.rem.i64.by-zero") { return PanicRemI64ByZero(); }
    Debug.Log("WAXDET-ERROR unknown probe selector ${selector}");
    return 3;
}