Independent review of the refined analysis and library contracts

Codex-956atf /root/semantics_critic, 2026-09-11. Read-only review assigned by root; ownership announced in Gitea issue #1 comment 156, coordination reread through comment 162. Owned only this report and harness/experiments/refined-contracts-review-20260911/. The frozen proposals, earlier experiments/review, production, ledgers and Git state were not edited. No Cargo, compiler, native input or prototype evaluator was run in this review. Root retains ratification and integration.

Recommendation and blocking finding

Retain the refined direction: required property-owned base bindings, explicit ModelBaseline | Case(id), one level of case overrides, shared independently targeted checks, pure parameter-only calculations and complete immutable document freeze. Retain exact package/reference/base identity alongside verified same-origin typed-contract equivalence and a scoped expected-to-actual member/path/operation map. The paired reports now agree on these boundaries; the previous R1/R2/R3/R5/R6/R7 objections do not justify returning to complete bindings in every active case or strict whole-archive identity as quantity compatibility.

C1 is a P1 resource-policy omission to close before evaluator implementation: small acyclic accepted calculations can demand billions of dynamic calls while satisfying the listed static limits. Define deterministic total-work accounting and exhaustion behavior. It does not require changing the metamodel or compatibility direction. C2 is a P2 limitation of the finite library prototype's evidence: its Budget evaluator omits limit-unit kind validation. The production analysis contract already requires that rejection.

The reports establish a coherent next implementation contract, not production acceptance. In particular, neither the 120-assertion library prototype nor the 218-assertion context prototype executes the complete proposed UUID source/typed/frozen analysis examples. The nonempty imported freeze, complete operator/type profile, real source/history adapters and broad approximate engineering mathematics remain separate required work.

Exact inputs and independent readback

Frozen input	Independently verified SHA-256
Baseline contract	`9D294A3A8AD41EF4D07CAAC9FA410286F22EA5464400CCF01714F76E01BA5802`
Library contract	`30BBFD379EC542827A22D3B604534E5B6329CD913FF243747004E1AFA2983EE5`
Final library prototype source	`BC31BACF250F3711758717F18A3104696ED941C3C9B89817CAA6A96E6540062A`
Final library evidence manifest	`1EB643F20645A83E88E644B1F2C42D554F35259FA2CFCEAFA0632BF47C2ED966`

The isolated audit script completed 292 checks, exit 0, using Python 3.12.14. Its results enumerate every check and all 11 baseline fixture hashes. It reads JSON with duplicate-key rejection, hashes bytes, compares typed fixture records/manifests and calculates literal boundaries and a closed-form work-count witness. It does not implement the proposed source parser, evaluator, type checker, package materializer or Studio admission.

Command used:

& 'C:\Users\User\.cache\codex-runtimes\codex-primary-runtime\dependencies\python\python.exe' 'harness/experiments/refined-contracts-review-20260911/audit_fixtures.py'

Audit source SHA-256: A449587294C83891803E52721F727FC61A6448137B0C47E7FAB6E41373846B60. Result SHA-256: BA51FA4A98569D17D86772A30C7D9F3E305CF1879E6081170ECDD5EE99ACC594. The script writes only its own result file.

Independent results:

The proposed active source is exactly 55 lines and 2,678 UTF-8 bytes. Its 17 explicit distinct UUIDs equal the typed project/element/definition/scoped-parameter identity set. All inspected local definition, subject, property and parameter/call references resolve in their intended fixture categories.
The complete portable JSON embeds those exact source bytes. The decoded freeze capsule equals the complete portable file byte for byte, SHA-256 6667773D90F83626F760B2FAA2BF7D57638947D95574E3FA3E80B64416F01497.
All four frozen effective binding ASTs and Base/Override origins equal the captured degraded context. The shared predicate, four-definition inventory and document hash match. Imports/packages are explicitly empty, appropriate to this local example.
All 81 final library fixture hashes and byte counts match the recorded manifest. All 11 updated files equal both the complete expected document and separate-process reopened files. Only generated-final/ was used; the superseded preliminary directory supplies no evidence here.
The library author records 120 assertions and a separate fresh-process reopen, both exit 0; this review independently checked their persisted outputs, without rerunning that program. The earlier context experiment executed 218 assertions in its own limited integer-duration dialect. Counts are not counts of independent production tests.

