trait-impl-pattern

Trait-Impl Pattern

Philosophy: Traits as ML Modules

Rust decided 40 years after ML modules were proven not to include them, opting instead for Haskell-style typeclasses (traits) for ad-hoc polymorphism. Because APAS-VERUS is a teaching corpus, we use traits to simulate module interfaces to maximize readability.

• Ignore standard Rust idioms: Do not restrict traits only to cases with multiple implementing types.
• Traits as Interfaces: Put almost every public function into a trait (some exceptions exist due to complex return types).
• Specs in Traits: Place the Verus specifications (requires / ensures) in the trait definition, not the implementation block. This separates the interface contract from the implementation details.

Every APAS module defines a trait containing all public functions, and implements them in a single impl Trait for Type block. There are no bare impl Type blocks for functions that belong in the trait.

Required Structure

pub trait FooTrait: Sized {
    fn new(...) -> Self;
    fn bar(&self, ...) -> ...;
    fn baz(&mut self, ...) -> ...;
}

impl FooTrait for Foo {
    fn new(...) -> Self { ... }
    fn bar(&self, ...) -> ... { ... }
    fn baz(&mut self, ...) -> ... { ... }
}

Bare impl Type is an Error

If the hole detector reports bare_impl, that means functions are on a direct impl Type block instead of impl Trait for Type. This must be fixed by moving the functions into the trait and the trait impl.

Recursive Spec Functions on Enums

Recursive spec fns can go directly in impl Trait for Type with decreases *self. Child traversal uses qualified trait calls: NodeTrait::spec_size(&*n). No inherent impl blocks or free spec fns needed. See multi-struct-spec-style.mdc for the full pattern and src/experiments/tree_module_style.rs for verified evidence.

For legacy code, the older delegation pattern (inherent methods + trait stubs) still works — see src/experiments/trait_decreases.rs Test 3. But the tree module style is preferred for new code.