multi-struct-spec-style

Multi-Struct Spec Style

Overview

For tree-like data structures with multiple node kinds (leaf, interior, root/tree wrapper), use separate structs composed into a discriminated enum. Each type gets its own trait with abstract specs and exec methods. Recursive spec fns go directly in the trait impl — no inherent impl blocks, no free spec fns, no stub delegation.

Structure

Types (bottom-up order)

pub struct Leaf { pub key: u64 }

pub struct Interior {
    pub key: u64,
    pub left: Option<Box<Node>>,
    pub right: Option<Box<Node>>,
}

pub enum Node {
    LeafNode(Leaf),
    InteriorNode(Interior),
}

pub struct Tree {
    pub child: Option<Box<Node>>,
}

• Structs ordered bottom-up: Leaf, Interior, Node, Tree.
• Tree is not in the enum — it wraps Option<Box<Node>>.
• Enum variants ordered bottom-up matching struct order.

Traits (bottom-up order)

Each type gets its own trait with abstract spec fns and exec methods:

pub trait LeafTrait: Sized {
    spec fn spec_size(&self) -> nat;
    spec fn spec_height(&self) -> nat;
    spec fn spec_contains(&self, needle: u64) -> bool;

    fn new(key: u64) -> (t: Self)
        ensures t.spec_size() == 1, t.spec_height() == 1, t.spec_contains(key);

    fn set_key(&mut self, key: u64)
        ensures self.spec_contains(key);
}

pub trait InteriorTrait: Sized { ... }
pub trait NodeTrait: Sized { ... }
pub trait TreeTrait: Sized { ... }

Impls (bottom-up order)

Impl member order matches trait declaration order.

Leaf — non-recursive, specs are constants or field comparisons:

impl LeafTrait for Leaf {
    open spec fn spec_size(&self) -> nat { 1 }
    open spec fn spec_height(&self) -> nat { 1 }
    open spec fn spec_contains(&self, needle: u64) -> bool { needle == self.key }
    fn new(key: u64) -> (t: Self) { Leaf { key } }
    fn set_key(&mut self, key: u64) { self.key = key; }
}

Interior — references children via qualified trait calls:

impl InteriorTrait for Interior {
    open spec fn spec_size(&self) -> nat {
        let l = match self.left { None => 0nat, Some(n) => NodeTrait::spec_size(&*n) };
        let r = match self.right { None => 0nat, Some(n) => NodeTrait::spec_size(&*n) };
        1 + l + r
    }
    // ...
}