assura-types 0.4.3

Type checking for the Assura contract language
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

// TypeError is a diagnostic struct (only allocated on the error path) and
// intentionally carries rich context. Suppressing because boxing 200+
// return sites would add noise with no performance benefit.
#![allow(clippy::result_large_err)]

//! 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.

/// Structural checkers: linearity, typestate, effects, info-flow, generics, etc.
///
/// See `CHECKER-LAYERS.md` for how `checkers/`, `checks/`, and `domain/` differ.
pub mod checkers;
/// Wiring functions that run domain and structural checkers.
mod checks;
/// Clause-body type checking (requires/ensures/invariant expressions).
pub mod clauses;
/// Type conversion functions (AST TypeExpr, raw tokens -> Type).
pub(crate) mod convert;
/// Domain-specific checkers (memory, concurrency, security, formatting, etc.).
pub mod domain;
/// Type environment construction.
pub(crate) mod env;
/// Generic type instantiation and arity checking.
pub(crate) mod generics;
/// Ghost and lemma function effect checking.
pub(crate) mod ghost_effects;
/// Expression type inference (`infer_expr`).
pub mod inference;
/// Type checking pipeline entry points.
mod pipeline;
/// Core type definitions (Type, TypeEnv, TypeError, TypedFile).
mod types;

// ---- Re-exports: maintain the exact public API ----

// From types module
pub use types::{Type, TypeEnv, TypeError, TypedFile};

// From checkers module
pub use checkers::{FrameChecker, PendingDecreaseCheck, TaintLabel};

// From domain module
pub use domain::{GeneratedTest, TableSmtObligation, TestGenerator, TestKind, TestableContract};

// From checks module (public API for pipeline)
pub use checks::collect_table_smt_obligations;

// Re-export checks/ helpers so domain/ can call them at crate scope.
pub(crate) use checks::{
    clauses_contract_fn, clauses_contract_fn_block, fn_or_contract_name_clauses,
    runtime_decl_clauses_params,
};

// From convert module (pub(crate) items accessed within crate)
pub(crate) use convert::parse_type_tokens;

// From inference module
pub(crate) use inference::*;

// From generics module (only used in tests)
#[cfg(test)]
pub(crate) use generics::{check_generic_instantiation, instantiate_builtin_generic, substitute};

// From ghost_effects module
pub(crate) use ghost_effects::{check_ghost_fn_effects, check_lemma_fn_effects};

// From pipeline module
pub use pipeline::{TypeChecker, type_check};

// Test-only re-exports: make checker types, domain types, and internal
// functions visible to the tests/ module via `use super::*;`.
#[cfg(test)]
pub(crate) use checkers::*;
#[cfg(test)]
pub(crate) use checks::*;
#[cfg(test)]
pub(crate) use domain::*;

#[cfg(test)]
mod tests;