Proof / property: resolver determinism + import-cycle rejection + qualified-path canonicality (ADR-014)

[hyperpolymath]

Parent: #513

Statement

Prove three properties of the resolver in lib/resolve.ml + lib/module_loader.ml:

1. Determinism: for a fixed program + module-search-path, resolve_program_with_loader returns the same symbol table on every call (no clock / hash-iter / fs-order leakage).
2. Cycle-freedom: import cycles are rejected at resolve time with an ImportCycle error.
3. Qualified-path canonicality (ADR-014 / LANG: type/effect grammar has no module-qualified path — Pkg.Type/Pkg.Effect unrepresentable (estate-wide port blocker; ADR-014) #228): Mod.T and Mod::T resolve to the same canonical symbol_id; an unbound Mod::T raises UnknownModule deterministically.

Mechanisation

Property tests (Alcotest + a small QCheck-style generator) suffice for (1) and (3). (2) needs a graph-cycle invariant — either property tests or a small TLA+ spec.

Target file: test/test_resolve_determinism.ml. The qualified-path part has prior art at test/test_qualified_paths.ml already; extend that suite.

Size

M. Estimate: 1 week. Mostly mechanical once a generator for "valid program with N modules + K imports" is in hand.

Status

NOT STARTED.

🤖 Generated with Claude Code