Require source-backed rounding tolerances in generated conservation properties

Split from #405. Closing that analysis issue does not mean this engineering work has shipped.

Problem

Invariant discovery and property fan-in preserve exact operands, units, denominators, and rounding direction, but the invariant implementation stage does not say how those semantics should affect aggregate conservation assertions.

In the R52 Aave v4 suite, catalogHubSpokeAggregates used unconditional equality and reported:

• Hub added assets: 100000100301
• Sum of Spoke added assets: 100000100300

The reference property used a relative-difference check together with a MIN_TOTAL_SUPPLIED floor. The generated one-unit failure is therefore more plausibly rounding dust than a protocol accounting defect, but it still consumes campaign and triage work.

.ultrafuzz/prompts/properties/property-specification-fanin.md already requires preservation of rounding direction and oracle provenance. .ultrafuzz/prompts/strategies/invariants/implement-properties.md preserves false-positive risks but never requires the implementation to derive and apply a justified tolerance.

Expected behavior

When implementing a conservation or aggregate-accounting property, the agent should determine whether the target’s documented arithmetic, constants, formulas, or supplied reference property requires:

• exact equality;
• a source-derived absolute tolerance;
• a source-derived relative tolerance; and/or
• a source-derived minimum-value floor.

Any tolerance must retain the original units, denominator, and comparison direction and cite the target or reference source from which it was derived. Ultrafuzz must not invent a generic ±1, basis-point threshold, epsilon, or floor merely to make an assertion pass.

When no source supports a tolerance, keep the strict assertion or emit an actionable implementation blocker; do not silently weaken it.

Acceptance criteria

• The invariant-property implementation prompt explicitly requires source-backed tolerance analysis for conservation and aggregate-accounting assertions.
• Absolute tolerances, relative tolerances, and minimum-value floors are permitted only when their value or derivation is tied to target code, target documentation, or a supplied reference property.
• Generated tolerance arithmetic preserves operands, units, denominator semantics, comparison direction, and overflow safety.
• The implementation handoff records the selected tolerance expression and its source, or records why strict equality remains appropriate.
• Missing evidence never produces a guessed tolerance or an unconditional broad precondition skip.
• Regression coverage pins these prompt semantics and includes an R52-shaped fixture proving that an allowed dust difference passes while a discrepancy outside the derived bound still fails.
• Existing exact invariants remain exact when their sources require exact equality.

Non-goals

This does not reclassify the historical R52 findings or introduce one global tolerance policy for every target. It addresses generated property semantics only.

Start by reading .ultrafuzz/prompts/property-specification-fanin.md and .ultrafuzz/prompts/strategies/invariants/implement-properties.md, then locate the regression coverage for generated property prompts. Update the implementation guidance to require source-backed tolerance decisions and handoff records. Done means the R52-shaped fixture accepts justified dust, rejects discrepancies outside the derived bound, and leaves exact invariants strict.