List of all items

Structs

• ast::AnnotBool
• ast::DecisionBlock
• ast::FnDef
• ast::FnResolution
• ast::MatchArm
• ast::Module
• ast::SourceSpan
• ast::Spanned
• ast::TailCallData
• ast::TypeVariant
• ast::VerifyBlock
• ast::VerifyGiven
• ast::VerifyLaw
• bench::DiffReport
• bench::MetricDiff
• bench::manifest::ExpectedShape
• bench::manifest::Manifest
• bench::manifest::Tolerance
• bench::report::BackendInfo
• bench::report::BenchReport
• bench::report::HostInfo
• bench::report::IterationStats
• bench::report::ScenarioMetadata
• checker::CheckFinding
• checker::FindingSpan
• checker::ModuleCheckFindings
• checker::VerifyCaseResult
• checker::VerifyLawContext
• checker::VerifyResult
• codegen::CodegenContext
• codegen::ModuleInfo
• codegen::ProjectOutput
• codegen::recursion::ProofModeIssue
• codegen::rust::emit_ctx::EmitCtx
• config::CheckSuppression
• config::EffectPolicy
• config::ProjectConfig
• diagnostics::analyze::AnalyzeOptions
• diagnostics::context::ContextDecisionSummary
• diagnostics::context::ContextFnSummary
• diagnostics::context::ContextSummary
• diagnostics::context::ContextTypeSummary
• diagnostics::context::FileContext
• diagnostics::model::AnalysisReport
• diagnostics::model::AnnotatedRegion
• diagnostics::model::Diagnostic
• diagnostics::model::FormatViolation
• diagnostics::model::RelatedSpan
• diagnostics::model::Repair
• diagnostics::model::SourceLine
• diagnostics::model::Span
• diagnostics::model::Underline
• diagnostics::model::VerifyBlockResult
• diagnostics::model::VerifySummary
• diagnostics::why::DecisionSummary
• diagnostics::why::FnDetail
• diagnostics::why::WhySummary
• ir::AnalysisResult
• ir::BodyBindingPlan
• ir::BoolMatchShape
• ir::BufferBuildShape
• ir::DispatchArmPlan
• ir::DispatchDefaultPlan
• ir::DispatchTableShape
• ir::FnAnalysis
• ir::ForwardCallPlan
• ir::FusionSite
• ir::ListMatchShape
• ir::NeutralAllocPolicy
• ir::ThinBodyPlan
• ir::pipeline::FnCountChange
• ir::pipeline::NonTailEntry
• ir::pipeline::PassDiagnostic
• ir::pipeline::PipelineConfig
• ir::pipeline::PipelineResult
• lexer::Lexer
• lexer::Token
• nan_value::ArenaUsage
• nan_value::AverTypes
• nan_value::NanValue
• parser::Parser
• replay::runtime::EffectReplayState
• replay::session::EffectRecord
• replay::session::SessionRecording
• runtime_bench_cases::CoreBenchCase
• source::LoadedModule
• tail_check::NonTailRecursionWarning
• types::checker::TypeCheckResult
• types::checker::TypeError
• types::checker::TypeErrorSpan
• types::checker::effect_classification::EffectClassification
• types::checker::effect_lifting::LiftConfig
• types::checker::hostile_effects::HostileProfile
• value::FunctionValue
• verify_law::ContextualHelperLawHint
• verify_law::MissingHelperLawHint
• verify_law::NamedLawFunction
• verify_law::VerifyLawSpecRef
• verify_law::expand::ExpandedCase
• visibility::ExportedTypeDef
• visibility::ModuleExports
• visibility::ModuleTypeDef
• visibility::SymbolEntry
• visibility::SymbolRegistry
• vm::CallFrame
• vm::CodeStore
• vm::FnChunk
• vm::VM
• vm::VmBuiltinProfile
• vm::VmFunctionProfile
• vm::VmOpcodeProfile
• vm::VmProfileReport
• vm::VmReturnStats
• vm::runtime::TraceCoord

