Repository navigation
docs: apply Phase 0 design review + nail five yellow-light joints - #2
Conversation
Apply the external Phase 0 review (SHOULD/COULD treated as MUST). The theme: remove semantic duplication and unencoded promises before any freeze. New specs and schemas: - SPEC_edict-lawpack-abi-v1.md (Lawpack ABI: pure/effect exports, semantic effects, proof-only vs runtime-materialized, typed obstruction payloads, target adapters, compatibility matrix). - docs/abi/ machine schemas as single source of truth: target-profile.cddl, target-lowerer.wit, lawpack.cddl. - docs/REQUIREMENTS.md Fixture Constitution; spec.lock.json; fixtures/ layout. Language/Core: - Minimal normative optic contract in Core; richer Observer Geometry as derived Aperture Ledger evidence (Option A). - Refined scalars String<max,canonical>/Bytes<max>; typed integer literals; pinned len units. - where = input refinement; mandatory else on runtime require/guarantee; short-circuit booleans; defined bounded for-loops. - Typed obstruction payloads with failure binders + exhaustive matching. - Core/target/admitted budget split; CapabilityRef<T>; namespace/shadowing and enum-vs-variant syntax rules; language vs minimal implementation profiles. - Purified Core IR: no self-hash, no lowerer/verifier/packaging fields in the preimage, verifiedOperationMode -> verifier report, pre/postconditions and diagnosticPolicy demoted. Target ABI / bundle / admission: - Real ABI: CDDL manifest + WIT plugin boundary + exchange types; pure/effect intrinsic class; removed duplicate manifest from the language spec. - Acyclic artifact graph: compile vs admission explanations, receipt body vs signature, universal acyclicity rule. - Logical source-path rules; semantic vs release bundle digests. Assurance: hash ladder, Aperture Ledger, Lawfulness Certificate, obstruction coverage, two-lowerer differential trial. Docs: edict code fences, corrected ER cardinality, bounded hello example, fixed alias-shadowing example. Design baseline marked non-normative historical context. Add .gitignore (.claude/, macOS, common dev artifacts) and CHANGELOG.md. Grammar and Core schema remain unfrozen; v1 is not stable.
Resolve the five underdetermined contracts flagged in review so implementation
semantics can be frozen by fixtures rather than prose.
1. Optic source production: add `basis` source clause (incl. `basis none`); one
deterministic source per Core optic field; basis is a typed Core expression,
apertureRequirement an explicit field, supportPolicy/lossDisposition are
canonical coordinates not strings (EDICT-OPTIC-SOURCE-001).
2. Lawpack classification: replace materialization with orthogonal
executionClass (proofOnly|runtime) x authoritative writeClass; readOnly
permits runtime reads (EDICT-LANG-READONLY-001).
3. Named typed failures: effects declare effectFailures (coordinate +
authorityClass + bounded payloadType); obstruction map keyed by failure
coordinate; target intrinsic CDDL is an enforced pure/effect union; lawpack
components made optional where appropriate (EDICT-ABI-FAILURE-NAMED-001,
EDICT-TARGET-INTRINSIC-UNION-001).
4. Digest wire format: canonical digest is typed [algorithm, bytes] across CDDL,
WIT, and bundle spec; "sha256:<hex>" is review-JSON only
(EDICT-DIGEST-WIRE-001).
5. Bundle subject: exact semantic/release preimages (toolchain identity in
release, not semantic); requests/receipts carry bundleSubject {kind,digest};
Moriarty tracks both; lowerer compares cost vs declared target ceiling, not
admitted budget (CONTINUUM-BUNDLE-SUBJECT-001).
Cleanups: canonicalEncode<T> returns bounded Bytes; bounded repo in the
normative example; missing lawpack adapter is a compiler/lowering error, not
admission-class. Registry + CHANGELOG updated.
Grammar and Core schema remain unfrozen; v1 not yet stable.
|
Warning Review limit reached
More reviews will be available in 40 minutes and 5 seconds. Learn how PR review limits work. Your organization has run out of usage credits. Purchase more credits in the billing tab to continue. ⌛ How to resolve this issue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based credits. 🚦 How do rate limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan refill rate. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, the refill rate gradually slows as usage increases. The highest same-day bursts are limited more strictly. Please see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (13)
WalkthroughPhase 0 Edict specification round 2: introduces canonical CDDL/WIT schemas for lawpack, target profile, and lowerer/verifier plugin boundary; adds new Lawpack ABI v1 specification; substantially revises language spec (typed obstructions, budget overhaul, optic contract, grammar tightening); updates continuum bundle/admission specs (bundleSubject identity, CBOR encoding); expands assurance transparency guide; introduces comprehensive requirements registry and fixture corpus framework; adds project scaffolding. ChangesEdict Phase 0 Specification Corpus
Estimated code review effort🎯 4 (Complex) | ⏱️ ~65 minutes Possibly related issues
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2352cad6aa
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
🔎 Audit triage — Code LawyerSelf-audit of Note: CodeRabbit did not review (org out of usage credits / rate-limited, ~43 min cooldown). Proceeding on Codex + self-audit. Queue (all resolved one commit per issue)
cc @codex for a second opinion on the fixes. Resolving now, one commit each. |
…admitted budget (EDICT-TARGET-NEUTRAL-LOWERING-001)
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
…ionMap (EDICT-CORE-GUARD-PAYLOAD-001)
…a coordinate (EDICT-CORE-WHERE-HASH-001)
…d map-key exclusions (EDICT-LANG-CAPREF-001)
…hority named failures (EDICT-ABI-FAILURE-NAMED-001)
…is specified (EDICT-ABI-LAWPACK-ADAPTER-DEFER-001)
…'t change semantic digest (CONTINUUM-SEMANTIC-OPTIONS-001)
… singular digest (CONTINUUM-BUNDLE-SUBJECT-001)
…quirement IDs (EDICT-TARGET-INTRINSIC-CLASS-001)
…CBOR size bound (EDICT-LANG-ENCODEMAX-001)
There was a problem hiding this comment.
💡 Codex Review
edict/docs/SPEC_edict-language-v1.md
Line 1700 in 2352cad
Carry guard obstruction payloads through Core
When a runtime require/guarantee maps to an obstruction with payload fields such as expected and observed, CoreGuard keeps only the obstruction coordinate and drops the payload constructor. That means source-level typed obstruction data cannot survive Core lowering for target-atomic guard failures, so guard obstructions become less expressive than effect obstruction maps; add a payload expression/constructor to the Core guard representation.
edict/docs/SPEC_edict-language-v1.md
Lines 1517 to 1520 in 2352cad
Add CapabilityRef to the Core type universe
The spec makes CapabilityRef<T> a first-class Core value, but the Core type universe listed here only includes records/enums/variants, Option, List, Map, and imported types. Implementations have no normative way to distinguish the built-in inert capability-reference type from an ordinary imported generic, so fixtures or effects that accept capability receipts will either be rejected or interpreted inconsistently.
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…LANG-BYTES-NOCANON-001)
…ntee authoritative) (EDICT-CORE-NODUP-PREPOST-001)
…e constructors (EDICT-LANG-ENCODEMAX-001)
…EDICT-ABI-INTRINSICS-DOC-001)
There was a problem hiding this comment.
Actionable comments posted: 18
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
docs/SPEC_edict-language-v1.md (2)
1856-1872: 🧹 Nitpick | 🔵 Trivial
readOnlydefinition is sound; the terminology distinction (runtime-materialized reads vs. records) clarifies any ambiguity.The definition at lines 1857–1860 is not contradictory. It correctly allows:
- Proof-only semantic facts (executionClass: proofOnly)
- Effects with writeClass: read, including runtime-materialized reads
The key insight from I-018 is that readOnly rejects "runtime-materialized semantic records" (writes), not "runtime semantic reads" (observations). These are distinct. The phrase "(including runtime semantic reads)" at line 1859 directly clarifies that runtime is allowed if writeClass is read. The final clause "no mutating writeClass" explicitly forbids write/create/delete/append.
The definition could be marginally tighter. "Plus" risks being read as ambiguous AND/OR logic when it means "accept category 1 OR category 2." A minor tightening would be:
"
readOnly: effects that are either proof-only semantic facts or have authoritativewriteClass: read(including runtime observations); no mutatingwriteClass."However, the current phrasing is acceptable as-is. The concern about contradictory "runtime + read-class" is unfounded given the explicit "no mutating writeClass" constraint.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/SPEC_edict-language-v1.md` around lines 1856 - 1872, Update the `readOnly` operation mode definition (lines 1857-1860) to clarify the logical relationship between its two acceptance criteria. Replace the "plus" conjunction with "either...or" phrasing to make explicit that effects matching category 1 (proof-only semantic facts) OR category 2 (writeClass: read) are accepted, eliminating any potential ambiguity about whether both conditions must be satisfied simultaneously. The updated phrasing should be: "effects that are either proof-only semantic facts or have authoritative writeClass: read (including runtime observations); no mutating writeClass."
1338-1352:⚠️ Potential issue | 🟡 MinorObstruction grammar correctly supports single-shorthand and multi-entry mapping; payload type checking is addressed in lawpack/profile ABI but normalization rule for bare coordinates is implicit.
The obstruction grammar properly enables:
- Single-shorthand:
else rope.WorldlineMissing- Multi-entry mapping:
else { missing => rope.WorldlineMissing, conflict => ... }- Optional failure binders:
mismatch(fault) => rope.TextBlobHashConflict({ ... })The examples throughout the spec (lines 481, 602, 605, 613, 2728, 2735) consistently use bare obstruction coordinates, confirming the grammar's optional payload syntax is intentional and correct. When payloads are present (e.g., line 640:
else rope.StaleBaseHead({ ... })), they are record literals.Payload type checking is defined: Lines 649–653 establish that obstruction payloads must be "typed and bounded" per the lawpack or target profile ABI. This is the correct place—the coordinate's payload schema lives in the ABI specification, not in the language grammar. You've delegated appropriately.
Empty payload normalization lacks explicit rule: The grammar allows bare
rope.WorldlineMissing, and the CoreExpr IR definition (line 1725) statespayload: CoreExpr # typed record expression; {} if empty. This implies bare coordinates desugar to empty{}at some point, but the spec never explicitly states this transformation. It's inferred from examples and implementation semantics, not normatively defined.Add a normalization rule or semantic note clarifying: "A bare obstruction-target is semantically equivalent to the same coordinate with an empty record payload
{}."🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/SPEC_edict-language-v1.md` around lines 1338 - 1352, The obstruction grammar correctly allows bare obstruction-target coordinates like rope.WorldlineMissing without payloads, but the spec lacks an explicit normalization rule clarifying how these bare coordinates desugar to empty record payloads. Add a normalization rule or semantic note immediately after the obstruction-target, obstruction-handler, and obstruction-map-lit grammar definitions that explicitly states: A bare obstruction-target without parenthesized payload is semantically equivalent to the same coordinate with an empty record payload {}, so rope.WorldlineMissing desugars to rope.WorldlineMissing({}). This makes the implicit transformation explicit and normative rather than inferred from examples and CoreExpr IR semantics.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/abi/edict-lawpack.cddl`:
- Around line 74-90: The shared type definitions `effect-failure`,
`effect-kind`, `authority-class`, and `core-type-ref` are duplicated across
multiple CDDL files and have already begun drifting (note `core-type-ref`
includes a comment in target-profile but not in lawpack). Create a new canonical
shared definitions file (e.g., `edict-shared-types.cddl`) and consolidate all
these shared types into it with their complete and final form (including
deciding whether `core-type-ref` should carry the "canonical Core type
coordinate" comment). Then update both `edict-lawpack.cddl` and
`edict-target-profile.cddl` to import and reference these definitions from the
shared file instead of maintaining local duplicates. This eliminates drift and
establishes a single source of truth for these critical type definitions.
In `@docs/SPEC_edict-language-v1.md`:
- Around line 1896-1907: In the canonicalization rules section (lines
2087–2113), add an explicit declarative list stating which Core intent fields
must be included in the hash preimage. The list should enumerate: Core intent
optic, requiredOperationProfile, target authorities, law profiles,
input-constraint reference, Core/target budgets, and body. This declarative
statement should directly follow the existing canonicalization mechanics
guidance (sort, encode integers/strings/bytes, alpha-normalize predicates) and
precede the exclusion rules for lowerer/verifier digests, verifiedOperationMode,
and preconditions/postconditions. This makes the hash-significant fields
explicit without requiring readers to cross-reference back to the preimage spec
section.
- Around line 1595-1608: The specification has an ambiguity regarding when
`else` clauses can be omitted in `require` and `guarantee` statements. The
current text states that requires "whose predicate depends on runtime state must
carry an else obstruction clause" with an exception only for verifierProof
checks, but does not explicitly address requires whose predicates depend only on
inputs (not runtime state and not verifierProof). Clarify this gap by adding
explicit guidance in the section around the total check requirement (constraint
EDICT-LANG-TOTAL-CHECK-001) that definitively states whether input-dependent
requires can omit `else` without verifierProof, or whether all runtime-checkable
requires without verifierProof must carry `else` regardless of input versus
state dependency. Ensure the clarification covers both cases shown in the
example (input-dependent like "input.repo != ''" versus runtime-dependent like
"currentHead == expectedHead").
- Around line 1525-1530: The map key restriction statement lacks
cross-references to essential implementation details that developers need. Add a
sentence immediately after the map-key-restriction paragraph (currently ending
at line 1530) that directs readers to the String canonicalization syntax
examples shown in the earlier section (around lines 1486-1489) and provides a
reference link to the Target Profile ABI specification document to clarify how
imported types declare canonical map-key semantics. This ensures developers have
clear, contextual guidance without having to search for scattered references
throughout the document.
- Around line 582-592: The canonicalization rules section does not explicitly
specify whether the digest carried by CapabilityRef<T> should be included in or
excluded from the Core IR hash preimage. Add explicit clarification to the
canonicalization rules section stating the digest treatment for
CapabilityRef<T>—specify whether the digest is included in the canonical
preimage (like lawpack/profile digests that affect effects), excluded like
verifier/lowerer component digests, or handled through an alternative mechanism.
Reference the three possible approaches outlined in the comment to guide your
decision.
- Around line 740-765: The spec section describing the three-layer budget model
is missing two critical definitions that are essential for implementers. First,
add explicit semantic definitions for each field in coreEvaluationBudget
(maxSteps, maxAllocatedBytes, maxOutputBytes) by documenting what each field
measures, its units, and the interpretation of its values—for example, clarify
whether maxSteps counts instructions, IR nodes, or uses another measure. Second,
clarify the targetBudget.value field format by explicitly documenting whether it
is a coordinate reference to a digest-locked budget schema in the contract
bundle, a lookup key into the target profile manifest, or another resolution
mechanism, and explain how a lowering engineer would dereference this value to
obtain the actual target-specific budget constraints. These definitions should
be added to the spec text immediately following the code block that shows the
budget structure.
- Around line 1214-1221: The specification has two unspecified gaps in integer
literal type resolution that need clarification. First, add documentation and an
error code requirement (separate from EDICT-LANG-INTLIT-001) to handle cases
where an explicit integer suffix mismatches the contextual type (such as 1i32
used in a U64 context). Second, clarify in the section listing context sources
(parameter type, field type, return type, target/lawpack argument type) whether
wrapped types like Option<T> are transparently unwrapped for literal type
resolution or treated as ambiguous contexts. Be explicit about whether
Option<I32> provides unambiguous context for resolving a bare literal to I32 or
if such cases are rejected.
- Around line 616-654: In the section describing single-obstruction shorthand
(which currently states that shorthand is legal only when exactly one
profile-declared domain-mappable failure class remains unmapped), add explicit
language to cover the edge case of zero domain-mappable failure classes. Specify
that if an effect has zero domain-mappable failure classes, the else clause may
be omitted entirely. Additionally, clarify that if the count of unmapped
domain-mappable failure classes is not equal to exactly one, the
single-obstruction shorthand form is rejected by the compiler. This ensures the
constraint is complete and leaves no ambiguity about what happens at the
boundaries of zero or multiple unmapped classes.
- Around line 1641-1657: In the Loops section (EDICT-LANG-LOOP-001) under the
paragraph starting with "The loop never silently truncates," replace the vague
phrase "if a runtime collection somehow exceeds its proven bound" with precise
language that clarifies this is a verifier or lowering defect, not a runtime
user-level fault. Add three explicit obligations: the lowerer must inject an
assertion that the collection size does not exceed the proven bound at the
target IR level, the verifier must validate that all loop code respects the
bound invariant, and specify that if this check fails at runtime it indicates an
internalFault or integrityFault (compiler/verifier defect), not a resourceFault.
Remove the resourceFault classification reference and eliminate the word
"somehow" to eliminate the false implication of non-determinism.
- Around line 1610-1630: The section on Where Clauses And Input Refinement
explains that inputConstraints must contain hash-significant typed predicate
trees, but only provides informal examples (binary operators with op/left/right
structure, field access with kind/of/field/type, function calls with call/args).
Add a formal schema definition for these typed predicate trees that specifies:
the complete set of allowed operator values (op), kind values, and call
coordinate formats; how type annotations attach to expression nodes (e.g., is
type on every node or only leaf nodes); composition and nesting rules for
combining predicates; and how polymorphic functions resolve their type
parameters within predicates. This can be presented as a JSON schema, grammar
notation, or a referenced definition from elsewhere in the spec if one already
exists, but must provide enough formal structure that conforming implementations
can validate and generate these trees without ambiguity.
- Around line 1664-1671: Add a formal definition section for the type function
CanonicalEncodedMax<T> that is currently only described in prose around line
1667-1671. This definition must include: a recursive formula or algorithm that
computes the maximum canonical-CBOR encoded byte length for every type in the
language, with explicit base cases for scalar types (U32, U64, String, etc.)
that cite concrete CBOR encoding byte counts from the edict.canonical-cbor/v1
specification, and recursive cases for composite types (List<T, max=M> and
Map<K, V, max=M>) that show how to calculate bounds based on element/entry
bounds and container overhead. Reference the CBOR RFC or normative encoding
specification to establish the exact byte widths for each type's encoded
representation so that implementers and verifiers can compute
CanonicalEncodedMax<T> deterministically without guesswork.
- Around line 1632-1639: In the Boolean Evaluation section, you need to address
two specification gaps. First, add a dedicated subsection that explicitly
defines the proof refinement mechanism by explaining that it employs
flow-sensitive type narrowing and describing how guard conditions (like
isSome(x)) enable safe operations (like unwrap(x)) in the subsequent expression.
Second, replace the parenthetical reference to A-normal effect form with an
explicit cross-reference to the Expressions section (lines 1537-1558) where
A-normal form is defined, and add a dedicated rule stating that boolean operands
must be pure expressions. Ensure both the proof refinement mechanism and the
effect rejection rule are formally specified as normative constraints rather
than implied by example or passing reference.
- Around line 1305-1313: The basis-clause grammar definition lacks explicit
constraints on what basis expressions can reference, unlike the where-clause
which clearly states constraints on predicates. Add explicit documentation for
the basis-clause section stating whether basis expressions can only reference
inputs and pure functions, whether they can invoke arbitrary functions, and
whether all functions must be from Core or lawpack. Additionally, basis
templates are referenced in multiple locations throughout the spec (including
around lines 1421-1423 and 1981) but are never formally defined anywhere. Add a
definition section or clarification explaining what basis templates are, what
format they take, how they are referenced by consumers, and whether the Target
Profile ABI v1 and Lawpack ABI v1 specifications define templates and should be
forward-referenced in the language spec.
- Around line 1973-1994: The Optic Contract table has three underspecified
entries that create normative ambiguity. First, add an explicit cross-reference
to SPEC_edict-target-profile-abi-v1.md in the row defining "resolved
operation-profile optic template" for opticKind and boundaryKind to clarify
where the template is sourced. Second, resolve the contradiction in the
apertureRequirement row by clarifying whether it is always a coordinate
reference (as shown in the line 1929 example) or can be an inline footprint
ceiling expression, and if conditional, specify the rules for each case. Third,
add documentation authority clarification to the supportPolicy and
lossDisposition rows explaining who owns the continuum.support coordinate
namespace and how new policies are registered in that namespace.
- Around line 1710-1730: The CoreGuard definition (lines 1710-1713) does not
clarify whether the obstruction field is required or optional, creating a
conflict with the source-level semantics that states verifierProof checks may
omit the else obstruction clause. Add explicit clarification to the CoreGuard
construct definition explaining how the obstruction field is handled for each
enforcement type (targetAtomic, verifierProof, and localDiagnostic).
Specifically, either mark the obstruction field as optional (using the ? syntax
like failureBinder on line 1720) if verifierProof guards do not require an
obstruction, or explain what synthetic/default value is used when the
source-level obstruction clause is absent. Also update the corresponding JSON
schema examples to show the actual representation for verifierProof guards with
missing obstruction clauses.
- Around line 1158-1177: The prelude section lacks explicit enumeration of
available operations and constructors, creating dangerous ambiguity about what
constitutes the actual language. Expand the prelude definition in the "Names,
Namespaces, And Shadowing" section (or create a dedicated "Prelude" section) to
explicitly list: all arithmetic operators (e.g., `+`, `-`, `*`, `/`, `%`,
bitwise operations if supported) with their overflow semantics and any checked
variants; all string and bytes operations by name with full type signatures;
clarification of whether type constructors like `Option<T>`, `List<T>`, `Map<K,
V>` are prelude exports or language syntax; and any numeric helper functions
such as `min`, `max`, `abs` if they exist. Use concrete examples and a complete
roster format to eliminate ambiguity about what the prelude actually provides.
- Around line 2292-2312: Remove the speculation that the Jedit stress test
(Appendix A) may require non-minimal features like variants or Map, as the code
actually only uses minimal-v1 compliant features (records, enums, Option, List,
pure first-order functions, if expressions, branch-yield, target/lawpack
effects, guards, obstructions, and budgets). Additionally, clarify that the
syntax for declaring capability flags in bundle metadata is not specified in
this Language Profile section but is instead defined in the referenced Continuum
Contract Bundle v1 specification, so readers understand where to find that
information rather than expecting it here.
- Around line 1479-1511: The spec underspecifies when and how bounds violations
are enforced for pure helpers. Add clarity to the specification around line 995
(where pure lawpack helpers are described) to explicitly state: the enforcement
point for bounds violations (whether during type checking of the helper
signature, during lowering of effect calls, or during lawpack import
validation), and how opaque helpers interact with the bounds requirement
(specifically whether an opaque helper with an unbounded String return can be
accepted with a declared conservative bound, or if it must be rejected
outright). Reference the existing constraints at lines 767-769 and
EDICT-LANG-BOUNDS-001 to ensure consistency.
---
Outside diff comments:
In `@docs/SPEC_edict-language-v1.md`:
- Around line 1856-1872: Update the `readOnly` operation mode definition (lines
1857-1860) to clarify the logical relationship between its two acceptance
criteria. Replace the "plus" conjunction with "either...or" phrasing to make
explicit that effects matching category 1 (proof-only semantic facts) OR
category 2 (writeClass: read) are accepted, eliminating any potential ambiguity
about whether both conditions must be satisfied simultaneously. The updated
phrasing should be: "effects that are either proof-only semantic facts or have
authoritative writeClass: read (including runtime observations); no mutating
writeClass."
- Around line 1338-1352: The obstruction grammar correctly allows bare
obstruction-target coordinates like rope.WorldlineMissing without payloads, but
the spec lacks an explicit normalization rule clarifying how these bare
coordinates desugar to empty record payloads. Add a normalization rule or
semantic note immediately after the obstruction-target, obstruction-handler, and
obstruction-map-lit grammar definitions that explicitly states: A bare
obstruction-target without parenthesized payload is semantically equivalent to
the same coordinate with an empty record payload {}, so rope.WorldlineMissing
desugars to rope.WorldlineMissing({}). This makes the implicit transformation
explicit and normative rather than inferred from examples and CoreExpr IR
semantics.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 8b1292a0-e8aa-4b75-987b-a86f1ea77e9e
📒 Files selected for processing (17)
.gitignoreCHANGELOG.mdREADME.mddocs/DESIGN_runtime-neutral-edict-sha-lock-assurance.mddocs/GUIDE_edict-assurance-transparency.mddocs/README.mddocs/REQUIREMENTS.mddocs/SPEC_continuum-admission-v1.mddocs/SPEC_continuum-contract-bundle-v1.mddocs/SPEC_edict-language-v1.mddocs/SPEC_edict-lawpack-abi-v1.mddocs/SPEC_edict-target-profile-abi-v1.mddocs/abi/edict-lawpack.cddldocs/abi/edict-target-lowerer.witdocs/abi/edict-target-profile.cddlfixtures/README.mdspec.lock.json
📜 Review details
🧰 Additional context used
🪛 LanguageTool
docs/SPEC_edict-lawpack-abi-v1.md
[grammar] ~33-~33: Ensure spelling is correct
Context: ...e conformance posture. Without it, every lawpack import is a well-dressed mystery. This...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
🔇 Additional comments (24)
docs/abi/edict-lawpack.cddl (1)
1-73: LGTM!docs/abi/edict-target-profile.cddl (1)
1-109: LGTM!docs/abi/edict-target-lowerer.wit (1)
1-77: LGTM!docs/SPEC_edict-lawpack-abi-v1.md (1)
1-281: LGTM!docs/SPEC_edict-target-profile-abi-v1.md (1)
27-40: LGTM!Also applies to: 43-107, 108-135, 176-211, 216-218, 233-245, 268-276
docs/SPEC_edict-language-v1.md (5)
537-538: Delete this comment — the specification is explicit and correct.The spec defines
readOnlyas a union of two independent conditions:
- Proof-only semantic facts (any
writeClass)- Effects whose authoritative
writeClassisread(anyexecutionClass)The clause "proof-only semantic facts plus effects whose authoritative
writeClassisread" uses "plus" to mean "and also," not "and both." This directly confirms orthogonality: a proof-only fact withwriteClass: createis readOnly, and a runtime effect withwriteClass: readis readOnly. The spec is unambiguous and handles all combinations correctly. No verifier clarification needed.
2087-2113: Canonicalization rules already cross-referenced in earlier section—spec defines where excluded fields live.The fields you questioned are actually defined earlier in the spec (lines 1963–1971):
verifiedOperationMode(line 1963): Explicitly stated as "a verifier-report field, not a Core claim. Core states the requirement; the verifier proves the verdict" (EDICT-CORE-VERIFIED-EXTERNAL-001).preconditions/postconditions(lines 1966–1968): Explicitly stated as "derived indices over the body'srequire/guaranteenodes… these flat arrays are derived analysis and excluded from the preimage" (EDICT-CORE-NODUP-PREPOST-001).diagnosticPolicy(lines 1970–1971): Explicitly stated as "a compile option / diagnostic sidecar selector. Repair wording is not operation law" (EDICT-CORE-NODIAG-001).The canonicalization rules section (lines 2087–2113) references these exclusions without re-explaining them. For pedantic clarity, the canonicalization rules could explicitly cross-reference the earlier field definitions (lines 1963–1971) when excluding these at lines 2106–2107, rather than requiring readers to hunt backwards. The source-location handling (lines 2101–2102) is clear: removed from hash input, included in sidecar diagnostic maps.
> Likely an incorrect or invalid review comment.
40-67: Surface map correctly enforces no-duplication constraint; manifest ownership properly delegated.The revised surface map splits Edict language semantics from lawpack and target profile ABIs, referencing separate SPEC documents. The no-duplication mandate (
EDICT-ABI-NODUP-001) is correctly enforced at lines 1812–1818: the language spec explicitly states it "intentionally does not duplicate the manifest JSON," and the canonical manifest is defined once inSPEC - Edict Target Profile ABI v1with machine schemas (abi/edict-target-profile.cddl,abi/edict-target-lowerer.wit).Verified: No JSON manifest structures or prose duplications of the canonical manifest exist in the Target Profiles section (lines 1779–1825) or anywhere else in this document. The boundary constraint is properly maintained.
1061-1076: Optic contract preservation is correctly integrated across Language and Target Profile specs.All three concerns are addressed:
Requirement IDs verified: Both
EDICT-OPTIC-PRESERVE-001andEDICT-OPTIC-SOURCE-001are documented in REQUIREMENTS.md. The PRESERVE requirement explicitly states "recorded or rejected," which forbids silent erasure.Aperture Ledger confirmed as recording mechanism: The spec establishes derived verifier evidence (the Aperture Ledger) as the authoritative store for support loss, degeneracy, footprint overlap, and witness debt. These are separated from Core syntax as intended.
Target Profile ABI enforces non-erasure constraint: The target-profile-abi spec explicitly mandates that lowering must preserve optic structure and states: "Support loss, degeneracy, footprint overlap, and witness debt cannot be silently erased by Core lowering, target lowering, or explanation artifacts." This cross-spec constraint is enforced across all lowering phases, not left implicit.
The spec correctly delegates the optic contract to Core IR, derived evidence to the Aperture Ledger, and enforcement to both the Language spec and Target Profile ABI spec. No gaps found.
1281-1290: The grammar correctly forbids type parameters in functions; reread the grammar rules to avoid confusion.The original concern is based on a misreading of the grammar:
Functions are monomorphic. The
fn-declgrammar (lines 1293–1294) does NOT include type parameters:fn-decl = "fn" , ident , "(" , param-list? , ")" , "->" , type-ref , pure-block ;Type parameters appear only in
type-decl(line 1262:type-params?). Thetype-args?at line 1281 (inqual-ident , type-args?) applies to usage of named types withintype-ref, not to function declarations. Functions cannot be generic.I-004 is irrelevant to this concern. I-004 ("Total Bounded Evaluation") forbids recursive function calls in v1, not generic or polymorphic functions. The grammar proves generics are rejected without requiring explicit mention in I-004.
Scalar-refine bounds are already enforced. The spec states (line 1498): "A naked, unbounded runtime
StringorBytesvalue is rejected." The grammar'sscalar-refinemakesmaxmandatory andcanonicaloptional, which aligns with the boundedness requirement. No clarification needed.Do not second-guess the grammar; read it precisely.
> Likely an incorrect or invalid review comment.docs/SPEC_continuum-admission-v1.md (4)
23-24: ⚡ Quick winSharpen purpose statement to mention
bundleSubjectexplicitly.The phrase "reference a contract bundle digest" is technically accurate but imprecise—the actual structure is
bundleSubject { kind, digest }. Readers scanning the purpose may miss that kind is a first-class component of the identity contract. Given that lines 73–78 later emphasize this point ("Carrying the fullbundleSubject— not a singular digest"), the purpose should be equally precise up front.✨ Proposed clarification
- Continuum admission is participant policy over a participant-neutral contract - bundle. Admission requests and receipts reference a contract bundle digest; they - are not components of that digest. + Continuum admission is participant policy over a participant-neutral contract + bundle. Admission requests and receipts reference a `bundleSubject` (identifying + which bundle—semantic or release—by kind and digest); they are not components of + that bundle digest.
30-65: LGTM! ThebundleSubjectdefinition and receipt split (body hashed separately from DSSE envelope) correctly implement the acyclicity requirement and bundle-subject contract. Receipt body echoingbundleSubjectand the explicit note that "a body never points to the envelope signing it" are surgical and precise.
71-79: LGTM! Admission Explanation section sharply defines the policy-epoch-specific role and critical constraint that it "lives outside the contract bundle" and must never be hashed into the participant-neutral bundle. The emphasis on carrying fullbundleSubject(not a singular digest) for replay/hash-impact tooling is exactly right.
81-87: LGTM! "Admission Evidence Is External" and "Policy Replay Defense" sections are watertight. Binding the admittedbundleSubject(kind + digest) in replay defense preserves detectability across semantic vs release bundle changes, and the note that "requests and receipts reference abundleSubjectbut are not components of either bundle digest" is unambiguous.Also applies to: 115-128
docs/SPEC_continuum-contract-bundle-v1.md (5)
26-68: LGTM! The Artifact Layers restructure is sharp. SeparatingAdmissionRequestandAdmissionReceiptBodyas explicit layer citizens, showing their bundleSubject {kind, digest} fields side-by-side with the bundle, and explicitly separating receipt body from DSSE envelope in DistributionEnvelope make acyclicity transparent. The note at lines 62–64 that "The signature lives in the distribution envelope, never inside the body it authenticates" is surgical.
84-94: LGTM! The semantic/nonsemantic compile-options split is razor-sharp. Line 84–85 states only semantic-affecting options entersemanticCompileOptionsDigest, explicitly excluding diagnosticPolicy and repair text. Line 91–94 correctly situates admission explanation as policy-epoch-specific and external (not hashed into participant-neutral bundle). This aligns perfectly with the assurance guide and CONTINUUM-SEMANTIC-OPTIONS-001.
100-159: LGTM! Semantic and Release Bundle Digest preimages are comprehensive and acyclic.semanticBundleDigest(lines 105–119) includes only operation-law-significant content;releaseBundleDigest(lines 135–148) layers on source provenance, toolchain identities, and nonsemantic compile options without back-referencing the semantic digest (preserving DAG invariant per line 151–152). The note at lines 130–133 that identical semantic content from different lowerers/verifiers must produce the same digest is a critical invariant for the two-lowerer trial.
187-201: LGTM! The "Logical Source Paths" subsection is a clean addition. The constraints (UTF-8, forward slashes, no dot-segments, no drive letters or absolute machine paths, no symlink-derived values) prevent unintended machine-local pollution of bundle provenance. Example and rejection criterion are unambiguous. Reference to CONTINUUM-SOURCEPATH-001 grounds this in the requirements registry.
238-241: LGTM! The digest wire-format rule is spot-on. Mandating[algorithm, bytes]typed pair in authoritative CBOR (never hex string) and allowing hex only in review JSON enforces EDICT-DIGEST-WIRE-001 and prevents accidental hex-only serialization in production contexts. The example["sha256", h'..32 bytes..']is crystal clear.docs/GUIDE_edict-assurance-transparency.md (5)
62-62: ⚡ Quick winClarify "decision / obstruction taxonomy" semantics.
Line 62 uses
decision / obstruction taxonomywithout explaining what "decision" means in this context. Does it mean admission outcomes (accept/reject) paired with observed obstructions? Or decisions about which obstructions to record? Suggest rewording to eliminate ambiguity.
69-102: LGTM!
211-211: ⚡ Quick winDefine or cite the "I-014" constraint reference.
Line 211 states the Lawfulness Certificate is "never runtime authority (I-014)" but the identifier "I-014" is not defined or cited elsewhere in this guide. Readers cannot verify what constraint I-014 represents or cross-reference it in the specification. Either define I-014 inline or provide a citation to the normative document where it is defined (e.g., Language spec, Requirements registry).
30-30: No action required—all requirement identifiers are properly defined and consistently named.All five requirement identifiers cited in the guide (
CONTINUUM-BUNDLE-DAG-001,EDICT-OPTIC-PRESERVE-001,EDICT-LANG-OBSTRUCT-EXHAUST-001,EDICT-CONFORMANCE-DIFFERENTIAL-001,CONTINUUM-BUNDLE-DAG-MORIARTY-001) are formally defined in REQUIREMENTS.md and consistently referenced across all specification and guide documents with zero naming variants, typos, or traceability breaks. Requirement IDs are uniquely assigned.
57-57: ThebundleSubjectstructure and semantic/release threading are already correct and consistent with the Continuum specs. The verification shows no issues.The guide's definition (
bundleSubject { kind: semantic | release, digest }) on line 57 precisely matches the specs (SPEC_continuum-contract-bundle-v1.md line 158 and SPEC_continuum-admission-v1.md line 30). The semantic/release distinction is correctly threaded:
- AdmissionRequest declares
bundleSubject(admission-v1.md:30)- AdmissionReceipt echoes the same
bundleSubject(admission-v1.md:53)- Admission Explanation references
bundleSubjectto identify which bundle it explains (admission-v1.md:73–78)The Moriarty matrix tracking both
semanticBundleDigest(executable semantics) andreleaseBundleDigest(semantics + provenance + toolchain) is orthogonal to bundleSubject and raises no contradictions. This guide is sound.
…andbox+fuel (EDICT-ABI-VERIFIER-BOUND-001)
…hema drift (EDICT-ABI-NODUP-001)
🧾 Code Lawyer — Activity SummaryTwo review batches landed: Codex (precise, high-signal) and CodeRabbit (ASSERTIVE, after its cooldown). All Codex threads resolved with one commit each; the concrete CodeRabbit-class defect (CDDL type drift) resolved. Resolved — Codex review (14 threads)
Resolved — CodeRabbit
Outstanding — 16 CodeRabbit threads (deferred, needs maintainer decision)The remaining 16 CodeRabbit findings are all on Recommendation: convert these 16 into Phase-0 implementation tickets (they map cleanly onto fixtures in the requirements registry) rather than blocking this docs PR. Holding for maintainer direction; not auto-resolving. |
…ficant (EDICT-LANG-CAPREF-001)
… zero omits else (EDICT-LANG-OBSTRUCT-EXHAUST-001)
… declared ceiling (EDICT-LANG-BUDGET-UNITS-001)
🧑⚖️ Code Lawyer — round 7Two Codex batches. The valuable ones this round were grammar gaps my consistency sweeps never checked — examples that couldn't even parse under the normative grammar:
Sweep: IDs 77/77 (0 missing/orphan), no stale CDDL refs, tables/links/JSON clean, 0 unresolved threads. @codex — addressed. The uniqueness guarantees are now structural (coordinate-as-map-key, redundant fields removed), and the keyword-exclusion limit is documented honestly rather than claimed. |
|
To use Codex here, create an environment for this repo. |
✅ Re: Codex review summary on
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: cc8e89a497
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| | EDICT-LANG-TOTAL-CHECK-001 | Runtime `require`/`guarantee` must carry `else`; faults are typed, never host exceptions | Language | `lang/require/with-else` | `lang/require/missing-else` | spec | | ||
| | EDICT-LANG-BOOL-001 | Boolean `and`/`or` operators short-circuit | Language | `lang/bool/short-circuit` | `lang/bool/effect-in-operand` | spec | | ||
| | EDICT-LANG-LOOP-001 | `for ... bounded N`: List only, list order, prove M<=N, never silently truncate | Language | `lang/loop/bounded-list` | `lang/loop/unprovable-bound` | spec | | ||
| | EDICT-LANG-OBSTRUCT-EXHAUST-001 | Obstruction mapping is exhaustive over domain-mappable classes, with typed payloads | Language | `lang/obstruct/exhaustive-payload` | `lang/obstruct/missing-class` | spec | |
There was a problem hiding this comment.
The registry row for EDICT-LANG-OBSTRUCT-EXHAUST-001 still defines the rule and negative fixture in terms of domain-mappable classes, but the language/target specs now require exhaustiveness by failure coordinate. When an effect declares two domainMappable failures with different coordinates, a fixture generated from this row could miss an unmapped coordinate arm and still satisfy the class-level wording, weakening the conformance suite for the updated rule.
Useful? React with 👍 / 👎.
| ; `effect-signature(coordinate)`). Each map key MUST equal its record's | ||
| ; `coordinate` field (EDICT-ABI-INTRINSIC-UNIQUE-001). |
There was a problem hiding this comment.
This comment still says each intrinsics map key must equal a record coordinate field, but the intrinsic union below deliberately has no coordinate member and the later comment says the key is the coordinate. If validators or fixtures follow this normative MUST, valid coordinate-keyed intrinsic documents can be rejected or padded with a non-schema field.
Useful? React with 👍 / 👎.
| | budget-clause ; | ||
| profile-clause = "profile" , qual-ident ; | ||
| implements-clause = "implements" , qual-ident ; | ||
| basis-clause = "basis" , ( "none" | expr ) ; |
There was a problem hiding this comment.
basis and none contextual
Adding basis/none as literal clause tokens collides with the spec's own rule that keywords are not bare identifiers unless they are explicitly allowed contextually. Without that carve-out, existing valid source using a record field named basis (e.g. { basis: input.basisId }) and the prelude constructor none<T>() become unparseable even though only a local binding named basis was meant to be forbidden.
Useful? React with 👍 / 👎.
| types: [* exported-type], | ||
| constants: [* exported-constant], | ||
| pureFunctions: [* pure-function], | ||
| effects: [* semantic-effect], | ||
| obstructions: [* obstruction-def], |
There was a problem hiding this comment.
These export arrays all contain records with a coordinate, but arrays allow two helpers/effects/obstructions with the same coordinate and different signatures or payloads. Source calls and adapter lowering resolve lawpack exports by coordinate, so a manifest with duplicate coordinates would leave binding nondeterministic; mirror the operation-profile map pattern or add explicit uniqueness validation for these export coordinates.
Useful? React with 👍 / 👎.
| acceptedCoreAbi: [+ tstr], | ||
| dependencies: [* lawpack-dep], ; acyclic, digest-locked (EDICT-LAWPACK-DAG-001) | ||
| exports: resource-ref, | ||
| ? targetAdapters: [+ target-adapter], ; required only if any runtime effect exists |
There was a problem hiding this comment.
The manifest keeps targetAdapters as an array, so two entries can advertise the same acceptedTargetProfile/acceptedTargetIr while pointing at different adapter resources. In that case the v1 rule that exactly one adapter resolves for a selected target becomes ambiguous even though the manifest still validates; key this collection by the digest-locked target profile (or require uniqueness) so ambiguous adapter sets are rejected at import time.
Useful? React with 👍 / 👎.
| | EDICT-LAWPACK-PURE-IMPL-001 | Exported pure helper needs a hash-bound implementation (edict body or component+sandbox+fuel) | Lawpack | `lawpack/pure/has-impl` | `lawpack/pure/signature-only` | spec | | ||
| | EDICT-LAWPACK-ADAPTER-TARGETIR-001 | Target adapter digest-locks its accepted target profile + Target IR; resolution can't bind a republished IR | Lawpack | `lawpack/adapter/targetir-locked` | `lawpack/adapter/targetir-unlocked` | spec | | ||
| | EDICT-ABI-FAILURE-UNIQUE-001 | An effect's `effectFailures` coordinates must be unique (obstruction map keyed by coordinate) | Target/Lawpack | `abi/failure/unique-coords` | `abi/failure/dup-coord` | spec | | ||
| | EDICT-ABI-FAILURE-IDENT-001 | Failure coordinates must be bare Edict `ident`s (source obstruction map LHS only accepts ident) | Target/Lawpack | `abi/failure/ident-coord` | `abi/failure/hyphen-coord` | spec | |
There was a problem hiding this comment.
The ABI rule now requires failure coordinates to be non-keyword Edict identifiers, but this registry only plans a hyphen-coordinate negative fixture. A coordinate like else or basis matches the CDDL regex but cannot be named on the source obstruction-map LHS, so the conformance suite can miss the extra keyword-exclusion validator that the schema comment requires.
Useful? React with 👍 / 👎.
1 participant
Applies the external Phase 0 design review to the Edict specs (SHOULD/COULD treated as MUST), then nails the five underdetermined contracts flagged in the follow-up yellow-light review. Documents-only; no code. Grammar and Core schema remain unfrozen and v1 is not declared stable — the intent is to make fixtures, not prose, the mechanism for remaining questions.
Commits
c7fae0d— apply Phase 0 review (encode promises, kill duplication)2352cad— nail the five yellow-light joints before Phase 0 buildRound 1 — encode promises, one fact one owner
SPEC_edict-lawpack-abi-v1.md) — the missing normative owner: pure-vs-effect exports, semantic effects, typed obstruction payloads, target adapters, compatibility matrix.docs/abi/edict-target-profile.cddl,edict-target-lowerer.wit,edict-lawpack.cddl; prose JSON declared generated/illustrative; duplicate manifest removed from the language spec.canonicalizationProfile), no lowerer/verifier/packaging fields in the preimage,verifiedOperationMode→ verifier report, pre/postconditions demoted to derived indices,diagnosticPolicy→ compile option.String<max,canonical>/Bytes<max>), typed integer literals,where= input refinement, mandatoryelse, short-circuit booleans, bounded loops, exhaustive obstruction matching with payload binders.CapabilityRef<T>; namespace/shadowing + enum-vs-variant rules; language-vs-minimal implementation profiles.docs/REQUIREMENTS.md) +spec.lock.json+fixtures/layout; assurance tooling (hash ladder, Aperture Ledger, Lawfulness Certificate, obstruction coverage, two-lowerer trial)..gitignore+CHANGELOG.mdadded.Round 2 — five yellow-light joints
basissource clause (incl.basis none); one deterministic source per Core optic field;basisis a typed Core expression;supportPolicy/lossDispositionare coordinates.materialization→ orthogonalexecutionClass(proofOnly/runtime) × authoritativewriteClass;readOnlypermits runtime reads.effectFailures(coordinate + authorityClass + bounded payloadType); obstruction map keyed by failure coordinate; target intrinsic CDDL is an enforced pure/effect union; optional lawpack components.[algorithm, bytes]everywhere; hex is review-JSON only.semanticBundleDigestvsreleaseBundleDigestpreimages (toolchain identity in release, not semantic); requests/receipts carrybundleSubject {kind,digest}; Moriarty tracks both; lowerer compares cost vs declared target ceiling, not admitted budget.Cleanups:
canonicalEncode<T>returns boundedBytes; boundedrepoin the normative example; missing lawpack adapter is a compiler/lowering error.Verification
No orphaned terms (
materialization/runtimeMaterialized, singularcontractBundleDigest, hex-string digests in schema field defs), no broken internal links, no Markdown table-pipe hazards, nothing junk staged.Not in this PR (deliberately deferred)
Actual fixtures, the
spec.lockgenerator + doc-build gate, and thekv.transactional@1reference interpreter — these belong to the Phase 0 implementation campaign.