Skip to content

feat: provable-contracts-macros #[contract] must support trait impl methods #702

@noahgift

Description

@noahgift

Problem

#[provable_contracts_macros::contract("yaml", equation = "eq")] wraps the annotated function in a new function, which breaks trait impl methods because the wrapper changes the function signature.

This blocks contract enforcement on ~5,000 trait impl methods in pmat (33% of all functions). Current ceiling: 39.3% penetration — cannot exceed ~53% without this fix.

Evidence (pmat dogfood)

CB-1340: 5928 call sites / 15073 functions = 39.3%
- 5,008 pub fn covered (99.7%)
- ~1,100 private non-trait fn covered
- ~5,000 private trait impl fn: BLOCKED (proc macro breaks them)

Sub-agents correctly skip all impl Trait for Type { fn method() } because compilation fails:

error[E0407]: method `format` is not a member of trait `DeadCodeFormatter`

Proposed Solution

Add a pass-through mode for trait impl methods. When #[contract] detects it's on a trait impl method (via syn's ImplItemFn with a trait path), it should:

  1. Not wrap the function (no rename, no outer function)
  2. Instead, inject debug_assert! preconditions at the start of the function body
  3. Read pre/postconditions from the YAML equation and emit them as debug_assert!

Example:

// Current (breaks):
#[contract("yaml", equation = "eq")]
fn metadata(&self) -> ToolMetadata { ... }
// Expands to wrapper that changes signature → compile error

// Proposed (pass-through):
#[contract("yaml", equation = "eq")]  
fn metadata(&self) -> ToolMetadata {
    // Injected by proc macro:
    debug_assert!(/* precondition from YAML */);
    // Original body...
    let _result = { /* original body */ };
    debug_assert!(/* postcondition from YAML */);
    _result
}

Impact

  • Unblocks pmat from 39% → 95%+ enforcement penetration
  • Applies to all sovereign stack repos with trait-heavy architectures (MCP tools, AST strategies, quality analyzers)
  • aprender's apr-cli uses traits extensively — same blocker at 63%

References

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions