Implement total pure v0 expression calculus

[alexlopashev]

Closes #104

Outcome

• add a closed checked evaluator for every v0 wire expression and pattern form
• retain only acyclic checked pure definitions; unknown, recursive, ambient, and hidden calls fail before evaluation
• support deterministic immutable values, exhaustive guarded matching, arbitrary-precision exact intermediates, checked machine arithmetic, explicit casts, and static or evidence-bound finite quantification
• publish EXP-01/EXP-02 evidence and include the focused target in the required CI partition

Red-to-green evidence

• Red: cargo test --test expression_calculus initially failed because bhcp::expression did not exist; the next focused run pinned record/tuple/let/if, match, and cast forms as BHCP4201 unsupported forms.
• Independent review reproduced overflow in a valid near-u64::MAX Rational comparison and identified unbound verifier witnesses, Text-only maps, rejected open-record extras, and an unbounded Decimal-exponent allocation path.
• Green: focused regressions cover every finding, including a 4-billion Decimal exponent faulting immediately as BHCP4202; the 10 calculus tests cover all constructors/patterns and adversarial totality/purity behavior.

Validation

• cargo fmt --check
• cargo clippy --all-targets -- -D warnings
• cargo test --all-targets (green in under one minute locally; focused calculus tests complete in 0.00s)
• cargo build --release
• cargo test --test schema_fixtures

Review finding resolution

• pinned safe-Rust big-number crates supply overflow-free exact intermediates; checked wire results still pass the canonical deterministic-CBOR value boundary.
• verifier witnesses are keyed by the complete deterministic expression, exact verifier identity, canonical evidence output, retained evidence value, trust classes, and finite domain.
• non-Text generic maps use deterministic-key-sorted unique [K, V] pairs; exact Text maps retain native canonical CBOR-map encoding.
• open records type-check and retain permitted extra fields; closed records still reject them.
• nonzero Decimal exponents above the deterministic 4096 evaluation ceiling fault before allocation; zero remains constant-time at any valid exponent.

Documentation impact

Updated README implementation coverage, the S5 implementation-status paragraph, conformance EXP evidence, and the CI semantic/conformance shard. General source definition resolution and semantic-IR elaboration remain explicitly deferred to #105.

Residual risk

The checked value model retains the repository-wide deterministic-CBOR integer component boundary; explicitly machine-sized overflow, non-integral Integer division, non-terminating Decimal quotients, and Decimal evaluation beyond the explicit allocation ceiling fault. The evaluator does not invoke verifier callbacks: it consumes evidence already accepted at the evaluation boundary and binds it to the complete checked quantifier.

Reviewed head

ea952c2b56510f803bb2aebc1e718900407b59d6

[alexlopashev]

Independent blocking review by Codex task /root/review_pr_87 at exact head fe5b32a235c5f72bf4b8e09c8905d53b7ea0adb3. GitHub rejected the formal REQUEST_CHANGES review because this task shares the PR author account; this comment records the independent task identity and blocking findings. Do not merge this head.\n\n1. [P1] Exact arithmetic faults on valid representable results (src/expression.rs:1026-1082). Comparisons and rational arithmetic cross-multiply in i128 before reduction. A focused boundary test using valid reduced rationals (u64::MAX-1)/u64::MAX and (u64::MAX-2)/(u64::MAX-1) should return true, but returns BHCP4202: exact comparison exceeds the executable number domain. Operands and Boolean result fit the canonical CBOR domain. This contradicts S4 unbounded exact numbers and S5, which names overflow faults for explicitly machine-sized operations. Use overflow-free exact comparison and cancellation/reduction, with regression coverage.\n\n2. [P1] Verifier-backed quantification accepts caller-fabricated witnesses without accepted evidence (src/expression.rs:19-22,175-191,644-668). The public context stores only expression_id -> Vec<Value> and retains no exact verifier identity, accepted evidence item, trust, predicate, or output. Any caller can make the evaluator treat a matching vector as “accepted.” checked_verifier_binding also accepts any checked output type and arbitrary non-empty trust text (src/expression.rs:1209-1228) instead of the CDDL evidence-type/evidence-class contract. Bind the witness to typed accepted evidence from the exact declared verifier boundary.\n\n3. [P1 authority contradiction] Generic map semantics are not implemented (schemas/v0/bhcp-v0.cddl:116,173; src/expression.rs:321-323,569-582; pre-existing src/typecheck.rs:2304-2317). Normative/wire map<K,V> and expression-key shapes are generic, while the value model/evaluator force Text keys. Resolve this explicitly by implementing canonical generic-key maps or narrowing the normative wire/claims through a reviewed roadmap decision before claiming every S5 form complete.\n\n4. [P2] Open-record construction rejects fields its declared type permits (src/expression.rs:260-268). CheckedType admits extra fields for record(open=true, ...), but this checker rejects them unconditionally. Preserve/type-check open-record extras or narrow the supported claim, with regression coverage.\n\nExisting focused tests are green but miss these boundaries. My independent exact-rational regression fails deterministically as described. No approval or merge is authorized.

