The Formula Was the Same. The Numeric Semantics Were Not.

Two low-precision dot products returned the exact same output bits. Both flagged that precision had been lost during execution.

One was correct. The other violated its contract.

The dot products exercise the engineering infrastructure we are building: how it connects a failing result to the relevant numeric contract and checks the effect of a correction. The product is the technology that makes that investigation possible.

The difference was not the value, nor was it the signal-level interface. It was the numeric contract under which each computation was executed.

A repair that made both computations exact eliminated every target mismatch—and introduced 589 failures in the neighboring operation. A separate discrepancy came from the reference oracle itself: it had discarded the sign of zero.

In quantized formats and mixed-precision arithmetic, a mathematical formula alone does not specify hardware behavior. Precision, accumulation order, rounding mode, and intermediate storage width are parts of the numeric contract.

In our previous case studies, we explored how design meaning can remain connected across spatial transformations in FIFOs and transaction lifetimes across reset. In this experiment, we examine a third dimension of hardware meaning: Can an AI-native engineering stack identify an arithmetic contract violation, pinpoint where information was first lost, and repair the targeted pipeline without corrupting a neighboring operation whose different behavior was intentional?

---

1. Where 4 + 1 − 4 Stops Being 1

To test this boundary, we constructed a minimal three-term dot product whose mathematical sum is trivial:

Mathematical sum: 4 + 1 − 4 = 1

The design specification called for two distinct arithmetic pipelines operating on a restricted floating-point format:

• Target Dot Product (Exact Accumulation Contract): Accumulate the intermediate products without precision loss, then apply a single rounding step at the end. Intended result: 1.
• Neighboring Dot Product (Sequential Accumulation Contract): Accumulate sequentially in the restricted floating-point format, applying nearest-even rounding after each addition. Intended result under sequential rounding: 0.

One rounding boundary, two contracts

Input terms: 4, +1, −4 · same low-precision format

1. 01

   Start at 4

   The first term is represented exactly.

2. 02

   4 + 1 → 5 → rounded to 4

   The intermediate addition loses the contribution of +1. This is the first inexact boundary.

3. 03

   4 − 4 → 0

   Cancellation exposes the information already discarded.

Defective target · exact contract

Expected 1 · observed 0

Intermediate rounding violates this operation’s contract.

Contract violated

Neighbor · sequential contract

Expected 0 · observed 0

The same rounding behavior is intentional here.

Contract satisfied

The Injected Defect

We injected the defect by replacing the Target Dot Product’s exact accumulator with a sequential low-precision accumulator. That implementation remained valid for the neighboring operation, which made the contract essential to diagnosis.

1. Step 1: 4 + 1 = 5. The low-precision intermediate register cannot represent 5 exactly under its configured nearest-even policy. It rounds to 4.
2. Step 2: 4 - 4 = 0. The final output returns 0.

When executed against an independent integer-based reference oracle, the target returned 0 instead of the expected 1.

---

2. Identical Outputs, Opposite Verdicts

Crucially, the Neighboring Dot Product received the exact same inputs (4, +1, -4), used the exact same low-precision format, returned the exact same result (0), and raised the exact same inexact-arithmetic flag.

However, because the neighbor’s contract explicitly permitted sequential rounding, its output of 0 was correct under that contract.

Same bits, opposite verdicts

Observation	Target	Neighbor
Output bits	0x0	0x0
Inexact flag	Set	Set
Required accumulation	Exact	Sequential rounding
Verdict	Reject	Accept

The witness separates observable values from the contract needed to interpret them:

• The output 0 alone does not distinguish the defective target from the valid neighbor.
• The inexact flag alone is not a defect: the neighboring operation permits intermediate rounding.
• Changing both dot products to exact accumulation would violate the neighbor’s sequential-rounding contract, as the repair sweep below shows.

Pinpointing the Point of Divergence

The investigation connected the failing output to its arithmetic pipeline and the relevant numeric contract. In this witness, it localized the first loss of information to the intermediate addition:

• Lane 0 (4): Represented exactly.
• Lane 1 (4 + 1): Intermediate value 5 is not exactly representable in the configured format; first inexact boundary triggered.
• Lane 2 (4 - 4): Evaluates to 0.

---

3. Four Repairs, Only One Respects Both Contracts

We evaluated four candidate repairs against all 4,096 combinations (16 × 16 × 16) of the three 4-bit left-hand input encodings, including signed zeros, with the right-hand terms fixed to one. Each candidate was checked against both the target contract and the neighbor’s contract.

Zero target failures is not enough. Making both dot products exact fixes the target while producing 589 neighbor failures. A valid correction must satisfy both contracts.

Why Partial and Over-Broad Fixes Fail

