feat(prd-6-future): ledger-attest proc-macro crate — #[attested] lint skeleton (#59)#94
Merged
Merged
Conversation
… skeleton Closes #59. Establishes the type attestation infrastructure so formal verification coverage is machine-checkable at compile time. - crates/ledger-attest/: new proc-macro crate exporting #[attested("invariant")] - syn v2 / quote / proc-macro2 only, no runtime deps - emits const fn trait-bound check; missing Attested impl = compile error - crates/ledger-core/src/attest.rs: Attested trait + AttestationSpec struct - doc-test compile_fail covers the missing-impl error path - unit tests assert all three attestees return correct invariant strings - ConstraintEvaluation: #[attested("constraint_evaluation_bounded")] kani_module = "kani_proofs::vendor_constraints" - InvoiceVerification: #[attested("invoice_arithmetic_valid")] kani_module = "kani_proofs::invoice_arithmetic" - CommitGate: #[attested("commit_gate_total")] kani_module = "kani_proofs::commit_gate" Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…lt and MetaCtx Extends the attestation coverage from 3 to 8 types. All types with a meaningful verifiable invariant in the current codebase are now attested. Attested: - Z3Result: z3_result_confidence_total — to_confidence() is total - MetaCtx: meta_ctx_confidence_bounded — accumulated_confidence stays in [0,1] - DocumentFields: document_fields_decimal_safe — amount never passes through f64 - VendorConstraintSet: vendor_constraint_bounds_ordered — strong_ratio in [0,1] - AuditRow: audit_row_entry_id_deterministic — entry_id is blake3 of doc+ref Kani harnesses: - kani-proofs/src/z3_result.rs: 3 proofs (Satisfied/Violated/Unknown confidence) - kani-proofs/src/meta_ctx.rs: 1 symbolic proof (confidence bounded after 2 advances) - INVENTORY.md updated with 4 new rows (7 harnesses total) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Contributor
There was a problem hiding this comment.
Pull request overview
This PR introduces an attestation framework to the Rust workspace: a new ledger-attest proc-macro attribute (#[attested("…")]) plus a ledger-core::attest trait/metadata model, and wires several ledger-core domain types to declare formal invariants (with Kani proof module pointers where available).
Changes:
- Add
crates/ledger-attestproc-macro crate providing#[attested("invariant")]compile-time trait-bound enforcement. - Add
ledger-core::attest::{Attested, AttestationSpec}and implement/annotate multipleledger-coretypes with attestation metadata. - Extend
kani-proofswith new proofs forZ3Result::to_confidenceandMetaCtx::advance, and record them in the inventory.
Reviewed changes
Copilot reviewed 15 out of 16 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| kani-proofs/src/z3_result.rs | Adds Kani proofs for Z3Result::to_confidence mapping. |
| kani-proofs/src/meta_ctx.rs | Adds Kani proof that MetaCtx::advance keeps confidence bounded (under assumptions). |
| kani-proofs/src/lib.rs | Registers new Kani proof modules behind cfg(kani). |
| kani-proofs/INVENTORY.md | Documents the added proof entry points. |
| crates/ledger-core/src/workbook.rs | Marks AuditRow as attested and provides its Attested metadata. |
| crates/ledger-core/src/validation.rs | Marks MetaCtx/CommitGate as attested and adds Attested metadata (incl. Kani module pointers). |
| crates/ledger-core/src/pipeline.rs | Marks DocumentFields as attested and provides Attested metadata. |
| crates/ledger-core/src/lib.rs | Exposes new attest module. |
| crates/ledger-core/src/legal.rs | Marks Z3Result as attested and provides Attested metadata + Kani module pointer. |
| crates/ledger-core/src/constraints.rs | Marks constraint/verification types as attested and provides Attested metadata + Kani module pointers. |
| crates/ledger-core/src/attest.rs | Introduces AttestationSpec/Attested plus tests and a compile-fail doctest. |
| crates/ledger-core/Cargo.toml | Adds dependency on ledger-attest. |
| crates/ledger-attest/src/lib.rs | Implements the #[attested] proc-macro attribute. |
| crates/ledger-attest/Cargo.toml | Adds new proc-macro crate manifest. |
| Cargo.toml | Adds crates/ledger-attest to the workspace members. |
| Cargo.lock | Records new crate and dependency graph updates. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+27
to
+46
| let type_name = match &item { | ||
| Item::Struct(s) => s.ident.clone(), | ||
| Item::Enum(e) => e.ident.clone(), | ||
| _ => { | ||
| return syn::Error::new( | ||
| proc_macro2::Span::call_site(), | ||
| "#[attested] can only be applied to structs and enums", | ||
| ) | ||
| .to_compile_error() | ||
| .into(); | ||
| } | ||
| }; | ||
|
|
||
| let expanded = quote! { | ||
| #item | ||
|
|
||
| const _: fn() = || { | ||
| fn _assert_attested<T: crate::attest::Attested>() {} | ||
| _assert_attested::<#type_name>(); | ||
| }; |
Comment on lines
+16
to
+17
| /// use ledger_core::attest::Attested; | ||
| /// |
Comment on lines
+1
to
+14
| [package] | ||
| name = "ledger-attest" | ||
| version.workspace = true | ||
| edition.workspace = true | ||
| license.workspace = true | ||
| publish = false | ||
|
|
||
| [lib] | ||
| proc-macro = true | ||
|
|
||
| [dependencies] | ||
| syn = { version = "2", features = ["full"] } | ||
| quote = "1" | ||
| proc-macro2 = "1" |
Comment on lines
+28
to
+33
| use crate::constraints::{ConstraintEvaluation, InvoiceVerification, VendorConstraintSet}; | ||
| use crate::legal::Z3Result; | ||
| use crate::pipeline::DocumentFields; | ||
| use crate::validation::{CommitGate, MetaCtx}; | ||
| use crate::workbook::AuditRow; | ||
|
|
Member
|
@copilot apply changes based on the comments in this thread |
Copilot stopped work on behalf of
elasticdotventures due to an error
May 12, 2026 12:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
crates/ledger-attest/proc-macro crate exporting#[attested("invariant")]— no runtime deps, justsynv2 /quote/proc-macro2const fntrait-bound check: if the annotated type doesn't implementAttested, the compiler errors with a clear trait-not-satisfied messageAttestedtrait +AttestationSpecstruct incrates/ledger-core/src/attest.rsConstraintEvaluationconstraint_evaluation_boundedkani_proofs::vendor_constraintsInvoiceVerificationinvoice_arithmetic_validkani_proofs::invoice_arithmeticCommitGatecommit_gate_totalkani_proofs::commit_gateTest plan
cargo build -p ledger-attest— cleancargo test -p ledger-core— 159 unit tests + all integration suites passattestation_spec_invariant_strings_are_correct— all three return correct invariant stringsattestation_spec_kani_modules_are_set— all three havekani_module: Some(...)compile_fail— type withoutAttestedimpl fails to compile@copilot please review
🤖 Generated with Claude Code