[alexlopashev]

Addressed every blocking finding in 118c11faaab7307f795da4c5b4bcb7ac0cf4bb80:

1. Exact operations now use pinned safe-Rust arbitrary-precision intermediates; the reproduced near-u64::MAX comparison and a cancellation-heavy product are green.
2. Quantifier evidence is bound to the complete deterministic checked expression, exact verifier identity, canonical evidence output, retained accepted classes/trust, and exact finite domain. Raw expression_id -> Vec<Value> injection was removed.
3. Generic map<K,V> is implemented canonically: Text keys use CBOR maps; other key types use deterministic-key-sorted unique [K,V] pairs within the recursive value domain.
4. Open-record extras are checked and retained; closed records still reject undeclared fields.

Focused type/calculus tests and all five local gates are green. Please re-review only the new exact head.

[alexlopashev]

Independent re-review by Codex task /root/review_pr_87 at new exact head 118c11faaab7307f795da4c5b4bcb7ac0cf4bb80. The four findings from my prior blocking review are resolved: boundary rational comparison/product now use pinned arbitrary-precision intermediates and pass; quantifier witnesses are bound to the complete checked expression, exact verifier, validated evidence output/classes/trust, and exact domain; non-Text maps use deterministic encoded-key-sorted unique [K,V] pairs while Text maps retain native CBOR maps; and open-record extras are checked and retained. The exact-pinned num-bigint 0.4.6, num-integer 0.1.46, and num-traits 0.2.19 dependency surface is narrowly used and builds with default features disabled. Focused expression_calculus (10/10) and type_checker (18/18) pass.\n\nNew blocking finding — [P1] Valid Decimal exponents can exhaust memory instead of faulting (src/expression.rs:1557-1565). CheckedType accepts every deterministic-CBOR integer exponent, and exact_ratio accepts any magnitude through u32::MAX, then executes BigInt::from(10_u8).pow(magnitude). A valid untrusted Decimal with exponent 4_000_000_000 therefore attempts to materialize roughly four billion decimal digits (gigabytes of allocation); the process can OOM/abort rather than terminate with BHCP4202. This violates S5’s total/terminating expression boundary and reintroduces hidden resource divergence through the new arbitrary-precision path. Use a resource-bounded or symbolic decimal algorithm that compares/reduces exponents before materialization and fails closed under an explicit executable limit, then add an adversarial large-exponent regression that proves bounded completion.\n\nBecause this task shares the author GitHub account, formal REQUEST_CHANGES is unavailable; this comment records the independent task identity and blocks approval. Do not merge this head. No locks were touched.

[alexlopashev]

Resolved the Decimal allocation blocker in ea952c2b56510f803bb2aebc1e718900407b59d6. Nonzero exponents above 4096 now fail before any big-number allocation with stable BHCP4202; zero coefficients remain constant-time regardless of exponent. A 4,000,000,000-exponent adversarial regression and all five local gates are green. Please review the new exact head.

[alexlopashev]

Independent approval by task /root/review_pr_87 at exact head ea952c2b56510f803bb2aebc1e718900407b59d6.

Final re-review result: approved; no actionable findings.

• The Decimal exponent allocation blocker is resolved: nonzero Decimal exponents above the explicit executable limit are rejected with stable BHCP4202 before BigInt::pow; zero coefficients retain a constant-time zero path.
• The adversarial regression using exponent 4_000_000_000 passes.
• Focused local validation passes: the exact totality-attack test (1/1), expression_calculus (10/10), and type_checker (18/18).
• The prior four remediations remain intact: overflow-safe exact rational arithmetic; verifier-backed quantifier witness/output/trust/domain validation; generic non-Text map representation; and open-record extra-field preservation.
• Hosted format, clippy, release build, schema fixtures, test-plan, unit/binaries, and semantic/conformance checks are green at this head; remaining test shards are still running.

Because the shared GitHub account authored the PR, this comment records the independent reviewer identity and approval instead of an invalid author approval. Exact-head squash auto-merge may proceed once all required checks pass.