Module features 

Feature-specific code generation for all 50 verification features. Feature-specific Rust code generation for Assura’s 50 verification features.

Each feature maps to a codegen strategy:

• debug_assert!: Runtime checks from contract clauses
• Newtype wrappers: Type-safe wrappers (region, taint)
• Rust attributes: cfg, unsafe, visibility markers
• Documentation: Contract metadata as doc comments

The coverage script greps for feature-specific identifiers in this crate. Each function here uses the canonical identifier for its feature.

Functions

compile_time_allocator

compile_time_axiom

CORE.4: Axiomatic definition compile_error!.

compile_time_behavioral_equiv

compile_time_binary_format

compile_time_bit_level

FMT.2: Bit-level width sum const assert.

compile_time_checksum

compile_time_circular

MEM.4: Circular buffer power-of-two const assert.

compile_time_codec_registry

compile_time_complexity_bound

compile_time_constant_time

SEC.3: Constant-time compile_error!.

compile_time_crash_recovery

compile_time_crypto

SEC.5: Crypto conformance compile_error!.

compile_time_deadline

compile_time_dependent_types

SEC.5: Dependent type / information-flow label enforcement.

compile_time_determinism

CONC.3: Determinism compile_error!.

compile_time_error_propagation

compile_time_feature_flag

compile_time_fixed_width

compile_time_frame

CORE.3: Frame conditions.

compile_time_ghost_erasure

CORE.1: Ghost code erasure.

compile_time_incremental

compile_time_interface

compile_time_lemma

CORE.2: Lemma erasure compile_error!.

compile_time_liveness

compile_time_lock_order

compile_time_monotonic

STOR.5: Monotonic wrapper type.

compile_time_multi_pass

compile_time_mvcc

compile_time_numerical_precision

compile_time_opaque

compile_time_page_cache

STOR.2: Page cache alignment const assert.

compile_time_platform

PLAT.1: Platform abstraction cfg gate.

compile_time_precomputed_table

compile_time_prophecy

compile_time_protocol_grammar

compile_time_reentrancy

compile_time_region

compile_time_resource_limit

compile_time_rollback

STOR.4: Rollback #[must_use] handle.

compile_time_scoped_invariant

compile_time_shared_memory

compile_time_storage_failure

STOR.6: Storage failure #[must_use].

compile_time_string_encoding

FMT.3: String encoding compile_error!.

compile_time_structural

compile_time_taint

SEC.1: Taint tracking compile_error!.

compile_time_test_gen

compile_time_trigger

compile_time_trigger_pattern

CORE.5: Trigger pattern validation.

compile_time_unsafe_escape

compile_time_weak_memory

compile_time_zeroize

SEC.4: Secure erasure compile_error!.

generate_all_feature_clauses

Generate all feature-specific annotations for a set of clauses. Called from contract and function codegen paths.

generate_allocator_check

generate_axiomatic_definition

generate_behavioral_equiv_test

TEST.2: Generate behavioral_equivalence test skeleton.

generate_binary_format_check

generate_bit_level_check

generate_callback_reentrancy_guard

CONC.2: Generate callback re-entrancy guard (custom, not a simple assert).

generate_checksum_check

generate_circular_buffer_check

generate_complexity_bound

PERF.2: Complexity bound annotation.

generate_constant_time_annotation

SEC.3: Generate constant-time execution annotation.

generate_crash_recovery_check

generate_crypto_conformance_check

generate_deadline_check

CONC.5: Temporal deadline annotation.

generate_deterministic_annotation

generate_error_propagation_check

generate_feature_clause

Generate feature-specific codegen for a single clause.

generate_feature_flag

PLAT.2: Feature flag annotation.

generate_ghost_compile_check

CORE.1: Generate compile-time ghost erasure check.

generate_incremental_contract

MISC.1: Generate incremental_contract version annotation.

generate_liveness_check

CORE.8: Generate liveness contract check.

generate_lock_order_annotation

CONC.4: Lock ordering annotation.

generate_monotonic_check

generate_multi_pass_refinement

TEST.3: Generate multi_pass_refinement check.

generate_mvcc_check

generate_numerical_precision_check

generate_opaque_function

generate_page_cache_check

generate_platform_abstraction

PLAT.1: Platform abstraction annotation.

generate_precomputed_table_check

generate_protocol_grammar_check

generate_region_annotation

generate_resource_limit_check

generate_rollback_check

generate_scoped_invariant

MISC.2: Generate scoped_invariant suspension marker.

generate_storage_failure_check

generate_string_encoding_check

generate_structural_invariant

generate_unsafe_escape

PERF.1: Unsafe escape annotation.