Enums

• ast::BinOp
• ast::DecisionImpact
• ast::Expr
• ast::FnBody
• ast::Literal
• ast::Pattern
• ast::Stmt
• ast::StrPart
• ast::TopLevel
• ast::TypeDef
• ast::VerifyGivenDomain
• ast::VerifyKind
• ast::types::Type
• bench::manifest::BenchTarget
• bench::manifest::ManifestError
• checker::VerifyCaseOutcome
• codegen::lean::VerifyEmitMode
• codegen::recursion::RecursionPlan
• config::IndependenceMode
• diagnostics::model::Severity
• diagnostics::why::Justification
• ir::BodyExprPlan
• ir::BodyPlan
• ir::BodyShape
• ir::BoolCompareOp
• ir::BoolSubjectPlan
• ir::CallPlan
• ir::ConsumerKind
• ir::DispatchBindingPlan
• ir::DispatchLiteral
• ir::ForwardArg
• ir::LeafOp
• ir::MatchDispatchPlan
• ir::SemanticConstructor
• ir::SemanticDispatchPattern
• ir::TailCallPlan
• ir::ThinKind
• ir::WrapperKind
• ir::pipeline::PassReport
• ir::pipeline::PipelineStage
• ir::pipeline::TypecheckMode
• lexer::LexerError
• lexer::TokenKind
• nan_value::AllocSpace
• nan_value::ArenaList
• nan_value::NanString
• parser::ParseError
• replay::json::JsonValue
• replay::runtime::EffectReplayMode
• replay::runtime::ReplayFailure
• replay::session::RecordedOutcome
• types::checker::effect_classification::EffectDimension
• types::checker::effect_classification::RuntimeType
• types::checker::effect_lifting::LiftError
• value::EnvFrame
• value::RuntimeError
• value::Value
• verify_law::expand::ExpansionMode
• visibility::ModuleTypeKind
• visibility::SymbolKind
• vm::VmError
• vm::runtime::VmExecutionMode

Traits

• ir::AllocPolicy
• ir::CallLowerCtx
• ir::ThinBodyCtx
• nan_value::ArenaTypes
• nan_value::FnValueName
• nan_value::MapLike
• nan_value::NanValueConvert

Functions

