a2e11f6ff2
planted/build.py now writes §9.3's probe beside the checker corpus: probe.wasm, whose wai_run loads each case's operands from a data segment at run time, runs the twelve operations of the table and stores each result in order (80 bytes), in a memory of one page whose minimum is its maximum; and probe.txt, each case's operands and the result the deterministic profile prescribes, and the probe's bytes. probe-nan-branch.wasm is the probe with a branch after each operation on whether its result is a NaN, writing the canonical NaN itself. Both checkers hold both at the float level and refuse them R3 at the integer level (cases.txt; tests/module_rules.rs). What the planted copy breaks is F1, a property of the probe on engines that no checker decides; the next commit's host shows the probe holds it and the planted copy fails it. Co-Authored-By: Claude Opus 5.5 <[email protected]>
19 lines
1.3 KiB
Text
19 lines
1.3 KiB
Text
# The probe of waism.md §9.3, written by build.py: `<case> <operation> <operands>
|
|
# <result>`, one line a case, each operand and result as its bits, a vector's lanes
|
|
# comma-joined with lane 0 first, the result the one the deterministic profile
|
|
# prescribes, little-endian hex. Last, `bytes <hex>`: the probe's bytes, the output
|
|
# of its wai_run, every result in order. probe.wasm is the probe; probe-nan-branch.wasm
|
|
# is it with a NaN-dependent branch planted after each operation.
|
|
1 f32.add 0xffa00001 0x3f800000 0000c07f
|
|
2 f32.mul 0xffa00001 0x40000000 0000c07f
|
|
3 f32.div 0x00000000 0x00000000 0000c07f
|
|
4 f32.sub 0x7f800000 0x7f800000 0000c07f
|
|
5 f32.sqrt 0xbf800000 0000c07f
|
|
6 f32.min 0xffa00001 0x3f800000 0000c07f
|
|
7 f32.nearest 0xffa00001 0000c07f
|
|
8 f32.demote_f64 0xfff4000000000001 0000c07f
|
|
9 f64.add 0xfff4000000000001 0x3ff0000000000000 000000000000f87f
|
|
10 f64.promote_f32 0xffa00001 000000000000f87f
|
|
11 f32x4.add 0xffa00001,0x7fa00001,0xffc00000,0x7f800000 0x3f800000,0x3f800000,0x3f800000,0xff800000 0000c07f0000c07f0000c07f0000c07f
|
|
12 f64x2.mul 0xfff4000000000001,0x7ff8000000000001 0x4000000000000000,0x4000000000000000 000000000000f87f000000000000f87f
|
|
bytes 0000c07f0000c07f0000c07f0000c07f0000c07f0000c07f0000c07f0000c07f000000000000f87f000000000000f87f0000c07f0000c07f0000c07f0000c07f000000000000f87f000000000000f87f
|