Crate assura_types 

Type checking for the Assura contract language.

Builds a TypeEnv (type environment) from a ResolvedFile by mapping each symbol in the symbol table to its Type. For T013 this creates the scaffolding: type environment construction and the type_check entry point. Actual expression-level type checking (T014-T018) builds on this.

Re-exports

pub use checkers::FrameChecker;

pub use checkers::PendingDecreaseCheck;

pub use checkers::TaintLabel;

pub use domain::GeneratedTest;

pub use domain::TableSmtObligation;

pub use domain::TestGenerator;

pub use domain::TestKind;

pub use domain::TestableContract;

Modules

checkers

Structural checkers: linearity, typestate, effects, info-flow, generics, etc.

clauses

Clause-body type checking (requires/ensures/invariant expressions). Clause body type checking.

domain

Domain-specific checkers (memory, concurrency, security, formatting, etc.). Domain-specific type checkers.

inference

Expression type inference (infer_expr). Expression type inference.

Structs

TypeChecker

Builder for type-checking. Replaces the 5 standalone type_check* functions with a single composable API:

TypeEnv

Maps names to their types. This is the typing context built during type checking.

TypeError

A structured type error with error code, span, and message.

TypedFile

The result of successful type checking: the resolved file plus the type environment constructed from its symbols.

Enums

Type

Represents all Assura types in the type checker.

Functions

collect_table_smt_obligations

Collect SMT verification obligations for precomputed tables.

type_check

Type-check a resolved file with default configuration.