• ast_rewrite::pattern_binding_names
• ast_rewrite::rewrite_idents_scoped
• bench::diff
• bench::format_diff
• bench::report::format_human
• bench::run_scenario
• call_graph::direct_calls
• call_graph::find_recursive_fns
• call_graph::find_tco_groups
• call_graph::ordered_fn_components
• call_graph::recursive_callsite_counts
• call_graph::recursive_scc_ids
• call_graph::tailcall_scc_components
• checker::check_module_intent
• checker::check_module_intent_with_sigs
• checker::check_module_intent_with_sigs_in
• checker::collect_cse_warnings
• checker::collect_cse_warnings_in
• checker::collect_independence_warnings
• checker::collect_independence_warnings_in
• checker::collect_module_effects_warnings
• checker::collect_module_effects_warnings_in
• checker::collect_naming_warnings
• checker::collect_naming_warnings_in
• checker::collect_perf_warnings
• checker::collect_perf_warnings_in
• checker::collect_plain_cases_effectful_warnings
• checker::collect_plain_cases_effectful_warnings_in
• checker::collect_traversal_warnings_in
• checker::collect_verify_coverage_warnings
• checker::collect_verify_coverage_warnings_in
• checker::collect_verify_law_dependency_warnings
• checker::collect_verify_law_dependency_warnings_in
• checker::expr_to_str
• checker::index_decisions
• checker::merge_verify_blocks
• codegen::build_context
• codegen::common::entry_basename
• codegen::common::is_pure_fn
• codegen::common::is_recursive_product
• codegen::common::is_recursive_sum
• codegen::common::is_recursive_type_def
• codegen::common::type_def_name
• codegen::dafny::transpile
• codegen::lean::proof_mode_findings
• codegen::lean::proof_mode_issues
• codegen::lean::transpile
• codegen::lean::transpile_for_proof_mode
• codegen::lean::transpile_with_verify_mode
• codegen::recursion::detect::analyze_plans
• codegen::recursion::fuel_helper_name
• codegen::recursion::rewrite_recursive_calls_body
• codegen::recursion::rewrite_recursive_calls_expr
• codegen::rust::emit_ctx::expr_can_move
• codegen::rust::emit_ctx::expr_skip_clone
• codegen::rust::emit_ctx::is_copy_type
• codegen::rust::emit_ctx::should_borrow_param
• codegen::rust::transpile
• diagnostics::analyze::analyze_source
• diagnostics::context::build_context_for_items
• diagnostics::context::compute_memo_fns
• diagnostics::context::is_memo_safe_type
• diagnostics::context::render_context_md
• diagnostics::context::summarize
• diagnostics::factories::from_check_finding
• diagnostics::factories::from_type_error
• diagnostics::factories::needs_format_diagnostic
• diagnostics::factories::replay_effect_error_diagnostic
• diagnostics::factories::replay_output_mismatch_diagnostic
• diagnostics::factories::unused_binding_diagnostic
• diagnostics::factories::verify_mismatch_diagnostic
• diagnostics::factories::verify_runtime_error_diagnostic
• diagnostics::factories::verify_unexpected_err_diagnostic
• diagnostics::model::json_escape
• diagnostics::verify_run::run_verify_blocks
• diagnostics::verify_run::run_verify_blocks_with_loaded
• diagnostics::verify_run::run_verify_blocks_with_loaded_and_mode
• diagnostics::verify_run::run_verify_blocks_with_mode
• diagnostics::vm_verify::run_verify_for_items_vm
• diagnostics::vm_verify::run_verify_for_items_vm_with_loaded
• diagnostics::vm_verify::run_verify_for_items_vm_with_loaded_and_mode
• diagnostics::vm_verify::run_verify_for_items_vm_with_mode
• diagnostics::why::summarize
• effects::effect_satisfies
• format::try_format_source
• ir::alias::annotate_program_alias_slots
• ir::analyze
• ir::classify_body_expr_plan
• ir::classify_body_plan
• ir::classify_bool_match_shape
• ir::classify_bool_match_shape_from_patterns
• ir::classify_bool_subject_plan
• ir::classify_call_plan
• ir::classify_callee
• ir::classify_constructor_name
• ir::classify_dispatch_pattern
• ir::classify_dispatch_table_shape
• ir::classify_dispatch_table_shape_from_patterns
• ir::classify_forward_call_parts
• ir::classify_forward_call_plan
• ir::classify_forward_fn_body
• ir::classify_leaf_op
• ir::classify_list_match_shape
• ir::classify_list_match_shape_from_patterns
• ir::classify_match_dispatch_plan
• ir::classify_match_dispatch_plan_from_patterns
• ir::classify_tail_call_plan
• ir::classify_thin_body_plan
• ir::classify_thin_fn_def
• ir::compute_alloc_info
• ir::compute_buffer_build_sinks
• ir::count_alloc_sites_in_fn
• ir::count_alloc_sites_in_program
• ir::dump::dump_items
• ir::escape::run
• ir::expr_to_dotted_name
• ir::find_fusion_sites
• ir::is_builtin_namespace
• ir::last_use::annotate_program_last_use
• ir::lower_interpolation_pass
• ir::pipeline::buffer_build
• ir::pipeline::interp_lower
• ir::pipeline::last_use
• ir::pipeline::resolve
• ir::pipeline::run
• ir::pipeline::tco
• ir::pipeline::typecheck
• ir::rewrite_fusion_sites
• ir::run_buffer_build_pass
• ir::synthesize_buffered_variants
• ir::thin_body_plan_is_parent_thin_candidate
• ir::thin_kind_is_parent_thin_candidate
• ir::vars::collect_vars
• ir::vars::collect_vars_stmt
• ir::vars::pattern_bindings
• replay::entry::encode_entry_args
• replay::entry::parse_entry_call
• replay::entry::recording_stem
• replay::json::first_diff_path
• replay::json::format_json
• replay::json::json_to_string
• replay::json::json_to_value
• replay::json::json_values_to_values
• replay::json::parse_json
• replay::json::value_to_json
• replay::json::value_to_json_lossy
• replay::json::values_to_json
• replay::json::values_to_json_lossy
• replay::session::parse_session_recording
• replay::session::session_recording_from_json
• replay::session::session_recording_to_json
• replay::session::session_recording_to_string_pretty
• resolver::resolve_program
• services::all_effect_names
• services::args::call
• services::args::call_nv
• services::args::effects
• services::args::register
• services::args::register_nv
• services::console::call
• services::console::call_nv
• services::console::effects
• services::console::register
• services::console::register_nv
• services::disk::call
• services::disk::call_nv
• services::disk::effects
• services::disk::register
• services::disk::register_nv
• services::env::call
• services::env::call_nv
• services::env::effects
• services::env::register
• services::env::register_nv
• services::http::call
• services::http::call_nv
• services::http::effects
• services::http::register
• services::http::register_nv
• services::http_server::call
• services::http_server::call_with_runtime
• services::http_server::effects
• services::http_server::register
• services::http_server::register_nv
• services::random::call
• services::random::call_nv
• services::random::effects
• services::random::register
• services::random::register_nv
• services::tcp::call
• services::tcp::call_nv
• services::tcp::effects
• services::tcp::register
• services::tcp::register_nv
• services::terminal::call
• services::terminal::call_nv
• services::terminal::effects
• services::terminal::register
• services::terminal::register_nv
• services::time::call
• services::time::call_nv
• services::time::effects
• services::time::register
• services::time::register_nv
• source::canonicalize_path
• source::find_module_file
• source::load_module_tree
• source::load_module_tree_from_map
• source::parse_source
• source::require_module_declaration
• tail_check::collect_non_tail_recursion_warnings
• tail_check::collect_non_tail_recursion_warnings_with_sigs
• tco::transform_program
• tty_render::render_tty
• types::bool::call
• types::bool::call_nv
• types::bool::effects
• types::bool::register
• types::bool::register_nv
• types::branch_path::call_nv
• types::branch_path::register_nv
• types::byte::call
• types::byte::call_nv
• types::byte::effects
• types::byte::register
• types::byte::register_nv
• types::char::call
• types::char::call_nv
• types::char::effects
• types::char::register
• types::char::register_nv
• types::checker::effect_classification::classifications_for_proof_subset
• types::checker::effect_classification::classify
• types::checker::effect_classification::is_classified
• types::checker::effect_classification::oracle_signature
• types::checker::effect_lifting::lift_body
• types::checker::effect_lifting::lift_fn_def
• types::checker::effect_lifting::lift_fn_def_with_helpers
• types::checker::effect_lifting::lower_pure_question_bang_fn
• types::checker::effect_lifting::oracle_params_for_effects
• types::checker::effect_lifting::type_to_annotation
• types::checker::hostile_effects::hostile_profiles_for
• types::checker::hostile_values::boundary_exprs
• types::checker::hostile_values::boundary_values
• types::checker::run_type_check
• types::checker::run_type_check_full
• types::checker::run_type_check_with_base
• types::checker::run_type_check_with_loaded
• types::effect_event::register
• types::float::call
• types::float::call_nv
• types::float::effects
• types::float::register
• types::float::register_nv
• types::int::call
• types::int::call_nv
• types::int::effects
• types::int::register
• types::int::register_nv
• types::list::call
• types::list::call_nv
• types::list::effects
• types::list::register
• types::list::register_nv
• types::map::call
• types::map::call_nv
• types::map::effects
• types::map::register
• types::map::register_nv
• types::map::set_nv_owned
• types::option::call
• types::option::call_nv
• types::option::effects
• types::option::extra_members
• types::option::register
• types::parse_type_str
• types::parse_type_str_strict
• types::result::call
• types::result::call_nv
• types::result::effects
• types::result::extra_members
• types::result::register
• types::string::call
• types::string::call_nv
• types::string::effects
• types::string::register
• types::string::register_nv
• types::trace::register
• types::vector::call
• types::vector::call_nv
• types::vector::effects
• types::vector::register
• types::vector::register_nv
• types::vector::vec_set_nv_owned
• value::aver_display
• value::aver_repr
• value::callable_declared_effects
• value::hash_memo_args
• value::list_from_vec
• value::list_head
• value::list_len
• value::list_slice
• value::list_to_vec
• verify_law::canonical_spec_ref
• verify_law::canonical_spec_shape
• verify_law::collect_contextual_helper_law_hints
• verify_law::collect_missing_helper_law_hints
• verify_law::contextual_helper_law_message
• verify_law::declared_spec_ref
• verify_law::expand::expand_law_cases
• verify_law::law_calls_function
• verify_law::law_spec_ref
• verify_law::missing_helper_law_message
• verify_law::named_law_function
• visibility::collect_all_module_symbols
• visibility::collect_module_exports
• visibility::collect_module_types
• visibility::is_exposed
• visibility::member_key
• visibility::module_decl
• visibility::qualified_member_key
• visibility::qualified_name
• vm::compile_program
• vm::compile_program_with_loaded_modules
• vm::compile_program_with_modules
• vm::opcode::opcode_name
• vm::opcode::opcode_operand_width
• vm::register_service_types