• Candidate 1 (Widen Downstream): Widening the bit-width after accumulation failed on 589 vectors. Once 5 was rounded down to 4 in the intermediate stage, converting 4 into a wider representation downstream could not recover the discarded contribution.
• Candidate 2 (Make Both Exact): Making both operations exact fixed the target but introduced 589 regressions in the neighboring dot product. Fixing a test by overriding the intentional contract of a neighboring block is a new bug, not a repair.
• Candidate 3 (Global Rounding Modification): Changing the global rounding mode produced 995 target failures and 534 neighbor failures in the sweep.
• Candidate 4 (Local Contract Restoration): Restoring exact accumulation only to the target pipeline produced 0 target failures and 0 neighbor failures across the 4,096 input vectors.

The repaired design passed all 4,096 cases in direct execution and all 4,096 in compiled execution. Independent integer-based oracles supplied the intended results; agreement between execution modes was not treated as the specification.

---

4. Counterfactual Replay: Move the Cancellation

To test order sensitivity in this witness, we reordered the same input terms:

Ordering A: 4 + 1 − 4
Ordering B: 4 − 4 + 1

Sequential low-precision accumulation is order-sensitive in this witness: changing the order changes where rounding occurs. The repaired target returns 1 for both tested orderings. This counterfactual demonstrates the intended behavior for these cases; it is not a general proof of invariance across arbitrary arithmetic designs.

---

5. The Oracle’s Signed-Zero Blind Spot

During the initial validation sweep, an unexpected discrepancy emerged: the repaired hardware design failed a single test vector against the independent reference oracle.

Investigation traced this discrepancy to the reference oracle’s treatment of signed zero. For this vector, the design’s result matched the specified signed-zero behavior; the oracle’s result did not.

The reference model lost a sign

Signed-zero witness · the configured contract requires −0

Repaired design

−0

Preserves the sign required for this vector.

Initial integer-based oracle

+0

Its abstraction discarded the sign of zero.

The failing left-hand vector was [-0, -0, -0]. Under the configured contracts, exact accumulation preserves -0, while the sequential recurrence starts from +0 and returns +0. The initial integer-based oracle discarded the sign of zero. That distinction had to be modeled for both intended computations, rather than normalized away.

We updated the oracle to preserve the signed-zero behavior required by the configured contract, retained the failing trace, and re-ran the suite. This illustrates a verification principle: an oracle is just another piece of software—it must be inspectable, challengeable, and verifiable against explicit mathematical specifications.

---

6. Evidential Integrity and Perturbation Testing

To test whether localization depended on names or positions, we subjected the design to structural perturbations:

1. Renaming & Refactoring: Internal names and source positions were changed.
2. Structural Decoys: A disconnected lookalike sequential dot product was inserted into the design hierarchy.

In the tested perturbations, localization retained the intended arithmetic target and rejected the disconnected decoy. This provides evidence that the investigation followed maintained design relationships rather than names or positions alone.

A complete repeat reproduced 39 generated artifacts byte-for-byte. The initial failing repair search was also retained, including the oracle’s signed-zero mistake, rather than overwritten by the corrected run.

A result must apply to the design being checked

Pre-repair evidence

Bound to the earlier design

The recorded design identity predates the correction.

Repaired artifact

Design identity changed

Earlier evidence is rejected as inapplicable.

Identity mismatch

In this experiment, pre-repair evidence was rejected against the repaired artifact because its design identity had changed. That rejection preserves the applicability of the evidence; it does not turn a bounded result into an unbounded proof.

---

Summary of Results & Boundaries

Within this bounded experiment, the Memdance stack:

1. Traced a wrong output bit to the target arithmetic pipeline and identified the intermediate rounding boundary where precision was lost.
2. Distinguished two adjacent operations returning identical bit-level outputs, identifying one as a contract violation and the other as valid under its own contract.
3. Rejected incomplete and over-broad candidate repairs in favor of a targeted correction that passed both contracts across the bounded sweep.
4. Localized a discrepancy to the reference oracle’s signed-zero handling, then retained the failing case and reran the sweep after correcting the oracle.

Explicit Evidential Boundaries

This experiment demonstrates bounded arithmetic verification; it is not an unbounded proof of arbitrary mathematical designs. The 4,096 passing vectors are retained as bounded regression evidence. Leaving the verification obligation explicitly open avoids converting finite passing tests into ungrounded claims of universal proof.

The repair search evaluated four defined candidates. This experiment does not establish general repair, inferred specification intent, arbitrary dot lengths or formats, independently varying right-hand operands, physical netlist tracing, or large-design scale.

Three experiments in preserved design meaning

1. 01
   Spatial identity

   Find the intended FIFO after structural changes.

2. 02
   Temporal identity

   Resolve ownership after reset and tag reuse.

3. 03
   Numeric contract

   Distinguish intentional rounding from lost information.

Together, these case studies examine spatial, temporal, and numeric aspects of design meaning. Our goal at Memdance is to determine how far maintaining those relationships can support engineering agents on increasingly difficult hardware problems. The useful question is not just what a value is, but what that value was promised to mean.