prd-6-future phase 1: ledger-attest crate — #[attested] proc-macro lint skeleton

[promptexecutionerr]

Context

PRD-6-FUTURE.md defines a #[attested("invariant")] proc-macro attribute that enforces at compile time: any type claiming a formal property must implement Attested with at least one Z3 predicate or Kasuari constraint bound. Without the proc-macro crate, the concept exists only as a design document.

Phase 1 is the minimum skeleton: the attribute compiles, the trait is defined, the lint fires, and three types in ledger-core are decorated as the first attestees.

Crate Shape

New crate crates/ledger-attest/ (proc-macro crate):

[lib]
proc-macro = true

[dependencies]
syn = { version = "2", features = ["full"] }
quote = "1"
proc-macro2 = "1"

Exports:

// Usage: #[attested("gst_arithmetic_valid")]
#[proc_macro_attribute]
pub fn attested(attr: TokenStream, item: TokenStream) -> TokenStream { ... }

Effect: emits a compile-time static assertion that Attested is implemented for the annotated type. If the impl is absent, the error message reads: error: type Foo is decorated with #[attested("X")] but does not implement Attested for invariant "X".

Attested Trait (in ledger-core)

pub trait Attested {
    fn attestation_spec() -> AttestationSpec;
}

pub struct AttestationSpec {
    pub invariant: &'static str,
    pub z3_predicate: Option<&'static str>,
    pub kasuari_description: Option<&'static str>,
    pub kani_module: Option<&'static str>,
}

First Three Attestees

Decorate these types in ledger-core as the initial set:

#[attested("invoice_arithmetic_valid")]
pub struct InvoiceVerification { ... }
// impl Attested for InvoiceVerification:
//   z3_predicate: "total = subtotal + gst"
//   kani_module: "kani_proofs::invoice_arithmetic"

#[attested("commit_gate_total")]
pub enum CommitGate { ... }
// impl Attested for CommitGate:
//   z3_predicate: "Approved | PendingOperator | Blocked covers all Reconciled states"
//   kani_module: "kani_proofs::commit_gate"

#[attested("constraint_evaluation_bounded")]
pub struct ConstraintEvaluation { ... }
// impl Attested for ConstraintEvaluation:
//   kasuari_description: "strong_ratio, medium_ratio, weak_ratio in [0.0, 1.0]"
//   kani_module: "kani_proofs::vendor_constraints"

Acceptance Criteria

• cargo build -p ledger-attest succeeds.
• #[attested("X")] on a type without an Attested impl produces a compile error (verified via trybuild or compile_fail test).
• #[attested("X")] on a type with an Attested impl compiles without error.
• InvoiceVerification, CommitGate, ConstraintEvaluation implement Attested and compile.
• Attested::attestation_spec() is callable in tests and returns the correct invariant string.
• No runtime cost: Attested is a trait with a const-friendly associated function; the proc-macro emits zero runtime code.

Files

• crates/ledger-attest/ (new crate, proc-macro)
• crates/ledger-core/Cargo.toml — add ledger-attest path dep
• crates/ledger-core/src/constraints.rs — decorate ConstraintEvaluation, add Attested impl
• crates/ledger-core/src/validation.rs — decorate CommitGate, add Attested impl
• crates/ledger-core/src/workbook.rs (or constraints.rs) — decorate InvoiceVerification, add Attested impl
• Cargo.toml (workspace) — add crates/ledger-attest to members

Dependencies

Independent of #55–#58. Logically follows #56 (Kani harnesses) since kani_module pointers in AttestationSpec reference harnesses that should already exist. Can be built speculatively before Kani CI is green — the kani_module field is Option and not validated until PRD-6-FUTURE Phase 2.