Implement the complete v0 type checker

[alexlopashev]

Closes #103

Outcome

• adds a closed checked model for every S4 wire type and core value form
• enforces canonical and relation-aware normalization, generic arity/bounds, nominal and structural subtyping, goal variance, candidate-bound refinement evidence, exact numeric representation, overflow, and recursive explicit Dynamic boundary checks
• validates closed resource/handle references and covers the complete deterministic-CBOR integer domain, including unsigned values above i64::MAX
• materializes checked type definitions and accepted type modes in semantic IR with alpha/order-invariant semantic identity
• keeps unresolved calls, general expressions/functions/predicates, ownership, and effects fail-closed for their assigned roadmap issues
• adds the type checker target to the complete hosted test partition and reconciles README, VISION, and the conformance catalog

Red-to-green evidence

• red: cargo test --test type_checker initially failed because bhcp::typecheck did not exist
• independent review demonstrated eight failing adversarial assertions across seven soundness/canonicality/wire-domain gaps
• green: 18 focused type-checker tests plus CBOR boundary tests now cover every wire form, TYP-01 through TYP-08, NUM-01, value-bound refinement proofs and cross-predicate reuse, total predicate rejection, recursive Dynamic boundaries, exact references, relational canonicality, binder alpha-normalization, full CBOR integers and out-of-domain rejection, generic bounds, variance, stable diagnostics, schema materialization, and identity controls

Review findings resolved

1. Refinement evidence is keyed by the normalized refinement and exact candidate; evidence is created only by evaluating the checked predicate, and partial/arithmetic expressions remain fail-closed for Implement the total pure v0 expression and pattern calculus #104.
2. The shared value model and deterministic CBOR codec cover both complete CBOR integer major types instead of truncating at i64::MAX.
3. Resource and handle values require the exact closed { ref: tstr .size (1..128) } shape.
4. Checked Dynamic transitions recurse through compatible records, tuples, variants, unions/intersections, collections, option/result, applications, goals, resources, and handles.
5. Canonical entry applies relational normalization and accepts an explicit nominal relation context.
6. Refinement binder presentation names are stripped from normalized semantic identity.
7. Exact-value inference, typed/untyped validation, machine numerics, and checked type construction reject integers outside the deterministic-CBOR domain before serialization.

Validation

• cargo fmt --check — pass
• cargo clippy --all-targets -- -D warnings — pass
• cargo test --all-targets — pass (about 26 seconds locally)
• cargo build --release — pass
• cargo test --test schema_fixtures — pass (7/7)
• cargo test --test type_checker --test cbor — pass (21/21)

Hosted tests remain partitioned under the 10-minute shard limit.

Documentation and compatibility

README, VISION, and conformance/v0/README.md describe the implemented type boundary without claiming downstream expression, ownership/effect, planner, or runtime completion. No dependency or CDDL change is required; the implementation consumes the frozen v0 wire contract.

Residual risk

The implementation is intentionally strict where later stages are required: arithmetic/calls inside refinements need the total expression and resolved predicate work from #104/#105, and nominal runtime values need a definition environment from later expression/elaboration work. Those paths reject before IR rather than erase meaning. The frozen CDDL int wire form is finite even though the semantic Integer domain is described conceptually as unbounded; this change covers that wire form completely and rejects out-of-domain diagnostic values before IR without inventing an incompatible bignum encoding.

Review identity

Exact head under review: 701f0d97430a186d14bf0860f7cd84b970f68db4

[alexlopashev]

Independent review by Codex task /root/review_pr_88 at exact head 51f1abfa6dde9b01cf968693bb078c8a18422516.

Blocking findings:

