Repository navigation
Conversation
…r-api plutus-ledger-api V3 wraps the guardrail script hash of a NewConstitution action in a Constitution record: Constr 5 [Maybe GovernanceActionId, Constr 0 [Maybe ScriptHash]] (Contexts.hs:692, 706; cardano-ledger Conway/TxInfo.hs transConstitution). julc encoded Constr 5 [Maybe id, Maybe hash], so a Julc contract reading a NewConstitution proposal saw the wrong layout. - New ledger record Constitution(Optional<ScriptHash> script), Constr 0, following the Committee convention; NewConstitution now carries it. The compiler builds on-chain types from the bundled ledger-api sources, so nc.constitution().script() compiles to the Haskell layout with no compiler change. - Golden hex derived from Haskell for all seven GovernanceAction constructors (encode and decode), replacing the self-comparing assertions in LedgerParityTest. No other action differed. All seven also match Yano's independent ConwayTxInfoTranslator byte for byte. - Catalog, completions, native metadata and docs updated; release note. - julc-verification: the pinned CardanoLedgerApiBlaster model declares Constitution as Option ScriptHash without the Constr 0 wrapper; recorded in the capability note and ADR, to be reported upstream. Contracts that read constitution() must be recompiled; contracts that only match the NewConstitution case keep identical bytes. Fixes #223 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MQvHGqr1BvpfjkzfbHWfW
satran004
left a comment
There was a problem hiding this comment.
Correctness-focused review of 09ad5a8: recommend changes before merge. Two P1 findings are attached inline:
- Adding the bundled
Constitutiontype silently changes binding and typed-boundary semantics for an existing user-declared nested record of the same name. A before/after PV11 Java-VM probe reverses acceptance of the intended integer payload and a wrong optional payload, with no compiler diagnostics. - Formal verification still admits/promotes Constitution properties against the acknowledged incompatible pinned Lean layout. Documentation alone does not fail this path closed.
The actual ledger wrapper and CCL conversion match the Haskell representation. Independently ran the full compiler suite (1,782 tests), ledger-api (218), CCL integration (235), verification suite, and CLI suite (442 discovered, 5 skipped): no failures. Also ran a separate DSL-admission probe and a before/after compiled-UPLC/VM probe; their results expose the findings despite the passing existing suites. No external DevKit, Yano, or full Lean proof run was performed.
Posted as a COMMENT review because the authenticated GitHub account owns this PR; the recommendation is request changes.
| * A constitution: the optional guardrails script hash. The anchor is omitted, as in plutus-ledger-api V3. | ||
| * Encoded as {@code Constr 0 [Maybe ScriptHash]}. | ||
| */ | ||
| public record Constitution(Optional<ScriptHash> script) implements PlutusDataConvertible { |
There was a problem hiding this comment.
[P1] Preserve source-declared Constitution binding before bundling this type
The newly registered ledger type captures a previously valid nested source record. Reproduced with @MintingValidator class ReviewBinding { record Constitution(BigInteger value) {} @Entrypoint static boolean validate(Constitution c, ScriptContext ctx) { return true; } } (ordinary imports for BigInteger, annotations and ScriptContext). Both versions compile with no diagnostics. Evaluating the generated programs with the Java VM configured for PV11 and the same V3 context gives:
| Redeemer | Before this PR | This PR |
|---|---|---|
Constr 0 [I 42] |
success | UnConstrData: not ConstrData |
Constr 0 [Constr 1 []] |
UnIData: not IntData |
success |
The compiler/ledger source used for the baseline is identical to this PR's parent. This is not merely a source-compatibility warning: an unused typed parameter silently validates against the ledger record instead of the declaration Java binds to, changing which datum/redeemer representations are accepted. Referencing c.value() also newly fails member resolution. The release-note workaround to rename the user's record does not prevent the silent case. Please fix source-type resolution/registration precedence as part of adding this bundled name, and add both compile/evaluate regressions so local declarations retain their own schema. This violates the repository's source-name binding and typed-boundary invariants.
| {"id":"constructor.governance.noConfidence","kind":"CONSTRUCTOR","status":"TYPED","source":"Governance.lean","signature":"| NoConfidence : Option GovernanceActionId → GovernanceAction","note":"E.4k exposes the optional prior action under its guard."}, | ||
| {"id":"constructor.governance.updateCommittee","kind":"CONSTRUCTOR","status":"TYPED","source":"Governance.lean","signature":"| UpdateCommittee : Option GovernanceActionId → OldCommitteeMembers → NewCommitteeMembers → Quorum → GovernanceAction","note":"E.4k exposes reviewed collections while withholding raw quorum."}, | ||
| {"id":"constructor.governance.newConstitution","kind":"CONSTRUCTOR","status":"TYPED","source":"Governance.lean","signature":"| NewConstitution : Option GovernanceActionId → Constitution → GovernanceAction","note":"E.4k exposes prior action and optional script hash only."}, | ||
| {"id":"constructor.governance.newConstitution","kind":"CONSTRUCTOR","status":"TYPED","source":"Governance.lean","signature":"| NewConstitution : Option GovernanceActionId → Constitution → GovernanceAction","note":"E.4k exposes prior action and optional script hash only. The pinned model (@5dab3c43) declares Constitution as Option ScriptHash and omits the Constr 0 wrapper of plutus-ledger-api, so a verified contract that reads constitution().script() is evaluated against the wrong data shape until the pin is bumped (julc #223; to be reported upstream)."}, |
There was a problem hiding this comment.
[P1] Fail closed on the incompatible Constitution verification path
Leaving this capability TYPED makes the new note informational only. I reproduced successful DslPropertyValidator.validateAndNormalize and ComposedDslPromotion.promote for tx.proposals().exists(p -> p.actionStrict().exists(a -> a.whenNewConstitution((previous, script) -> script.isPresent()))); its generated Lean still calls the pinned IsData.fromData ... : Option GovernanceAction and matches a bare optional script.
At the pinned Governance.lean, Constitution is Option ScriptHash. Therefore the canonical new payload Constr 5 [Nothing, Constr 0 [Just (B hash)]] fails that strict action decoder: it tries to decode Just (B hash) as the bytes of a ScriptHash. The Nothing case fails for the same reason. The compiled validator now reads those ledger values correctly, while the admitted property cannot recognize them. Merely warning in JSON/ADR/release notes leaves a runnable verification path with the wrong meaning.
Please update/patch the model pin and add full payload encode/decode controls, or reject the affected strict-action/Constitution verification paths until that is available. Add an admission regression and cross-model controls for both script-present and script-absent canonical data; the existing tag/arity-only control does not detect this mismatch.
Fixes #223.
Summary
plutus-ledger-api V3 encodes
NewConstitutionasConstr 5 [Maybe GovernanceActionId, Constr 0 [Maybe ScriptHash]]. The guardrail script hash sits inside aConstitutionrecord (Contexts.hs:692, 706; cardano-ledgerConway/TxInfo.hstransConstitution). julc left out theConstr 0wrapper.Constitution(Optional<ScriptHash> script), encoded asConstr 0. It follows theCommitteeconvention, andNewConstitution(Optional<GovernanceActionId>, Constitution)now carries it.nc.constitution().script()compiles to the Haskell layout. A compiled-script test checks this against Haskell-layout data, for the hash both present and absent.makeIsDataSchemaIndexeddeclarations,Maybe/RationalToDataandtransGovAction.LedgerParityTest, a gap flagged in the Build JulcTransactionEvaluator script contexts as cardano-ledger does #221 review.ConwayTxInfoTranslatorbyte for byte.LedgerCatalog), playground completions, native metadata and docs, plus a release note.Compatibility
constitution()must be recompiled, and their script hashes change. Contracts that only match theNewConstitutioncase compile to identical bytes; the byte-snapshot tests pass.NewConstitutionnow passes aConstitution.Known: julc-verification Lean model
The pinned CardanoLedgerApiBlaster model (@5dab3c43) declares
ConstitutionasOption ScriptHash, without the wrapper, and upstream HEAD is the same.constitution().script()isn't sound until the pin is bumped.Tests
./gradlew testGovernanceTypeTest27/0,julc-verification92/0,julc-cli442/0ledger-conformance133/0, anchor 15/15,appchain-anchor-onchain120/120script-evaluatorsIndependently reviewed: the reviewer hand-checked all seven goldens against Haskell and approved. Minors applied.
🤖 Generated with Claude Code