Type Aliases

• ast::SourceLine
• ir::SemanticCallee
• ir::pipeline::AfterPassHook
• nan_value::Arena
• nan_value::ArenaEntry
• nan_value::ArenaSymbol
• nan_value::PersistentMap
• value::Env
• verify_law::FnSigMap

Constants

• diagnostics::model::SCHEMA_VERSION
• diagnostics::vm_verify::VERIFY_HOSTILE_MAX_CASES
• nan_value::ARENA_REF_BIT
• nan_value::IMM_FALSE
• nan_value::IMM_TRUE
• nan_value::IMM_UNIT
• nan_value::INT_INLINE_MAX
• nan_value::INT_INLINE_MIN
• nan_value::SYMBOL_BUILTIN
• nan_value::SYMBOL_FN
• nan_value::SYMBOL_NAMESPACE
• nan_value::SYMBOL_NULLARY_VARIANT
• nan_value::TAG_ERR
• nan_value::TAG_IMMEDIATE
• nan_value::TAG_INLINE_VARIANT
• nan_value::TAG_INT
• nan_value::TAG_LIST
• nan_value::TAG_MAP
• nan_value::TAG_NONE
• nan_value::TAG_OK
• nan_value::TAG_RECORD
• nan_value::TAG_SOME
• nan_value::TAG_STRING
• nan_value::TAG_SYMBOL
• nan_value::TAG_TUPLE
• nan_value::TAG_VARIANT
• nan_value::TAG_VECTOR
• nan_value::WRAP_ERR
• nan_value::WRAP_OK
• nan_value::WRAP_SOME
• runtime_bench_cases::CORE_BENCH_CASES
• services::args::DECLARED_EFFECTS
• services::console::DECLARED_EFFECTS
• services::disk::DECLARED_EFFECTS
• services::env::DECLARED_EFFECTS
• services::http::DECLARED_EFFECTS
• services::http_server::DECLARED_EFFECTS
• services::random::DECLARED_EFFECTS
• services::tcp::DECLARED_EFFECTS
• services::terminal::DECLARED_EFFECTS
• services::time::DECLARED_EFFECTS
• types::branch_path::TYPE_NAME
• types::effect_event::FIELD_ARGS
• types::effect_event::FIELD_METHOD
• types::effect_event::FIELD_PATH
• types::effect_event::TYPE_NAME
• types::trace::FIELD_EVENTS
• types::trace::TYPE_NAME
• vm::opcode::ADD
• vm::opcode::ADD_FLOAT
• vm::opcode::ADD_INT
• vm::opcode::BUFFER_APPEND_SEP_UNLESS_FIRST
• vm::opcode::BUFFER_APPEND_STR
• vm::opcode::BUFFER_FINALIZE
• vm::opcode::BUFFER_NEW
• vm::opcode::CALL_BUILTIN
• vm::opcode::CALL_BUILTIN_OWNED
• vm::opcode::CALL_KNOWN
• vm::opcode::CALL_KNOWN_OWNED
• vm::opcode::CALL_LEAF
• vm::opcode::CALL_PAR
• vm::opcode::CALL_VALUE
• vm::opcode::CONCAT
• vm::opcode::DIV
• vm::opcode::DIV_FLOAT
• vm::opcode::DUP
• vm::opcode::EQ
• vm::opcode::EQ_INT
• vm::opcode::EXTRACT_FIELD
• vm::opcode::EXTRACT_TUPLE_ITEM
• vm::opcode::GT
• vm::opcode::GT_FLOAT
• vm::opcode::GT_INT
• vm::opcode::JUMP
• vm::opcode::JUMP_IF_FALSE
• vm::opcode::LIST_CONS
• vm::opcode::LIST_HEAD_TAIL
• vm::opcode::LIST_LEN
• vm::opcode::LIST_NEW
• vm::opcode::LIST_NIL
• vm::opcode::LIST_PREPEND
• vm::opcode::LOAD_CONST
• vm::opcode::LOAD_FALSE
• vm::opcode::LOAD_GLOBAL
• vm::opcode::LOAD_LOCAL
• vm::opcode::LOAD_LOCAL_2
• vm::opcode::LOAD_LOCAL_CONST
• vm::opcode::LOAD_TRUE
• vm::opcode::LOAD_UNIT
• vm::opcode::LT
• vm::opcode::LT_FLOAT
• vm::opcode::LT_INT
• vm::opcode::MATCH_CONS
• vm::opcode::MATCH_DISPATCH
• vm::opcode::MATCH_DISPATCH_CONST
• vm::opcode::MATCH_FAIL
• vm::opcode::MATCH_INT_LITERAL
• vm::opcode::MATCH_NIL
• vm::opcode::MATCH_TAG
• vm::opcode::MATCH_TUPLE
• vm::opcode::MATCH_UNWRAP
• vm::opcode::MATCH_VARIANT
• vm::opcode::MOD
• vm::opcode::MOVE_LOCAL
• vm::opcode::MUL
• vm::opcode::MUL_FLOAT
• vm::opcode::MUL_INT
• vm::opcode::NEG
• vm::opcode::NOP
• vm::opcode::NOT
• vm::opcode::POP
• vm::opcode::PROPAGATE_ERR
• vm::opcode::RECORD_GET
• vm::opcode::RECORD_GET_NAMED
• vm::opcode::RECORD_NEW
• vm::opcode::RECORD_UPDATE
• vm::opcode::RETURN
• vm::opcode::STORE_GLOBAL
• vm::opcode::STORE_LOCAL
• vm::opcode::SUB
• vm::opcode::SUB_FLOAT
• vm::opcode::SUB_INT
• vm::opcode::TAIL_CALL_KNOWN
• vm::opcode::TAIL_CALL_SELF
• vm::opcode::TAIL_CALL_SELF_THIN
• vm::opcode::TUPLE_NEW
• vm::opcode::UNWRAP_OR
• vm::opcode::UNWRAP_RESULT_OR
• vm::opcode::VARIANT_NEW
• vm::opcode::VECTOR_GET
• vm::opcode::VECTOR_GET_OR
• vm::opcode::VECTOR_SET
• vm::opcode::VECTOR_SET_OR_KEEP
• vm::opcode::WRAP