Module verified 

Verified implementations of all of trame’s runtime traits: storage is heavily bounded, all operations are checked, we track a lot of things.

Structs

AllocHistory

History of operations for one allocation.

HeapOp

An operation that was performed on an allocation.

VArena

Fixed-size arena for Kani verification.

VFieldDef

A synthetic field for Kani verification.

VFieldView

A field view that borrows from a store.

VHeap

Verified heap that tracks state for Kani proofs.

VPtr

Fat pointer for verified heap operations.

VRuntime

A runtime that verifies all operations

VShapeDef

A bounded shape definition for Kani verification.

VShapeHandle

A handle to a shape in a DynShapeStore.

VShapeStore

A store of DynShape definitions.

VShapeView

A view into a shape, borrowing from a store.

VStructDef

A synthetic struct type for Kani verification.

VStructView

A struct type view that borrows from a store.

Enums

HeapOpKind

The kind of heap operation.

VDef

Type-specific definition for verified shapes.

VHeapError

Error from heap operations.

Constants

MAX_FIELDS_PER_STRUCT

Maximum number of fields in a struct (for bounded verification).

MAX_SHAPES_PER_STORE

Maximum number of shapes in a store (for bounded verification).

MAX_VARENA_SLOTS

Maximum number of arena slots for verification.

MAX_VHEAP_ALLOCS

Maximum number of allocations tracked by VHeap.

Functions

vshape_register

Register a new verified shape in the global store.

vshape_store

vshape_store_reset^⚠

Reset the global shape store. For testing only.

vshape_view

View a previously registered shape from the global store.

Type Aliases

VLayout

VLayoutError