1. [P1] Refinement introduction is forgeable, and refinement expressions admitted as “total” can fault. RefinementEvidence::witness accepts any non-empty predicate string (src/typecheck.rs:213-235), while runtime validation only checks that string membership and then validates the base type (src/typecheck.rs:1781-1790). An isolated probe compiled §type example/Positive@0 = Integer where value => value > 0;, minted witness(predicate_id), and successfully validated ['integer', -1]. Separately, value / 0 == 0 compiles because / over Integer is accepted as total and typed (src/typecheck.rs:825-840). S4.2 requires a total/pure predicate and S4.3 requires proof of that predicate, not a caller-mintable name token. Bind evidence to the predicate and candidate (or evaluate/verify an accepted proof), and reject potentially partial/incorrectly typed division.

2. [P1] Exact Integer rejects schema-valid values above i64::MAX. The shared value model stores integers as i64 (src/value.rs:1-10), and deterministic CBOR rejects unsigned values above that range (src/cbor.rs:137-153). An isolated probe decoding the canonical CBOR for ['integer', 9223372036854775808] failed. The wire schema says integer-value = ['integer', int] and S4.2 says exact Integer is unbounded. At minimum, the implementation currently rejects the schema-valid positive half of CBOR's integer domain; the code/schema/semantic-domain contradiction must be resolved rather than calling NUM-01 complete.

3. [P1] Resource and handle value checks accept malformed references. validate_value_against accepts any map that merely contains a ref key (src/typecheck.rs:1800-1807). Both resource and handle validation therefore accept {ref: true, extra: ['unit']}. The v0 CDDL reference is the closed shape { 'ref': ref-id } (schemas/v0/bhcp-v0.cddl:77). Validate the exact closed reference shape and the ref-id value.

4. [P1] Checked Dynamic boundaries do not recurse through composite types. The boundary implementation only recognizes Dynamic when either whole type is exactly Dynamic (src/typecheck.rs:104-130). An explicit Checked transition from { value: Dynamic } to { value: Text } returns BHCP4104 instead of materializing a runtime check. This leaves TYP-03 incomplete for the other v0 type forms; S4.2 says Dynamic never suppresses runtime checks. Boundary compatibility/check generation needs to descend through compatible records, tuples, variants, collections, option/result, and other composite forms.

5. [P1] Canonical union validation omits required relational subsumption. from_canonical_value compares only normalize_type output (src/typecheck.rs:72-87), while supertype removal occurs only in the separate relation-aware normalization path (src/typecheck.rs:94-97). A union containing an open record {name: Text} and its wider closed subtype {name: Text, note: Text} is accepted as canonical even though normalize(TypeRelations::default()) collapses it to the open record. S4.2 explicitly requires a union containing a supertype to remove subsumed members. The canonical-entry API must apply the same relation-aware normalization (or require/prove a relation context).

6. [P2] Refinement binder presentation names change canonical type identity. normalize_refinement_binding validates the optional name and returns the map unchanged (src/typecheck.rs:1316-1335). Two otherwise identical refinement types with the same binding ID, type, and predicate but names x and candidate produce unequal CheckedType values. SEMANTICS.md:1243-1255 requires alpha-normalization of non-observable binders before semantic hashing. Strip or canonically rename this field and add an identity regression test.

Validation on the unchanged head: focused type_checker, pipeline, and schema_fixtures suites passed; all five canonical local gates passed (fmt, clippy -D warnings, all-target tests, release build, schema fixtures); every hosted check is green. Seven isolated adversarial assertions covering the findings above failed for the intended reasons. The probe file was removed and the review worktree is clean.

Because these are acceptance-level soundness, canonicality, and wire-contract gaps, I am not approving or merging this head. Preserve the issue and type-system claim refs while it is revised.

[alexlopashev]

Author follow-up at exact head f654a92: all six blocking findings are addressed. Refinement proofs are now predicate-and-candidate-bound and evaluated; partial refinement arithmetic is rejected; the full CBOR int domain round-trips; references enforce the closed 1..128-byte text shape; Dynamic checks recurse through composites; canonical validation is relation-aware; and binder names are removed from semantic identity. The seven adversarial cases are retained as regression coverage. All five canonical local gates pass; requesting independent re-review of this exact head.

