feat(#231): wire the wsc.facts value-range SOURCE (constants, masks, booleans)

[avrabe]

v1.3.0 shipped the wsc.facts emitter and said plainly in the release notes
that "the fact source that would populate it at volume is not yet wired".
module.facts was only ever filled by a test injector, so the section shipped
empty in practice. This wires the source.

Fact sources wired, and why each is sound

Every derivation is a property of the value's term shape alone — never of
the program point, local/memory state, or a path condition. That is precisely
what makes value-keying sound: a structural range holds at every occurrence of
the term, so a fact can never be stale for the value it names.

#	Source	Justification
1	Constants — i32.const c / i64.const c → [c, c]	The value is c. Derived from the FINAL body, so a value the folder rewrote to i32.const 5 reports [5,5] at the operator the encoder actually emits.
2	Masks — x & K for a non-negative constant K → [0, K]	The set bits of x & K are a subset of K's, so 0 <= (x & K) <= K for any x, with no assumption about x at all. K >= 0 also clears the result's sign bit, so the signed and unsigned readings coincide. This is the shape that makes a downstream bounds check elidable.
3	Booleans — relops and eqz → [0, 1]	The WebAssembly integer comparisons return i32 0/1 by definition.

Facts are recorded on the loom Value in an OptimizationEnv via the existing
assume_range (the value-keyed carrier — never an instruction index), then
resolved to the producing operator in the final sequence. The emitter, its
drop rule and the wsc.* trust boundary are untouched.

Operator keying — where a fact source can silently miscompile the consumer

Function::instructions is a nested representation. The encoder flattens
Block/Loop/If bodies (Block → block + body + end) and an
Instruction::End in the list encodes to no operator at all. So an
instructions index equals the emitted operator ordinal only while every
preceding entry encodes 1:1.

The walk therefore models a whitelist of operators that each encode to exactly
one operator, and stops at the first instruction outside it — all
structured control flow included. Facts are produced only for the straight-line
prefix, where index == ordinal holds by construction.

That claim is tested, not asserted in a comment:

• every_modeled_instruction_encodes_one_to_one encodes a body per modeled
  operator and asserts the decoded operator count is instructions.len() + 1
  (the appended function end). If a future encoder change makes a modeled
  operator emit zero or two operators, this fails.
• Every other test re-decodes the emitted binary and asserts the operator at
  value_id is the one the fact claims.

Renumbering safety is structural rather than a repair: collection runs on the
final module immediately before the encode that consumes it (both the serial
and the islands encode sites), so a fact never outlives a pass.

Tests

Nine new tests in facts::wsc_facts_source_tests:

Test	Asserts
mask_yields_zero_to_mask_range_fact	x & 0xFF → [0,255] reaches wsc.facts, keyed to the i32.and, with the schema-v1 bytes present
constant_folded_value_yields_point_range_fact	a value the folder rewrote to i32.const 5 carries [5,5] at the FOLDED index (0), not the pre-fold index (2)
unjustifiable_values_yield_no_fact	soundness guard — an unconstrained local, a sum of unknowns, a mask whose sign bit is free, a negative constant and a shift by an unknown amount all produce no fact
walk_stops_at_structured_control_flow	a mask inside a block yields nothing; only the straight-line prefix produces facts
value_deleted_by_a_later_pass_is_dropped_not_miskeyed	after DCE deletes a fact-bearing value, its fact is gone and survivors are re-keyed to post-pass indices
every_modeled_instruction_encodes_one_to_one	the 1:1 ordinal claim, locked against the encoder
facts_use_the_full_function_index_and_bool_range	imports-first function indexing, plus the boolean source
fact_collection_is_deterministic	same module → identical Vec<ModuleFact> (REQ-14)
no_derivable_fact_means_no_section	a module with no derivable fact encodes byte-identically

cargo test --release -p loom-core --features verification --lib →
490 passed, 0 failed, 2 ignored (baseline 481; +9, none lost). The ten
existing wsc_facts_* tests are untouched and green.

Measured on this tree

On the calculator component's unbundled core module (2.3 MB, 352 functions):
322 facts — 314 point facts on literal constants, 6 mask ranges, 2
booleans. Stated honestly: the consumer-useful yield is the 8 non-literal ones;
a consumer already knows what i32.const 5 is by decoding it. Suppressing point
facts on operators the consumer reads directly (keeping them only where folding
produced them) is a sensible follow-up, but the two cases are not
distinguishable post-hoc today.

Spot-checked against ground truth (wasm-tools print), function 234:

0: local.get 0
1: i32.const -8     <- negative: correctly NO fact
2: local.get 0
3: i32.sub
4: i32.const 15     <- [15,15]
5: i32.and          <- [0,15]   emitted fact: func=234 value_id=5

Facts-off byte identity: the branch binary's default output is cmp-clean
against a binary built from origin/main on four inputs, including that
2.3 MB module (153243 bytes out).

Deliberately not done — stated so it is not implied

• Negative ranges are dropped, not emitted. The consumer's reading of a
  negative bound for a value it may treat as unsigned is not pinned down by the
  wire format visible from this repo; FactSet::unsigned_max already applies
  exactly this conservatism internally. Facts we cannot state unambiguously are
  not stated.
• The Carry Verus value-range/no-alias facts as IR premises + algebraic mid-end — feed synth's beat-LLVM specialization #240 premise map is not harvested. assume_max / assume_range have
  no non-test callers — the optimizer derives no bound of its own today, so
  there is nothing to record. Harvesting an always-empty map would be theatre.
  This was one of the three candidate sources in the brief; it is dropped with
  evidence rather than faked.
• No arithmetic propagation ((x&0xff) + (y&0xff) etc.). True over the
  integers; wasm arithmetic wraps, and a sound version needs a per-operator
  overflow argument.
• No nested-body coverage. Keying a fact inside a block requires the
  flattened ordinal, which would mean changing the shipped emitter's bound
  check and agreeing the convention with the consumer — not verifiable from this
  repo. This is the single largest coverage limit and the obvious next step.
• No zero-extending-load facts (load8_u → [0,255], etc.). Airtight, but
  it widens the modeled operator set; left out to keep this change auditable.
• The component pipeline and the WAT path emit no facts. --facts on a
  component now prints a warning instead of looking like it worked.

Rivet

TEST-WSC-FACTS-SOURCE added to safety/requirements/verification.yaml
(verifies REQ-1, REQ-4, REQ-5, REQ-12, REQ-14). Its steps[].run names the
eight real test functions, so rivet check verification-evidence resolves them
— it flags the same 5 pre-existing artifacts as on main and not this one.
rivet validate → PASS (42 warnings), identical to the baseline.

Refs #231, #303

[avrabe]

Reviewed. The engineering is solid — value-keyed carriers reused rather than reinvented, drop rule untouched, byte-identity checked with cmp against a main-built binary rather than asserted, and the 48-arm encoder audit locked behind a live test (every_modeled_instruction_encodes_one_to_one). The End-encodes-to-zero-operators finding is exactly the kind of thing that silently mis-keys a fact, and catching it before shipping is the whole point of the value-keyed design.

Two things to change or decide before merge.

1. Don't emit point-ranges for literal constants

Your own measurement makes the case: 322 facts on the calculator core, of which 314 are point/literal and 8 are useful. A consumer reading i32.const 5 already knows the range is [5,5] — the fact carries no information it cannot derive by looking at the operator it is keyed to.

That would be harmless if the section were free, but it isn't: this pipeline's neighbouring issue (#303) is about shrinking artefacts for parts measured in kilobytes, and we would be adding a custom section that is ~97% redundant. A fact channel whose payload is dominated by restatements of literals is also harder to reason about — the interesting facts are buried.

Proposal: suppress the point-range when the value's producing operator is itself a literal constant in the emitted stream. Keep it when the range is a derived point (a value proven constant that is not spelled as a constant). Expected effect on your own numbers: 322 → 8, all of them load-bearing.

If you disagree — e.g. the consumer's ingestion is simpler when every value it might reference is present — say so and we keep them, but then the section-size cost should be measured and stated rather than incidental.

2. Prefix-only coverage is the real limit, and it should be visible

You identified this correctly as the binding constraint: the walk stops at the first structured control-flow instruction, so only the straight-line prefix of a function is covered. On real code that is a small fraction, and the 8 useful facts on a 352-function module are consistent with that.

I am fine shipping prefix-only — soundness first, and extending to nested bodies needs the flattened ordinal plus consumer agreement, which is a bigger change. But the limitation must not be discoverable only by reading the source. Please state it in the module docs of facts.rs in the same terms you used in the report, so the next person does not read "wsc.facts value-range source" and assume whole-function coverage.

Accepted as-is

• Dropping negative ranges — right call at the boundary until the unsigned reading is pinned down.
• Leaving zero-extending-load facts out to keep the modeled set auditable — agreed; a small auditable set beats a large plausible one.
• --facts on a component now warning instead of silently no-op'ing — good; a silent no-op is the failure mode this repo keeps finding.

Separately: your source-#3 finding is its own bug

assume_max/assume_range have no non-test callers

I verified this independently and it holds — every call site is inside a test module. That means #240's "proof-carrying IR premises" half is inert: the hook exists, is tested, and nothing in the optimizer produces a premise through it. That is the fourth instance of this exact shape in the codebase (a trap gate with no callers, a pin held only by a comment, a proof that never ran). It is not yours to fix in this PR — filing it separately — but it is the reason source #3 was empty, and it is worth knowing that the emptiness was a defect rather than a design choice.