MV Validator Coverage ARCHIVE

MV Validator Coverage Specification

Version: v0.2.8 Status: Formalization of existing behavior Audit Reference: manus_epistemic_integrity_audit_2026-01-03_v0.2.2_response.md lines 65-67

Purpose

This document formalizes the exact coverage boundary of the MV (Mechanical Validation) arithmetic validator. It closes a deferred audit commitment and provides auditors with a canonical reference for what the system does and does not verify.

This document describes existing behavior. No code changes accompany this specification.

Coverage Summary

Claim Pattern	Outcome	Example
Valid arithmetic equality (true)	VERIFIED	`2 + 2 = 4`
Valid arithmetic equality (false)	REFUTED	`2 + 2 = 5`
Non-arithmetic claim	ABSTAINED	`forall x, P(x)`
Division by zero	ABSTAINED	`5 / 0 = 0`
Non-exact division	ABSTAINED	`7 / 3 = 2`
Float literals	ABSTAINED	`3.14 + 1 = 4.14`
Complex expressions	ABSTAINED	`(2 + 3) * 4 = 20`

Exact Pattern

The validator accepts claims matching this regex:

^\s(-?\d+)\s([+\-/])\s(-?\d+)\s=\s(-?\d+)\s*$

In plain language: a op b = c where:

a, b, c are integers (optionally negative, no decimal point)
op is one of: +, -, *, /
Whitespace is permitted around operands and operators

Source: governance/mv_validator.py:54-56

Outcome Definitions

VERIFIED

Returned when:

The claim matches the pattern
The operation a op b is defined (no division by zero, exact division)
The computed result equals c

Interpretation: The arithmetic equality is mechanically confirmed correct.

REFUTED

Returned when:

The claim matches the pattern
The operation a op b is defined
The computed result does NOT equal c

Interpretation: The arithmetic equality is mechanically confirmed incorrect.

ABSTAINED

Returned when ANY of:

The claim does not match the pattern
Division by zero is attempted (b = 0 with / operator)
Division is non-exact (a % b != 0 with / operator)

Interpretation: The validator cannot make a determination. This is NOT a failure; it is the correct response when the claim is outside the validator's scope.

What Is Covered

Feature	Status	Notes
Integer addition	Covered	`a + b = c`
Integer subtraction	Covered	`a - b = c`
Integer multiplication	Covered	`a * b = c`
Exact integer division	Covered	`a / b = c` where `a % b == 0`
Negative integers	Covered	`-5 + 3 = -2`
Arbitrary precision	Covered	Python integers have no overflow
Leading/trailing whitespace	Covered	Stripped before matching
Whitespace around operators	Covered	`2 + 2 = 4` matches

What Is NOT Covered

Feature	Status	Outcome	Rationale
Float literals	Not covered	ABSTAINED	Pattern requires `\d+` (no decimal point)
Scientific notation	Not covered	ABSTAINED	Pattern does not include `e` or `E`
Complex expressions	Not covered	ABSTAINED	Only binary `a op b = c` supported
Parentheses	Not covered	ABSTAINED	Not in pattern
Multiple operators	Not covered	ABSTAINED	Only single operator supported
Division by zero	Not covered	ABSTAINED	Undefined operation
Non-exact division	Not covered	ABSTAINED	`7 / 3` has remainder
Symbolic math	Not covered	ABSTAINED	No variable support
Inequalities	Not covered	ABSTAINED	Only `=` supported
Modulo operator	Not covered	ABSTAINED	Only `+`, `-`, `*`, `/`

Overflow Behavior

There is no overflow risk.

Python integers are arbitrary-precision. The expression 101000 + 1 = 101000 + 1 will be correctly evaluated as VERIFIED (assuming it matches the pattern, which it does not due to **).

For claims that DO match the pattern, such as:

999999999999999999999999999999 + 1 = 1000000000000000000000000000000

This will be correctly parsed and evaluated without overflow.

Determinism Guarantee

The validator is:

Pure: No side effects, no external calls, no randomness
Deterministic: Same input always produces same output
Bounded: O(n) time complexity where n is claim length

This determinism is required for replay verification integrity.

Tier Classification

MV Validator Correctness remains Tier B.

Tier B Definition: Logged and replay-visible. Violation is detectable but not prevented.
What This Means: All validation outcomes are logged in reasoning artifacts with validation_outcome and proof_payload fields. An auditor can replay the evidence pack and see exactly what the validator returned.
What This Does NOT Mean: Tier B does not claim that validator bugs are self-detecting. If the validator had a bug (hypothetically), the logged outcome would reflect the buggy behavior, not the correct behavior.

The coverage gaps documented above (floats, complex expressions, etc.) are by design, not bugs. They return ABSTAINED, which is the correct outcome for out-of-scope claims.

Audit Trail

This document closes a deferred commitment from the external audit response:

Resolution: Deferred to v0.2.4. Create docs/MV_VALIDATOR_COVERAGE.md documenting:

- Covered: a op b = c integer/decimal arithmetic

- Not covered: overflow, float precision, complex expressions

Source: manus_epistemic_integrity_audit_2026-01-03_v0.2.2_response.md lines 65-67

This commitment was deferred past v0.2.4 and is now delivered in v0.2.8.

How Auditors Should Use This Document

Scope verification: Check that demo claims match the covered patterns before expecting VERIFIED/REFUTED
ABSTAINED interpretation: Any claim outside the pattern table should return ABSTAINED
Replay validation: Evidence packs contain the full proof_payload with parsed values for independent verification
Coverage boundary testing: The demo deliberately shows ABSTAINED for out-of-scope claims (e.g., sqrt(2) is irrational)