From 8c35b5219fcad64eae7cb2745603e6cb994158a2 Mon Sep 17 00:00:00 2001 From: ScottMoore0 <121321607+ScottMoore0@users.noreply.github.com> Date: Fri, 16 Oct 2026 21:58:40 +0100 Subject: [PATCH] test(base): pin the native U32, Nat and Bool ops to Base's defs U32's arithmetic, bitwise, shift and comparison ops, Nat's ops and U32.to_nat run as native C and JS (comp.ts OPERATIONS). Each new test's main prints a list of calls at edge values (0, 1, 2^31-1, 2^31, 2^32-1, shifts past 31), and its model def proves by {==} that the same calls equal the printed values in Base's defs. So the test gate checks every lane against the values and --verdict checks the values against the model: a native that drifts from its def fails its lane. Co-Authored-By: Claude Opus 5.5 --- tests/base/nat_native_model.bend | 149 ++++++++++ tests/base/u32_native_compare.bend | 99 +++++++ tests/base/u32_native_model.bend | 427 +++++++++++++++++++++++++++++ 3 files changed, 675 insertions(+) create mode 100644 tests/base/nat_native_model.bend create mode 100644 tests/base/u32_native_compare.bend create mode 100644 tests/base/u32_native_model.bend diff --git a/tests/base/nat_native_model.bend b/tests/base/nat_native_model.bend new file mode 100644 index 000000000..fd590b787 --- /dev/null +++ b/tests/base/nat_native_model.bend @@ -0,0 +1,149 @@ +# Nat's ops and U32.to_nat run as native C and JS (comp.ts +# OPERATIONS), not as Base's defs. +# model proves by {==} that the calls equal these values in Base's defs, +# so --verdict pins the model; main prints the same calls, so every lane +# must print what the model computes. The values are each lane's answers. +import Base + +def calls() -> List: + [ + Nat.add(0n, 0n), + Nat.add(0n, 7n), + Nat.add(7n, 0n), + Nat.add(3n, 10n), + Nat.add(10n, 3n), + Nat.add(31n, 64n), + Nat.add(100n, 7n), + Nat.add(64n, 64n), + Nat.sub(0n, 0n), + Nat.sub(0n, 7n), + Nat.sub(7n, 0n), + Nat.sub(3n, 10n), + Nat.sub(10n, 3n), + Nat.sub(31n, 64n), + Nat.sub(100n, 7n), + Nat.sub(64n, 64n), + Nat.mul(0n, 0n), + Nat.mul(0n, 7n), + Nat.mul(7n, 0n), + Nat.mul(3n, 10n), + Nat.mul(10n, 3n), + Nat.mul(31n, 64n), + Nat.mul(100n, 7n), + Nat.mul(64n, 64n), + Nat.div(0n, 0n), + Nat.div(0n, 7n), + Nat.div(7n, 0n), + Nat.div(3n, 10n), + Nat.div(10n, 3n), + Nat.div(31n, 64n), + Nat.div(100n, 7n), + Nat.div(64n, 64n), + Nat.mod(0n, 0n), + Nat.mod(0n, 7n), + Nat.mod(7n, 0n), + Nat.mod(3n, 10n), + Nat.mod(10n, 3n), + Nat.mod(31n, 64n), + Nat.mod(100n, 7n), + Nat.mod(64n, 64n), + Nat.min(0n, 0n), + Nat.min(0n, 7n), + Nat.min(7n, 0n), + Nat.min(3n, 10n), + Nat.min(10n, 3n), + Nat.min(31n, 64n), + Nat.min(100n, 7n), + Nat.min(64n, 64n), + Nat.max(0n, 0n), + Nat.max(0n, 7n), + Nat.max(7n, 0n), + Nat.max(3n, 10n), + Nat.max(10n, 3n), + Nat.max(31n, 64n), + Nat.max(100n, 7n), + Nat.max(64n, 64n), + Nat.double(0n), + Nat.double(7n), + Nat.double(100n), + Nat.pow(0n, 0n), + Nat.pow(2n, 5n), + Nat.pow(3n, 3n), + U32.to_nat(0), + U32.to_nat(255), + U32.to_nat(1000) + ] + +def model() -> {calls() == [ + 0n, + 7n, + 7n, + 13n, + 13n, + 95n, + 107n, + 128n, + 0n, + 0n, + 7n, + 0n, + 7n, + 0n, + 93n, + 0n, + 0n, + 0n, + 0n, + 30n, + 30n, + 1984n, + 700n, + 4096n, + 0n, + 0n, + 0n, + 0n, + 3n, + 0n, + 14n, + 1n, + 0n, + 0n, + 7n, + 3n, + 1n, + 31n, + 2n, + 0n, + 0n, + 0n, + 0n, + 3n, + 3n, + 31n, + 7n, + 64n, + 0n, + 7n, + 7n, + 10n, + 10n, + 64n, + 100n, + 64n, + 0n, + 14n, + 200n, + 1n, + 32n, + 27n, + 0n, + 255n, + 1000n + ] : List}: + {==} + +def main() -> List: + calls() + +#|[0n, 7n, 7n, 13n, 13n, 95n, 107n, 128n, 0n, 0n, 7n, 0n, 7n, 0n, 93n, 0n, 0n, 0n, 0n, 30n, 30n, 1984n, 700n, 4096n, 0n, 0n, 0n, 0n, 3n, 0n, 14n, 1n, 0n, 0n, 7n, 3n, 1n, 31n, 2n, 0n, 0n, 0n, 0n, 3n, 3n, 31n, 7n, 64n, 0n, 7n, 7n, 10n, 10n, 64n, 100n, 64n, 0n, 14n, 200n, 1n, 32n, 27n, 0n, 255n, 1000n] diff --git a/tests/base/u32_native_compare.bend b/tests/base/u32_native_compare.bend new file mode 100644 index 000000000..de3e2ef0c --- /dev/null +++ b/tests/base/u32_native_compare.bend @@ -0,0 +1,99 @@ +# U32's comparisons run as native C and JS (comp.ts OPERATIONS), +# not as Base's defs. +# model proves by {==} that the calls equal these values in Base's defs, +# so --verdict pins the model; main prints the same calls, so every lane +# must print what the model computes. The values are each lane's answers. +import Base + +def calls() -> List: + [ + U32.is_eq(0, 0), + U32.is_eq(0, 4294967295), + U32.is_eq(4294967295, 0), + U32.is_eq(2147483648, 2147483647), + U32.is_eq(2147483647, 2147483648), + U32.is_eq(4294967295, 4294967295), + U32.is_ne(0, 0), + U32.is_ne(0, 4294967295), + U32.is_ne(4294967295, 0), + U32.is_ne(2147483648, 2147483647), + U32.is_ne(2147483647, 2147483648), + U32.is_ne(4294967295, 4294967295), + U32.is_lt(0, 0), + U32.is_lt(0, 4294967295), + U32.is_lt(4294967295, 0), + U32.is_lt(2147483648, 2147483647), + U32.is_lt(2147483647, 2147483648), + U32.is_lt(4294967295, 4294967295), + U32.is_le(0, 0), + U32.is_le(0, 4294967295), + U32.is_le(4294967295, 0), + U32.is_le(2147483648, 2147483647), + U32.is_le(2147483647, 2147483648), + U32.is_le(4294967295, 4294967295), + U32.is_gt(0, 0), + U32.is_gt(0, 4294967295), + U32.is_gt(4294967295, 0), + U32.is_gt(2147483648, 2147483647), + U32.is_gt(2147483647, 2147483648), + U32.is_gt(4294967295, 4294967295), + U32.is_ge(0, 0), + U32.is_ge(0, 4294967295), + U32.is_ge(4294967295, 0), + U32.is_ge(2147483648, 2147483647), + U32.is_ge(2147483647, 2147483648), + U32.is_ge(4294967295, 4294967295), + U32.is_zero(0), + U32.is_zero(1), + U32.is_zero(2147483648), + U32.is_zero(4294967295) + ] + +def model() -> {calls() == [ + True{}, + False{}, + False{}, + False{}, + False{}, + True{}, + False{}, + True{}, + True{}, + True{}, + True{}, + False{}, + False{}, + True{}, + False{}, + False{}, + True{}, + False{}, + True{}, + True{}, + False{}, + False{}, + True{}, + True{}, + False{}, + False{}, + True{}, + True{}, + False{}, + False{}, + True{}, + False{}, + True{}, + True{}, + False{}, + True{}, + True{}, + False{}, + False{}, + False{} + ] : List}: + {==} + +def main() -> List: + calls() + +#|[True{}, False{}, False{}, False{}, False{}, True{}, False{}, True{}, True{}, True{}, True{}, False{}, False{}, True{}, False{}, False{}, True{}, False{}, True{}, True{}, False{}, False{}, True{}, True{}, False{}, False{}, True{}, True{}, False{}, False{}, True{}, False{}, True{}, True{}, False{}, True{}, True{}, False{}, False{}, False{}] diff --git a/tests/base/u32_native_model.bend b/tests/base/u32_native_model.bend new file mode 100644 index 000000000..4f0a64912 --- /dev/null +++ b/tests/base/u32_native_model.bend @@ -0,0 +1,427 @@ +# U32's arithmetic, bitwise and shift ops run as native C and JS +# (comp.ts OPERATIONS), not as Base's defs. +# model proves by {==} that the calls equal these values in Base's defs, +# so --verdict pins the model; main prints the same calls, so every lane +# must print what the model computes. The values are each lane's answers. +import Base + +def calls() -> List: + [ + U32.add(0, 0), + U32.add(0, 4294967295), + U32.add(1, 4294967295), + U32.add(4294967295, 4294967295), + U32.add(2147483648, 2147483648), + U32.add(4294967295, 2), + U32.add(65535, 65535), + U32.add(2147483647, 2), + U32.add(3, 4294967294), + U32.add(255, 32), + U32.add(4294967294, 3), + U32.add(2, 31), + U32.sub(0, 0), + U32.sub(0, 4294967295), + U32.sub(1, 4294967295), + U32.sub(4294967295, 4294967295), + U32.sub(2147483648, 2147483648), + U32.sub(4294967295, 2), + U32.sub(65535, 65535), + U32.sub(2147483647, 2), + U32.sub(3, 4294967294), + U32.sub(255, 32), + U32.sub(4294967294, 3), + U32.sub(2, 31), + U32.mul(0, 0), + U32.mul(0, 4294967295), + U32.mul(1, 4294967295), + U32.mul(4294967295, 4294967295), + U32.mul(2147483648, 2147483648), + U32.mul(4294967295, 2), + U32.mul(65535, 65535), + U32.mul(2147483647, 2), + U32.mul(3, 4294967294), + U32.mul(255, 32), + U32.mul(4294967294, 3), + U32.mul(2, 31), + U32.div(0, 0), + U32.div(0, 4294967295), + U32.div(1, 4294967295), + U32.div(4294967295, 4294967295), + U32.div(2147483648, 2147483648), + U32.div(4294967295, 2), + U32.div(65535, 65535), + U32.div(2147483647, 2), + U32.div(3, 4294967294), + U32.div(255, 32), + U32.div(4294967294, 3), + U32.div(2, 31), + U32.mod(0, 0), + U32.mod(0, 4294967295), + U32.mod(1, 4294967295), + U32.mod(4294967295, 4294967295), + U32.mod(2147483648, 2147483648), + U32.mod(4294967295, 2), + U32.mod(65535, 65535), + U32.mod(2147483647, 2), + U32.mod(3, 4294967294), + U32.mod(255, 32), + U32.mod(4294967294, 3), + U32.mod(2, 31), + U32.and(0, 0), + U32.and(0, 4294967295), + U32.and(1, 4294967295), + U32.and(4294967295, 4294967295), + U32.and(2147483648, 2147483648), + U32.and(4294967295, 2), + U32.and(65535, 65535), + U32.and(2147483647, 2), + U32.and(3, 4294967294), + U32.and(255, 32), + U32.and(4294967294, 3), + U32.and(2, 31), + U32.or(0, 0), + U32.or(0, 4294967295), + U32.or(1, 4294967295), + U32.or(4294967295, 4294967295), + U32.or(2147483648, 2147483648), + U32.or(4294967295, 2), + U32.or(65535, 65535), + U32.or(2147483647, 2), + U32.or(3, 4294967294), + U32.or(255, 32), + U32.or(4294967294, 3), + U32.or(2, 31), + U32.xor(0, 0), + U32.xor(0, 4294967295), + U32.xor(1, 4294967295), + U32.xor(4294967295, 4294967295), + U32.xor(2147483648, 2147483648), + U32.xor(4294967295, 2), + U32.xor(65535, 65535), + U32.xor(2147483647, 2), + U32.xor(3, 4294967294), + U32.xor(255, 32), + U32.xor(4294967294, 3), + U32.xor(2, 31), + U32.min(0, 0), + U32.min(0, 4294967295), + U32.min(1, 4294967295), + U32.min(4294967295, 4294967295), + U32.min(2147483648, 2147483648), + U32.min(4294967295, 2), + U32.min(65535, 65535), + U32.min(2147483647, 2), + U32.min(3, 4294967294), + U32.min(255, 32), + U32.min(4294967294, 3), + U32.min(2, 31), + U32.max(0, 0), + U32.max(0, 4294967295), + U32.max(1, 4294967295), + U32.max(4294967295, 4294967295), + U32.max(2147483648, 2147483648), + U32.max(4294967295, 2), + U32.max(65535, 65535), + U32.max(2147483647, 2), + U32.max(3, 4294967294), + U32.max(255, 32), + U32.max(4294967294, 3), + U32.max(2, 31), + U32.inc(0), + U32.inc(1), + U32.inc(2147483647), + U32.inc(2147483648), + U32.inc(2147483649), + U32.inc(4294967294), + U32.inc(4294967295), + U32.inc(123456789), + U32.shl(0), + U32.shl(1), + U32.shl(2147483647), + U32.shl(2147483648), + U32.shl(2147483649), + U32.shl(4294967294), + U32.shl(4294967295), + U32.shl(123456789), + U32.shr(0), + U32.shr(1), + U32.shr(2147483647), + U32.shr(2147483648), + U32.shr(2147483649), + U32.shr(4294967294), + U32.shr(4294967295), + U32.shr(123456789), + U32.not(0), + U32.not(1), + U32.not(2147483647), + U32.not(2147483648), + U32.not(2147483649), + U32.not(4294967294), + U32.not(4294967295), + U32.not(123456789), + U32.shln(1, 0n), + U32.shln(1, 1n), + U32.shln(1, 31n), + U32.shln(1, 32n), + U32.shln(1, 33n), + U32.shln(2147483648, 0n), + U32.shln(2147483648, 1n), + U32.shln(2147483648, 31n), + U32.shln(2147483648, 32n), + U32.shln(2147483648, 33n), + U32.shln(4294967295, 0n), + U32.shln(4294967295, 1n), + U32.shln(4294967295, 31n), + U32.shln(4294967295, 32n), + U32.shln(4294967295, 33n), + U32.shln(3141592653, 0n), + U32.shln(3141592653, 1n), + U32.shln(3141592653, 31n), + U32.shln(3141592653, 32n), + U32.shln(3141592653, 33n), + U32.shrn(1, 0n), + U32.shrn(1, 1n), + U32.shrn(1, 31n), + U32.shrn(1, 32n), + U32.shrn(1, 33n), + U32.shrn(2147483648, 0n), + U32.shrn(2147483648, 1n), + U32.shrn(2147483648, 31n), + U32.shrn(2147483648, 32n), + U32.shrn(2147483648, 33n), + U32.shrn(4294967295, 0n), + U32.shrn(4294967295, 1n), + U32.shrn(4294967295, 31n), + U32.shrn(4294967295, 32n), + U32.shrn(4294967295, 33n), + U32.shrn(3141592653, 0n), + U32.shrn(3141592653, 1n), + U32.shrn(3141592653, 31n), + U32.shrn(3141592653, 32n), + U32.shrn(3141592653, 33n), + U32.pow(0, 0n), + U32.pow(2, 31n), + U32.pow(2, 32n), + U32.pow(3, 33n), + U32.pow(7, 16n), + U32.pow(65535, 2n), + U32.pow(4294967295, 2n), + U32.pow(4294967295, 3n), + U32.from_nat(0n), + U32.from_nat(1n), + U32.from_nat(255n), + U32.from_nat(256n) + ] + +def model() -> {calls() == [ + 0, + 4294967295, + 0, + 4294967294, + 0, + 1, + 131070, + 2147483649, + 1, + 287, + 1, + 33, + 0, + 1, + 2, + 0, + 0, + 4294967293, + 0, + 2147483645, + 5, + 223, + 4294967291, + 4294967267, + 0, + 0, + 4294967295, + 1, + 0, + 4294967294, + 4294836225, + 4294967294, + 4294967290, + 8160, + 4294967290, + 62, + 0, + 0, + 0, + 1, + 1, + 2147483647, + 1, + 1073741823, + 0, + 7, + 1431655764, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 1, + 3, + 31, + 2, + 2, + 0, + 0, + 1, + 4294967295, + 2147483648, + 2, + 65535, + 2, + 2, + 32, + 2, + 2, + 0, + 4294967295, + 4294967295, + 4294967295, + 2147483648, + 4294967295, + 65535, + 2147483647, + 4294967295, + 255, + 4294967295, + 31, + 0, + 4294967295, + 4294967294, + 0, + 0, + 4294967293, + 0, + 2147483645, + 4294967293, + 223, + 4294967293, + 29, + 0, + 0, + 1, + 4294967295, + 2147483648, + 2, + 65535, + 2, + 3, + 32, + 3, + 2, + 0, + 4294967295, + 4294967295, + 4294967295, + 2147483648, + 4294967295, + 65535, + 2147483647, + 4294967294, + 255, + 4294967294, + 31, + 1, + 2, + 2147483648, + 2147483649, + 2147483650, + 4294967295, + 0, + 123456790, + 0, + 2, + 4294967294, + 0, + 2, + 4294967292, + 4294967294, + 246913578, + 0, + 0, + 1073741823, + 1073741824, + 1073741824, + 2147483647, + 2147483647, + 61728394, + 4294967295, + 4294967294, + 2147483648, + 2147483647, + 2147483646, + 1, + 0, + 4171510506, + 1, + 2, + 2147483648, + 0, + 0, + 2147483648, + 0, + 0, + 0, + 0, + 4294967295, + 4294967294, + 2147483648, + 0, + 0, + 3141592653, + 1988218010, + 2147483648, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 2147483648, + 1073741824, + 1, + 0, + 0, + 4294967295, + 2147483647, + 1, + 0, + 0, + 3141592653, + 1570796326, + 1, + 0, + 0, + 1, + 2147483648, + 0, + 2790964099, + 2768600449, + 4294836225, + 1, + 4294967295, + 0, + 1, + 255, + 256 + ] : List}: + {==} + +def main() -> List: + calls() + +#|[0, 4294967295, 0, 4294967294, 0, 1, 131070, 2147483649, 1, 287, 1, 33, 0, 1, 2, 0, 0, 4294967293, 0, 2147483645, 5, 223, 4294967291, 4294967267, 0, 0, 4294967295, 1, 0, 4294967294, 4294836225, 4294967294, 4294967290, 8160, 4294967290, 62, 0, 0, 0, 1, 1, 2147483647, 1, 1073741823, 0, 7, 1431655764, 0, 0, 0, 1, 0, 0, 1, 0, 1, 3, 31, 2, 2, 0, 0, 1, 4294967295, 2147483648, 2, 65535, 2, 2, 32, 2, 2, 0, 4294967295, 4294967295, 4294967295, 2147483648, 4294967295, 65535, 2147483647, 4294967295, 255, 4294967295, 31, 0, 4294967295, 4294967294, 0, 0, 4294967293, 0, 2147483645, 4294967293, 223, 4294967293, 29, 0, 0, 1, 4294967295, 2147483648, 2, 65535, 2, 3, 32, 3, 2, 0, 4294967295, 4294967295, 4294967295, 2147483648, 4294967295, 65535, 2147483647, 4294967294, 255, 4294967294, 31, 1, 2, 2147483648, 2147483649, 2147483650, 4294967295, 0, 123456790, 0, 2, 4294967294, 0, 2, 4294967292, 4294967294, 246913578, 0, 0, 1073741823, 1073741824, 1073741824, 2147483647, 2147483647, 61728394, 4294967295, 4294967294, 2147483648, 2147483647, 2147483646, 1, 0, 4171510506, 1, 2, 2147483648, 0, 0, 2147483648, 0, 0, 0, 0, 4294967295, 4294967294, 2147483648, 0, 0, 3141592653, 1988218010, 2147483648, 0, 0, 1, 0, 0, 0, 0, 2147483648, 1073741824, 1, 0, 0, 4294967295, 2147483647, 1, 0, 0, 3141592653, 1570796326, 1, 0, 0, 1, 2147483648, 0, 2790964099, 2768600449, 4294836225, 1, 4294967295, 0, 1, 255, 256]