C1 — P1: static bounds do not define a total evaluation-work bound

Locations: baseline contract lines 100, 108, 120, 134 and 182; the retained numeric profile in release-analysis-semantics-design-20260910.md:240. The latter lists depth 128, 65,536 expression nodes per case/definition closure, list length 1,024 and call depth 32. It bounds numeric intermediates and promises NumericLimit on computational exhaustion, but does not define whether closure nodes count distinct stored AST nodes, expanded work, or a runtime fuel charge.

Minimal falsifier, using only pure acyclic Number definitions and allowed exact operations:

f0(x) = x
fn(x) = f(n-1)(2*x) + f(n-1)(2*x + 1), for n = 1..30
requested result = f30(0)

There are 31 definitions, 333 stored expression nodes including the root call, and at most 31 call levels. Each nonleaf body has 11 expression nodes; f0 has one and the requested call adds two. Each body's AST depth is small. The expanded call graph has 2,147,483,647 dynamic definition invocations. At depth k the arguments are the distinct integers 0 through 2^k-1, so memoization keyed by definition and arguments does not collapse that work. Leaf inputs need only 30 bits and the exact result, the sum of 0 through 2^30-1, needs 59 bits. No large literal, overflow, recursion, list or anonymous dimension is involved. The audit computes these counts algebraically; it does not execute billions of calls.

Under the natural distinct-stored-node interpretation, this passes the named bounds but can occupy a worker for excessive time. If “nodes per closure” was meant to charge expanded work, the contract must state that rule and how it is counted without first expanding the graph. A bounded report trace alone does not bound evaluation.

Recommended resolution: add a numeric-profile-versioned deterministic work budget covering dynamic expression visits, function invocations, list elements and required exact-number work, with a separate aggregate request ceiling. Charge work through the shared evaluator, including calls and all requested outputs. Define a stable target/operand traversal and logical accounting so cache warmth or implementation optimization does not change Value versus NumericLimit. A fresh request-local accounting context is required; a process-wide mutable counter is unsuitable. Exact integer bit/intermediate limits still apply independently.

When fuel is exhausted, stop boundedly and return a located supported-operation failure/Unresolved outcome with NumericLimit and the causes actually collected. The strict rule to collect required-child causes must explicitly yield to terminal work exhaustion; it cannot require traversing all remaining siblings after the budget is gone. Do not present the resulting cause list as exhaustive. Admission can continue to accept a well-typed acyclic but expensive model; evaluation must fail predictably rather than hang or silently approximate. Choose the actual numeric ceiling from measured implementation costs before publishing the profile.

Acceptance falsifier: the example must terminate at the documented logical work limit with the same outcome and location under cold/warm caches and source/REST/private frozen replay. A nearby bounded example must succeed. Target ordering/aggregation and strict missing-plus-failure cases must obey the documented exhaustion rule. Root concurred that this is an implementation-blocking resource-policy omission, not a reason to reject B or typed compatibility.

C2 — P2: the finite Budget probe does not validate its threshold's kind

Locations: harness/experiments/library-compatibility-20260911/main.rs:781, :820, :870 and :908. Admission only gathers the Budget's left/right record references. evaluate_policy validates declared/input/unit kind compatibility for the two addends, then calls millis(limit) without checking the limit unit against the Budget's declared kind. millis reads the first millis= scale field and multiplies the magnitude; it does not itself establish a kind. In contrast, evaluate_check at lines 862–865 explicitly checks both effective input and limit kinds.

Source-derived counterexample, not an executed negative test: construct a valid initial fixture package with its existing Duration/Energy definitions and an additional row def|joule|Unit|Neutral|millis=1|Energy, using that archive's actual new digest. Keep both duration properties unchanged and set only the outside Budget limit to 2000@controls1:joule. This finite dialect can parse that unit row. The Budget path checks the duration addends, computes 1,500, converts the threshold numerically to 2,000 and reports satisfied; it does not reach a Duration-versus-Energy comparison. The odd millis= label is the prototype's scalar representation, not a claim about physical joules.

