feat(prd-6-future): ledger-attest proc-macro crate — #[attested] lint 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>

Author: Claude Sonnet (coordinator)

Cargo.lock

@@ -1,6 +1,7 @@
 [workspace]
 members = [
   "crates/ledger-core",
+  "crates/ledger-attest",
   "crates/ledgerr-focus",
   "crates/ledgerr-host",
   "crates/ledgerr-mcp",

Cargo.toml

@@ -0,0 +1,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"

crates/ledger-attest/Cargo.toml

@@ -0,0 +1,50 @@
+use proc_macro::TokenStream;
+use quote::quote;
+use syn::{parse_macro_input, Item, LitStr};
+
+/// Emit a compile-time trait-bound assertion that the annotated type implements
+/// `crate::attest::Attested`.
+///
+/// Usage (within `ledger-core`):
+/// ```ignore
+/// #[attested("my_invariant")]
+/// pub struct MyType { ... }
+/// ```
+///
+/// If `MyType` does not implement `Attested`, the compiler emits a
+/// trait-not-satisfied error at the call site.
+///
+/// # Note on crate paths
+/// The generated assertion references `crate::attest::Attested`. This macro is
+/// intended for use within `ledger-core`. External crates using this attribute
+/// must have `pub mod attest` with the `Attested` trait re-exported as
+/// `crate::attest::Attested` at their crate root.
+#[proc_macro_attribute]
+pub fn attested(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let _invariant_lit = parse_macro_input!(attr as LitStr);
+    let item = parse_macro_input!(item as Item);
+
+    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>();
+        };
+    };
+
+    expanded.into()
+}

crates/ledger-attest/src/lib.rs

@@ -30,6 +30,7 @@ arc-kit-au = { path = "../arc-kit-au", optional = true }
 tokio = { workspace = true }
 tracing = "0.1"
 notify = "8.2"
+ledger-attest = { path = "../ledger-attest" }
 
 # filesystem metadata — xattr on Linux; sidecar fallback is pure std
 [target.'cfg(target_os = "linux")'.dependencies]

crates/ledger-core/Cargo.toml

@@ -0,0 +1,50 @@
+//! Attestation trait — types with formal verification backing.
+
+/// Metadata describing a type's formal verification coverage.
+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>,
+}
+
+/// Implemented by types that carry formal property attestations.
+///
+/// # Compile-fail: missing impl
+/// ```compile_fail
+/// use ledger_attest::attested;
+/// use ledger_core::attest::Attested;
+///
+/// #[attested("missing")]
+/// pub struct MissingImpl { pub x: u32 }
+/// ```
+pub trait Attested {
+    fn attestation_spec() -> AttestationSpec;
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::constraints::{ConstraintEvaluation, InvoiceVerification};
+    use crate::validation::CommitGate;
+
+    #[test]
+    fn attestation_spec_invariant_strings_are_correct() {
+        assert_eq!(
+            ConstraintEvaluation::attestation_spec().invariant,
+            "constraint_evaluation_bounded"
+        );
+        assert_eq!(
+            InvoiceVerification::attestation_spec().invariant,
+            "invoice_arithmetic_valid"
+        );
+        assert_eq!(CommitGate::attestation_spec().invariant, "commit_gate_total");
+    }
+
+    #[test]
+    fn attestation_spec_kani_modules_are_set() {
+        assert!(ConstraintEvaluation::attestation_spec().kani_module.is_some());
+        assert!(InvoiceVerification::attestation_spec().kani_module.is_some());
+        assert!(CommitGate::attestation_spec().kani_module.is_some());
+    }
+}

crates/ledger-core/src/attest.rs

@@ -2,6 +2,8 @@
 //! Uses the Cassowary algorithm to evaluate constraints against transaction populations.
 
 use serde::{Deserialize, Serialize};
+use ledger_attest::attested;
+use crate::attest::{Attested, AttestationSpec};
 
 /// Constraint strength levels (matching Kasuari).
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
@@ -17,6 +19,7 @@ pub enum ConstraintStrength {
 }
 
 /// Result of constraint evaluation.
+#[attested("constraint_evaluation_bounded")]
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub struct ConstraintEvaluation {
     /// Whether REQUIRED constraints passed.
@@ -98,6 +101,7 @@ impl ConstraintEvaluation {
 }
 
 /// Structured result from invoice verification.
+#[attested("invoice_arithmetic_valid")]
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub struct InvoiceVerification {
     pub evaluation: ConstraintEvaluation,
@@ -106,6 +110,18 @@ pub struct InvoiceVerification {
     pub audit_note: String,
 }
 
+
+impl Attested for ConstraintEvaluation {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "constraint_evaluation_bounded",
+            z3_predicate: None,
+            kasuari_description: Some("strong_ratio, medium_ratio, weak_ratio in [0.0, 1.0]"),
+            kani_module: Some("kani_proofs::vendor_constraints"),
+        }
+    }
+}
+
 /// A historical constraint set for a vendor or category.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct VendorConstraintSet {
@@ -213,6 +229,18 @@ impl LayoutSolver {
     }
 }
 
+
+impl Attested for InvoiceVerification {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "invoice_arithmetic_valid",
+            z3_predicate: Some("total = subtotal + gst"),
+            kasuari_description: None,
+            kani_module: Some("kani_proofs::invoice_arithmetic"),
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

crates/ledger-core/src/constraints.rs

@@ -1,3 +1,4 @@
+pub mod attest;
 pub mod calendar;
 pub mod classify;
 pub mod constraints;

crates/ledger-core/src/lib.rs

@@ -4,6 +4,8 @@
 
 use std::fmt;
 use serde::{Deserialize, Serialize};
+use ledger_attest::attested;
+use crate::attest::{Attested, AttestationSpec};
 
 /// Disposition classifies how an issue should be handled by the pipeline.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
@@ -232,6 +234,7 @@ pub enum ApprovalGate {
 
 /// Gate decision for committing a reconciled transaction.
 /// Replaces unconditional tray-approval with confidence-aware routing.
+#[attested("commit_gate_total")]
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub enum CommitGate {
     /// All checks passed above threshold -- may commit automatically.
@@ -329,6 +332,18 @@ pub mod verbs {
     }
 }
 
+
+impl Attested for CommitGate {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "commit_gate_total",
+            z3_predicate: Some("Approved | PendingOperator | Blocked covers all Reconciled states"),
+            kasuari_description: None,
+            kani_module: Some("kani_proofs::commit_gate"),
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;