feat(prd-6-future): ledger-attest proc-macro crate — #[attested] lint skeleton (#59)

Cargo.toml

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

crates/ledger-attest/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/src/lib.rs

@@ -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-core/Cargo.toml

@@ -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/src/attest.rs

@@ -0,0 +1,76 @@
+//! 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, VendorConstraintSet};
+    use crate::legal::Z3Result;
+    use crate::pipeline::DocumentFields;
+    use crate::validation::{CommitGate, MetaCtx};
+    use crate::workbook::AuditRow;
+
+    #[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");
+        assert_eq!(
+            Z3Result::attestation_spec().invariant,
+            "z3_result_confidence_total"
+        );
+        assert_eq!(
+            MetaCtx::attestation_spec().invariant,
+            "meta_ctx_confidence_bounded"
+        );
+        assert_eq!(
+            DocumentFields::attestation_spec().invariant,
+            "document_fields_decimal_safe"
+        );
+        assert_eq!(
+            VendorConstraintSet::attestation_spec().invariant,
+            "vendor_constraint_bounds_ordered"
+        );
+        assert_eq!(
+            AuditRow::attestation_spec().invariant,
+            "audit_row_entry_id_deterministic"
+        );
+    }
+
+    #[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());
+        assert!(Z3Result::attestation_spec().kani_module.is_some());
+        assert!(MetaCtx::attestation_spec().kani_module.is_some());
+        assert!(VendorConstraintSet::attestation_spec().kani_module.is_some());
+    }
+}

crates/ledger-core/src/constraints.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,7 +110,20 @@ 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.
+#[attested("vendor_constraint_bounds_ordered")]
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct VendorConstraintSet {
     pub vendor_id: String,
@@ -149,6 +166,17 @@ impl VendorConstraintSet {
     }
 }
 
+impl Attested for VendorConstraintSet {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "vendor_constraint_bounds_ordered",
+            z3_predicate: None,
+            kasuari_description: Some("evaluate() strong_ratio in [0.0, 1.0] for all finite f64 inputs"),
+            kani_module: Some("kani_proofs::vendor_constraints"),
+        }
+    }
+}
+
 /// Invoice arithmetic constraints (total = subtotal + gst).
 #[derive(Debug, Clone, Default)]
 pub struct InvoiceConstraintSolver {
@@ -213,6 +241,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/legal.rs

@@ -2,6 +2,8 @@
 //! Encodes hard legal predicates as satisfiability checks over transaction facts.
 
 use serde::{Deserialize, Serialize};
+use ledger_attest::attested;
+use crate::attest::{Attested, AttestationSpec};
 #[cfg(feature = "legal-z3")]
 use z3::{ast::Bool, Config, Context, SatResult, Solver};
 
@@ -44,6 +46,7 @@ impl Jurisdiction {
 }
 
 /// Result of Z3 SAT check.
+#[attested("z3_result_confidence_total")]
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub enum Z3Result {
     Satisfied,
@@ -98,6 +101,17 @@ impl From<Z3Result> for Vec<crate::validation::Issue> {
     }
 }
 
+impl Attested for Z3Result {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "z3_result_confidence_total",
+            z3_predicate: Some("to_confidence: Satisfied->1.0 | Violated->0.0 | Unknown->0.5"),
+            kasuari_description: None,
+            kani_module: Some("kani_proofs::z3_result"),
+        }
+    }
+}
+
 /// A legal rule encoded for verification.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct LegalRule {

crates/ledger-core/src/lib.rs

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

crates/ledger-core/src/pipeline.rs

@@ -3,6 +3,8 @@
 
 use serde::{Deserialize, Serialize};
 use std::marker::PhantomData;
+use ledger_attest::attested;
+use crate::attest::{Attested, AttestationSpec};
 
 // ============================================================================
 // TYPE-STATE: Compile-time valid transitions
@@ -21,6 +23,7 @@ pub struct Committed;
 #[derive(Debug)]
 pub struct NeedsReview;
 
+#[attested("document_fields_decimal_safe")]
 #[derive(Debug, Clone, Default, Serialize, Deserialize)]
 pub struct DocumentFields {
     pub vendor_jurisdiction: Option<String>,
@@ -32,6 +35,17 @@ pub struct DocumentFields {
     pub is_necessary: Option<bool>,
 }
 
+impl Attested for DocumentFields {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "document_fields_decimal_safe",
+            z3_predicate: None,
+            kasuari_description: Some("amount: Option<Decimal> — parsed via Decimal::from_str, never f64"),
+            kani_module: None,
+        }
+    }
+}
+
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct PipelineState<S = Ingested> {
     pub document_id: String,

crates/ledger-core/src/validation.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)]
@@ -92,6 +94,7 @@ impl Issue {
 }
 
 /// Accumulated state flowing forward through the pipeline.
+#[attested("meta_ctx_confidence_bounded")]
 #[derive(Debug, Clone, Default, PartialEq, Serialize, Deserialize)]
 pub struct MetaCtx {
     pub accumulated_confidence: f32,
@@ -232,6 +235,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 +333,29 @@ pub mod verbs {
     }
 }
 
+
+impl Attested for MetaCtx {
+    fn attestation_spec() -> AttestationSpec {
+        AttestationSpec {
+            invariant: "meta_ctx_confidence_bounded",
+            z3_predicate: Some("forall c in [0,1]: advance(c).accumulated_confidence in [0,1]"),
+            kasuari_description: None,
+            kani_module: Some("kani_proofs::meta_ctx"),
+        }
+    }
+}
+
+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::*;