Resolution: do not cite the 120 assertions as full dimensional rejection coverage. The common production expression type checker must validate the comparison's threshold and every other operand, including unused/unselected checks; baseline contract lines 108 and 169 already require this. If this prototype is extended as evidence, add the same limit-unit kind check used by evaluate_check and explicit wrong-kind threshold cases. No frozen prototype was patched or rerun for this review. This finding does not invalidate its correct 1,500/1,650 ms examples or its same-origin compatibility comparison.

What the refinement resolves

Earlier concern	Concrete resolution checked	Evidence boundary
R4: repeated fixed assumptions across complete active cases	Properties own required bases; an absent override uses the base expression in the requested context. Explicit Unbound masks it; clearing removes only the override key. Checks are shared and targets explicit.	The 218-assertion comparison supports this choice. The new property-owned-base representation and UUID grammar are complete paper fixtures, not that executable's grammar.
R6: unnamed intermediate operators were incomplete	The table closes N/L/P/A operations, anonymous addition/comparison, Number normalization of A(0), explicit AsKind, affine point/difference rules and flat list Sum with an explicit initial value. Every unlisted combination rejects.	Specification-level closure; no complete force/length/affine/list type checker has run here.
R7: accepted exact literals could not round-trip through source	The component limit is 1,234 decimal digits with an actual 4,096-bit test. Integer/ratio canonical spelling avoids mandatory decimal expansion. Signed ratio literals preserve Number versus UnaryNegate AST identity.	Independently checked exact packet values and spellings; source-to-AST-to-source execution and the separate unary-negation packet remain implementation gates.
R1: concise instance source omitted authoritative state	Pending request, prepared directory and accepted source are distinct. Accepted files contain exact packages, typed bases, original/current maps and lineage. Stored old inputs verify the old base.	Final 11-file readback is complete for the finite dialect; production UUID allocation, atomic directory acceptance, stale plans and source/history parity remain unexecuted.
R2: cosmetic package update broke arithmetic and outside typed consumers	Exact DefRefs/pins remain distinct. Same nominal origin plus verified canonical rooted contract permits compatible typed use. Public result identity is anchored to its declared output reference. Scoped maps preserve expected/actual path and allocation identity.	The finite update retains `900 D1.ms`, declares `D2.Duration`, preserves the right instance/outside records and yields 1,650 ms. It covers one Boolean item/interface path, not every real data consumer.
R3: subjectless case/check export disappeared	Both contracts require explicit properties/checks/whole-case selection, all selected binding dependencies, and explicit external roles. No inverse pull of every case using a property.	Final D1 bytes explicitly contain P/K/C selection and the outside Q/G context. Complete Studio selection/transition is future work.
R5: immutable OA data could not become SA data by relabeling	Exact pinned target-layer counterpart or a fresh editable local derivative; no global OA/SA identity equivalence or mutation of the original mount. Reverse refinement must meet the actual demanded contract.	Finite complete dictionary/ports/exchange records exercise the disposition. Actual transition, operation occurrence and history integration remain separate gates.

The R7 measurements are concrete: 10^300 has 301 digits/997 bits; 1/(2^4095) has a 1,233-digit/4,096-bit denominator; -(2^4096-1) has a 1,234-digit/4,096-bit numerator. All are reduced and their source strings exactly represent the intended Number nodes. The ratio constructor makes the negative-literal distinction explicit without constant-folding arbitrary unary source.

R6 also intentionally allows dimension erasure through multiplication/division: Energy/Torque yields Number, while their addition/comparison and direct AsKind(Energy, TorqueValue) reject. An explicit dimension-algebra expression can reconstruct an anonymous quantity and then assert a kind. This is consistent with the proposed operator table; it must not be advertised as a proof that authors cannot deliberately reinterpret quantity meaning.