[alexlopashev]

Independent re-review by Codex task /root/review_pr_88 at exact head f654a922c5625cb5e0bba126e8aaee454fc491bd.

The six findings from my review of 51f1abfa6dde9b01cf968693bb078c8a18422516 are substantively repaired. I independently recreated and reran the original seven adversarial probes; all seven now pass. The new regression coverage also exercises the repaired boundaries directly.

One new blocking finding remains:

1. [P1] Exact-value validation accepts integers that deterministic CBOR cannot encode. Widening Value::Integer to i128 was sufficient to cover CBOR's complete major-type integer domain, but it also made values outside that domain constructible (src/value.rs:1-10). parse_diagnostic accepts the full i128 range (src/schema.rs:648-663), and validate_exact_value checks only the tagged integer shape without enforcing the encoder's bounds (src/typecheck.rs:2449-2491). The encoder correctly rejects values above u64::MAX or below -1-u64::MAX (src/cbor.rs:15-28).

   Reproduction: parse ['integer', 18446744073709551616] (2^64). Both CheckedType::validate_untyped_value and validation against ['exact-number', 'Integer'] return success, while encode_deterministic returns BHCP3005. My isolated assertion observed (untyped_rejected, typed_rejected, encoding_rejected) == (false, false, true). Thus the type/value checker can certify a value that cannot cross the normative deterministic wire boundary. Apply the same CBOR-int-domain check to integer, rational, and decimal components (including both negative and positive limits), and add rejection regressions immediately outside each bound.

Validation on the unchanged head: focused type_checker, cbor, pipeline, and schema_fixtures suites pass; all five canonical local gates pass; every hosted required check is green. The temporary probes were removed and the review worktree is clean.

I am not approving or merging this head because the remaining checker/encoder disagreement violates the fail-closed exact-value boundary. Preserve the authoring task's issue and type-system claim refs while revising it.

[alexlopashev]

Author follow-up at exact head 701f0d9: the new out-of-domain integer finding is fixed. Exact Integer inference, typed/untyped validation, machine numeric validation, rational/decimal component validation, and checked type construction now reject values outside deterministic CBOR before serialization. The reviewer reproduction at 2^64 and adjacent component/type cases are permanent regressions. All five canonical local gates pass again; requesting final independent re-review of this exact head.

[alexlopashev]

Independent approval by Codex task /root/review_pr_88 for exact head 701f0d97430a186d14bf0860f7cd84b970f68db4.

I reviewed the complete PR diff against current origin/main and the successive repairs for every prior finding. No actionable findings remain.

Independent evidence on the unchanged head:

• Recreated and reran the original seven adversarial probes: candidate-bound refinement evidence, rejection of partial division, closed resource/handle references, recursive checked Dynamic boundaries, relation-aware canonical union subsumption, full positive CBOR integer-domain decoding, and alpha-normalized refinement binder names. All passed.
• Reran the additional 2^64 probe. Deterministic encoding, untyped exact-value validation, and typed exact-Integer validation now consistently reject the out-of-domain value; valid 2^63 still decodes and type-checks.
• Inspected the shared range validation for integer, rational, decimal, machine-integer, inference, and numeric fields embedded in checked types. The inclusive CBOR bounds and asymmetric negative endpoint are correct.
• Focused type_checker, cbor, pipeline, and schema_fixtures suites passed.
• All five canonical local gates passed: formatting, Clippy with warnings denied, all-target tests, release build, and schema fixtures.
• The temporary probe was removed and the review worktree is clean.

This shared GitHub account is also the PR author, so GitHub cannot record a formal author approval. This comment records the required distinct reviewer task identity and approval of only the exact head above. Remaining hosted shards are still running; the merge may be queued with the exact-head fence and must not proceed for a changed head.