Engineering usability and remaining bounded integration gates

The active study contract no longer requires a first case, reusable calculation or a separate baseline identity to enter one property value. A small inline budget is legal. The complete 55-line example includes an optional reusable two-parameter calculation and threshold property to exercise identity and variation; those lines are not unavoidable overhead for every two-value budget. In the earlier 20-case experiment, B kept 62 binding rows versus D's 480, and changing one fixed assumption touched one B binding versus 20 D bindings. Factoring formulas also helped D, so only the repeated-input saving should be attributed to inheritance. D remains useful for independently authored studies; a complete private snapshot provides that independence for a frozen B study.

The required context explanation is now concrete: inherited formulas read the selected case, and every result/provenance stamp names its captured model and context. In the complete local example, baseline gives 7/4 s and satisfied; degraded gives 9/4 s and violated; unmeasured is Missing; Clear restores 7/4 s. These are hand-derived fixture expectations. The frozen manifest correctly selects the 1,250 ms override and shared formula; transport equality alone does not prove that an implementation evaluates it correctly.

Text-only library maintenance now has an explicit route to all required state. Generated version-controlled management files are acceptable as inspectable source state; the engine must own their legal transitions and cannot trust hand-edited historical claims. The final normalized update has 11 files/125 lines/5,708 bytes as reported. The 11-line creation request is a finite scenario macro dialect: budget supplies a 2,000 ms limit and global_case a 3,000 ms override from main.rs:605 and :638; those values become explicit in accepted output. That count is not evidence of a general public authoring grammar or human comprehension. This is not the earlier missing-prototype defect: all reusable prototype records are now in the exact package bytes.

Keep the following implementation gates concrete rather than repeating the broader design exercise:

One common evaluator/type checker: run the complete UUID source/typed examples; prove AST/source/AST identity for the three exact boundary packets and distinct UnaryNegate; add the wrong-kind threshold and C1 exhaustion controls. Exercise 3 N * 4 m + 2 N * 7 m, one outer Energy assertion and 26 J; anonymous compare/sum; named-kind mismatch; point subtraction, point-plus-difference and point-plus-point rejection. Approximate engineering operations require their own reproducible profile; exact rationals do not complete the release's full numeric scope.
Imported freeze and two-project reuse: use the final complete D1/D2 payloads as transport fixtures, then the real archive implementation. A second project must reopen solely from its declared files; selectively advance the first project's left instance while the second project and first project's right instance retain exact D1. Freeze with both D1 and D2, remove ambient files/cache, replay privately, corrupt one byte under an unchanged pin and require rejection. Later compatible content must never replace frozen bytes. The present library run creates two instances in Alpha; it is not an executed two-project library lifecycle or imported analysis freeze.
Actual typed consumer coverage: implement the class-specific rooted contract profile and feed the same proof through item/interface satisfaction, carried paths, exact operation allocations, message values and history/query projections. Existing crates/oa-core/src/data.rs:129 and :138 only apply local identity/ancestry; replacing those booleans alone is insufficient. The bounded path walker at :159 also illustrates why finite type graphs and bounded work are distinct requirements. Test repeated paths, two operations carrying one item, inheritance and changed cardinality without rewriting outside identities.
Ordinary source maintenance: execute first property, small budget, twenty-case fixed assumption edit, Unbound/Clear, selective library update and exact undo/reopen using the actual source/document boundary. Verify no-op compile, alias-only rename, stale prepared input and missing/corrupt management bytes. Measure wrong-context edits and repair comprehension as well as source size. Current Project in crates/oa-core/src/model.rs:1621 still lacks the proposed analysis/definition/import fields; current source/GUI successes do not establish these gates.

The exact package contract remains authoritative for resolution, update facets, history and freeze. Compatibility is a derived, versioned typed-use proof. That distinction is sufficient to converge now; adding global bridges, mandatory baseline elements, implicit case selection or cross-origin dimensional coercions would add state without resolving C1 or the remaining concrete integration gates.

19 KiB Raw Permalink Blame History Unescape Escape