Introduction
1.
Introduction
2.
Language Subsetting
3.
Terminology
4.
User's Guide
❱
4.1.
Inspecting Compiler Results
4.2.
Checking rustc Conformance
4.3.
Exploring the Design
4.4.
Worked examples
❱
4.4.1.
Struct signature
4.4.2.
Function body and field access
4.4.3.
Macro-generated struct
4.4.4.
A direct trait obligation
4.4.5.
A nested trait proof
4.4.6.
An external trait method call
4.4.7.
An oracle-checked method body
Design
5.
Overview
❱
5.1.
Meta
❱
5.1.1.
Book Structure and Rendering
5.1.2.
The .sage Language
5.1.3.
Anchors and Evidence
5.1.4.
Architectural Contracts
5.1.5.
Reviewing Implementations and Tests
5.1.6.
Validation Practices
5.2.
Tenets
5.3.
Anchors
❱
5.3.1.
crates
❱
5.3.1.1.
sage_inspector
❱
5.3.1.1.1.
inspection
❱
5.3.1.1.1.1.
balanced_traces
5.3.1.1.1.2.
canonical_ownership
5.3.1.1.1.3.
derive_reflection
5.3.1.1.1.4.
detail_free_index
5.3.1.1.1.5.
deterministic_trace
5.3.1.1.1.6.
durable_navigation
5.3.1.1.1.7.
generic_browser
5.3.1.1.1.8.
owned_reflection
5.3.1.1.1.9.
product_availability
5.3.1.1.1.10.
revision_and_demand
5.3.1.1.1.11.
semantic_phase_boundary
5.3.1.1.1.12.
source_evidence
5.3.1.1.1.13.
typed_service
5.3.1.1.1.14.
unknown_work
5.3.1.1.1.15.
workspace_actor
5.3.1.2.
sage_ir
❱
5.3.1.2.1.
checking
❱
5.3.1.2.1.1.
body
❱
5.3.1.2.1.1.1.
elaboration
5.3.1.2.1.1.2.
expected_types
5.3.1.2.1.1.3.
interface_dependencies
5.3.1.2.1.1.4.
isolated_completion
5.3.1.2.1.1.5.
operator_calls
5.3.1.2.1.2.
identity_minting
5.3.1.2.1.3.
owned_products
5.3.1.2.1.4.
signature
❱
5.3.1.2.1.4.1.
body_independence
5.3.1.2.1.4.2.
narrow_detail
5.3.1.2.1.4.3.
owner_binder
5.3.1.2.1.4.4.
storage
5.3.1.2.1.5.
symbol_keyed_interfaces
5.3.1.2.2.
crate
❱
5.3.1.2.2.1.
explicit_restrictions
5.3.1.2.2.2.
identity_before_detail
5.3.1.2.2.3.
incremental_evidence
5.3.1.2.2.4.
narrow_demands
5.3.1.2.2.5.
reexecution_and_invalidation
5.3.1.2.2.6.
represented_completeness
5.3.1.2.2.7.
restrictions_and_gaps
5.3.1.2.2.8.
semantic_query_boundaries
5.3.1.2.2.9.
terminal_incompleteness
5.3.1.2.3.
inference
❱
5.3.1.2.3.1.
atomic_checking
5.3.1.2.3.2.
body_local_quiescence
5.3.1.2.3.3.
canonical_boundary
5.3.1.2.3.4.
completed_body_boundary
5.3.1.2.3.5.
numeric_domains
5.3.1.2.3.6.
subtyping_and_coercion
5.3.1.2.3.7.
terminal_obligations
5.3.1.2.3.8.
transaction_isolation
5.3.1.2.4.
metadata
❱
5.3.1.2.4.1.
explicit_incompleteness
5.3.1.2.4.2.
keyed_reuse
5.3.1.2.4.3.
product_boundaries
5.3.1.2.4.4.
provider_authority
5.3.1.2.5.
modules
❱
5.3.1.2.5.1.
expand
❱
5.3.1.2.5.1.1.
completeness
5.3.1.2.5.1.2.
dependencies
5.3.1.2.5.1.3.
direct_members
5.3.1.2.5.1.4.
recursion_and_fixpoint
5.3.1.2.5.2.
parse
❱
5.3.1.2.5.2.1.
dependencies
5.3.1.2.5.2.2.
detail_firewall
5.3.1.2.5.2.3.
recovery_completeness
5.3.1.2.5.2.4.
syntax_identities
5.3.1.2.6.
resolution
❱
5.3.1.2.6.1.
lookup
❱
5.3.1.2.6.1.1.
completeness
5.3.1.2.6.1.2.
dependencies
5.3.1.2.6.1.3.
expansion_import_ambiguity
5.3.1.2.6.1.4.
identity_only
5.3.1.2.6.1.5.
precedence
5.3.1.2.7.
solver
❱
5.3.1.2.7.1.
alternative_isolation
5.3.1.2.7.2.
bounded_completeness
5.3.1.2.7.3.
candidate_completeness
5.3.1.2.7.4.
canonical_cycles
5.3.1.2.7.5.
canonical_outputs
5.3.1.2.7.6.
local_index_firewall
5.3.1.2.7.7.
normalization_demand
5.3.1.2.7.8.
schedule_independence
5.3.1.2.7.9.
shared_final_result
5.3.1.2.8.
symbols
❱
5.3.1.2.8.1.
associated_identity
5.3.1.2.8.2.
associated_interfaces
5.3.1.2.8.3.
body_interfaces
5.3.1.2.8.4.
definition_identity
5.3.1.2.8.5.
external_fact_queries
5.3.1.2.8.6.
external_identity
5.3.1.2.8.7.
kind_wrappers
5.3.1.2.8.8.
local_identity
5.3.1.2.9.
types
❱
5.3.1.2.9.1.
aliases
❱
5.3.1.2.9.1.1.
identity
5.3.1.2.9.1.2.
revelation
5.3.1.2.9.2.
binder
❱
5.3.1.2.9.2.1.
owner_parameters
5.3.1.2.9.3.
body
❱
5.3.1.2.9.3.1.
await
5.3.1.2.9.3.2.
closures
5.3.1.2.9.3.3.
conditional_patterns
5.3.1.2.9.3.4.
coroutines
5.3.1.2.9.3.5.
diagnosed_recovery
5.3.1.2.9.3.6.
elaborated
5.3.1.2.9.3.7.
for_iteration
5.3.1.2.9.3.8.
indexing
5.3.1.2.9.3.9.
macro_expansion
5.3.1.2.9.3.10.
no_inference
5.3.1.2.9.3.11.
resolved_references
5.3.1.2.9.3.12.
try_residual
5.3.1.2.9.3.13.
typed_provenance
5.3.1.2.9.4.
calls
❱
5.3.1.2.9.4.1.
dispatch_families
5.3.1.2.9.4.2.
selected_semantics
5.3.1.2.9.5.
lifetimes
❱
5.3.1.2.9.5.1.
dummy
5.3.1.2.9.5.2.
unchecked_borrows
5.3.1.2.9.6.
operators
❱
5.3.1.2.9.6.1.
lazy_control_flow
5.3.1.2.9.6.2.
trait_calls
5.3.1.2.9.7.
scoped_identities
5.3.1.2.9.8.
spans
❱
5.3.1.2.9.8.1.
generated_identity
5.3.1.2.9.8.2.
item_origin
5.3.1.2.9.8.3.
offset_reuse
5.3.1.2.9.8.4.
relative_composition
5.3.1.3.
sage_oracle_harness
❱
5.3.1.3.1.
crate
❱
5.3.1.3.1.1.
deterministic_emission
5.3.1.3.1.2.
exact_comparison
5.3.1.3.1.3.
fixed_projection
5.3.1.3.1.4.
independent_coverage
5.3.1.4.
sage_stash
❱
5.3.1.4.1.
storage
❱
5.3.1.4.1.1.
handle_ownership
5.3.1.4.1.2.
immutable_entries
5.3.1.4.1.3.
query_value
5.3.1.4.1.4.
rooted_equality
5.3.1.4.1.5.
typed_interning
5.3.1.5.
sage_test_harness
❱
5.3.1.5.1.
compile_tests
❱
5.3.1.5.1.1.
annotation_validation
5.3.1.5.1.2.
blessing_gate
5.3.1.5.1.3.
callsite_updates
5.3.1.5.1.4.
checking_scope
5.3.1.5.1.5.
compiler_conditions
5.3.1.5.1.6.
completed_types
5.3.1.5.1.7.
coordinates
5.3.1.5.1.8.
dependencies
5.3.1.5.1.9.
diagnostic_counts
5.3.1.5.1.10.
diagnostic_locations
5.3.1.5.1.11.
edition
5.3.1.5.1.12.
fixtures
5.3.1.5.1.13.
grouped_observations
5.3.1.5.1.14.
invocation
5.3.1.5.1.15.
production_execution
5.3.1.5.1.16.
project_isolation
5.3.1.5.1.17.
query_capture
5.3.1.5.1.18.
query_projection
5.3.1.5.1.19.
rendering
5.3.1.5.1.20.
resolved_symbols
5.3.1.5.1.21.
review_visibility
5.3.1.5.1.22.
rustc_execution
5.3.1.5.1.23.
rustc_lints
5.3.1.5.1.24.
starting_expressions
5.3.1.5.1.25.
target_line
5.3.2.
meta
❱
5.3.2.1.
anchors
❱
5.3.2.1.1.
anchor_pages
5.3.2.1.2.
book_explorer
5.3.2.1.3.
canonical_sources
5.3.2.1.4.
content
❱
5.3.2.1.4.1.
blocks
5.3.2.1.4.2.
explicit_end
5.3.2.1.4.3.
heading
5.3.2.1.4.4.
literal_syntax
5.3.2.1.4.5.
next_anchor
5.3.2.1.4.6.
source_end
5.3.2.1.4.7.
unmatched_end
5.3.2.1.5.
context_navigation
5.3.2.1.6.
evidence_status
5.3.2.1.7.
explorer_navigation
5.3.2.1.8.
implementation_coverage
5.3.2.1.9.
implementation_references
5.3.2.1.10.
placeholder_status
5.3.2.1.11.
point_excerpts
5.3.2.1.12.
region_balance
5.3.2.1.13.
region_excerpts
5.3.2.1.14.
test_coverage
5.3.2.1.15.
test_references
5.3.2.1.16.
unique_names
5.3.2.2.
book
❱
5.3.2.2.1.
anchor_moves
5.3.2.2.2.
authority
5.3.2.2.3.
browser_delivery
5.3.2.2.4.
browser_dependencies
5.3.2.2.5.
browser_rust_source
5.3.2.2.6.
browser_search
5.3.2.2.7.
browser_serve
5.3.2.2.8.
browser_structure
5.3.2.2.9.
chapter_names
5.3.2.2.10.
crate_ownership
5.3.2.2.11.
crates_landing
5.3.2.2.12.
entity_links
5.3.2.2.13.
index_groups
5.3.2.2.14.
index_namespace_pages
5.3.2.2.15.
index_rows
5.3.2.2.16.
index_status
5.3.2.2.17.
rfd_changes
5.3.2.2.18.
sage_chapters
5.3.2.2.19.
self_description
5.3.2.2.20.
shared_model
5.3.2.2.21.
source_roles
5.3.2.3.
contracts
❱
5.3.2.3.1.
cache_invocations
5.3.2.3.2.
correspondence
5.3.2.3.3.
observation_coverage
5.3.2.3.4.
validated_session
5.3.2.4.
language
❱
5.3.2.4.1.
calls
❱
5.3.2.4.1.1.
declared
5.3.2.4.1.2.
forbidden
5.3.2.4.2.
classes
❱
5.3.2.4.2.1.
abstract_complete
5.3.2.4.2.2.
override_signature
5.3.2.4.2.3.
single_inheritance
5.3.2.4.3.
contexts
❱
5.3.2.4.3.1.
inheritance
5.3.2.4.4.
envelopes
❱
5.3.2.4.4.1.
class_calls
5.3.2.4.4.2.
creates
5.3.2.4.4.3.
direct_calls
5.3.2.4.4.4.
leaf
5.3.2.4.4.5.
permissions
5.3.2.4.4.6.
reads
5.3.2.4.4.7.
receiver_calls
5.3.2.4.5.
fields
❱
5.3.2.4.5.1.
context_state
5.3.2.4.5.2.
kinds
5.3.2.4.6.
methods
❱
5.3.2.4.6.1.
kinds
5.3.2.4.6.2.
prose
5.3.2.4.7.
model
❱
5.3.2.4.7.1.
forbidden_paths
5.3.2.4.7.2.
inherited_prohibitions
5.3.2.4.7.3.
virtual_dispatch
5.3.2.4.8.
types
❱
5.3.2.4.8.1.
argument_arity
5.3.2.4.8.2.
declaration_prose
5.3.2.4.8.3.
enum_variants
5.3.2.4.8.4.
field_prose
5.3.2.4.8.5.
generic_parameters
5.3.2.4.8.6.
member_commas
5.3.2.4.8.7.
name_resolution
5.3.2.4.8.8.
opaque_representation
5.3.2.4.8.9.
prelude
5.3.2.4.8.10.
qualified_names
5.3.2.4.8.11.
recursive_values
5.3.2.4.8.12.
struct_fields
5.3.2.4.8.13.
tuples
5.3.2.4.8.14.
type_expressions
5.3.2.4.8.15.
unique_fields
5.3.2.4.8.16.
unique_parameters
5.3.2.4.8.17.
unique_variants
5.3.2.4.8.18.
unknown_names
5.3.2.4.8.19.
variant_prose
5.3.2.5.
reviews
❱
5.3.2.5.1.
claim_text
5.3.2.5.2.
complete_test_set
5.3.2.5.3.
decisions
5.3.2.5.4.
fragment_associations
5.3.2.5.5.
fragment_format
5.3.2.5.6.
fragment_freshness
5.3.2.5.7.
gate
5.3.2.5.8.
input_format
5.3.2.5.9.
input_fragments
5.3.2.5.10.
output_format
5.3.2.5.11.
preparation
5.3.2.5.12.
record_required
5.3.2.5.13.
recorded_reads
5.3.2.5.14.
recording
5.3.2.5.15.
review_delegation
5.3.2.5.16.
review_diagnostics
5.3.2.5.17.
review_instructions
5.3.2.5.18.
review_scope
5.3.2.5.19.
selector_claim
5.3.2.5.20.
selector_line_range
5.3.2.5.21.
selector_test
5.3.2.5.22.
selector_whole_file
5.3.2.5.23.
source_representation
5.3.2.5.24.
staleness
5.3.2.5.25.
summary_format
5.3.2.5.26.
test_source
5.3.2.5.27.
validation_layout
5.3.2.6.
validation
❱
5.3.2.6.1.
claim_specific_evidence
5.3.2.6.2.
independent_inspection
5.3.2.6.3.
review_packets
5.4.
Crates
❱
5.4.1.
rust_ref
5.4.2.
sage
❱
5.4.2.1.
driver
5.4.3.
sage_emit
❱
5.4.3.1.
emission
5.4.4.
sage_host
❱
5.4.4.1.
driver
5.4.5.
sage_inspector
❱
5.4.5.1.
inspection
5.4.5.2.
Semantic Inspector
5.4.6.
sage_ir
❱
5.4.6.1.
checking
5.4.6.2.
inference
5.4.6.3.
metadata
5.4.6.4.
modules
5.4.6.5.
resolution
5.4.6.6.
solver
5.4.6.7.
symbols
5.4.6.8.
types
5.4.6.9.
Architecture
5.4.6.10.
Body Checking and Typed-IR Elaboration
5.4.6.11.
Shared Checking Design
5.4.6.12.
Module and Macro Expansion
5.4.6.13.
Incrementality and Query Boundaries
5.4.6.14.
Type Inference
5.4.6.15.
External Metadata
5.4.6.16.
Parsing and Stable Symbol Creation
5.4.6.17.
Rust Compilation Pipeline
5.4.6.18.
Representations and Infrastructure
5.4.6.19.
Name Resolution
5.4.6.20.
Signature Checking
5.4.6.21.
Trait Solver Design
5.4.6.22.
Spans (`span.rs`)
5.4.6.23.
Semantic Subsystems
5.4.6.24.
Symbols and Semantic Identity
5.4.6.25.
Typed IR
5.4.7.
sage_macros_from_impls
5.4.8.
sage_meta
❱
5.4.8.1.
language
5.4.9.
sage_oracle
❱
5.4.9.1.
oracle
5.4.10.
sage_oracle_harness
❱
5.4.10.1.
Oracle Test Harness
5.4.11.
sage_reflect
❱
5.4.11.1.
reflection
5.4.12.
sage_reflect_derive
5.4.13.
sage_rustc_bridge
❱
5.4.13.1.
provider
5.4.14.
sage_stash
❱
5.4.14.1.
storage
5.4.14.2.
Stash (`sage-stash`)
5.4.15.
sage_stash_macros
5.4.16.
sage_test_harness
❱
5.4.16.1.
Inline Compilation Tests
5.4.17.
xtask
5.5.
RFDs
❱
5.5.1.
RFD template
❱
5.5.1.1.
Implementation plan and status
5.5.2.
Draft
❱
5.5.2.1.
Inline Compilation Tests
❱
5.5.2.1.1.
Implementation plan and status
5.5.2.2.
Trait Impl Candidate Discovery
❱
5.5.2.2.1.
Implementation plan and status
5.5.2.3.
Trait Solver Cycle Semantics
❱
5.5.2.3.1.
Implementation plan and status
5.5.2.4.
Trait Solver Scheduling and Fairness
❱
5.5.2.4.1.
Implementation plan and status
5.5.2.5.
Incremental Trait Results
❱
5.5.2.5.1.
Implementation plan and status
5.5.3.
Accepted
❱
5.5.3.1.
Sage Contracts and Walkthroughs
❱
5.5.3.1.1.
Implementation plan and status
5.5.3.2.
Semantic Inspector
❱
5.5.3.2.1.
JSON protocol
5.5.3.2.2.
Web application walkthrough
5.5.3.2.3.
Implementation plan and status
5.5.3.3.
Async Type Checker
❱
5.5.3.3.1.
Implementation plan and status
5.5.3.4.
Resolve at Position
❱
5.5.3.4.1.
Implementation plan and status
5.5.3.5.
Stash Safety
❱
5.5.3.5.1.
Implementation plan and status
5.5.3.6.
Faster Collision Chains
❱
5.5.3.6.1.
Implementation plan and status
5.5.3.7.
Symbol-Level Signature Queries
❱
5.5.3.7.1.
Implementation plan and status
5.5.3.8.
Numeric Inference Domains and Binary Operator Typing
❱
5.5.3.8.1.
Implementation plan and status
5.5.3.9.
Trait System
❱
5.5.3.9.1.
Implementation plan and status
5.5.3.10.
Trait Solving
❱
5.5.3.10.1.
Solving implementation sketch
5.5.3.10.2.
Whiteboard implementation sketch
5.5.3.10.3.
Implementation plan and status
5.5.3.11.
Method Resolution
❱
5.5.3.11.1.
Implementation plan and status
5.5.3.12.
Typed IR Elaboration
❱
5.5.3.12.1.
Implementation plan and status
5.5.4.
Completed
❱
5.5.4.1.
Phase-Oriented, Auditable Architecture Guide
❱
5.5.4.1.1.
Proposed phase chapter shape
5.5.4.1.2.
Implementation plan and status
5.5.4.2.
Associated Type Normalization for Parse::next
❱
5.5.4.2.1.
Implementation plan and status
5.5.4.3.
Initial Setup
❱
5.5.4.3.1.
Implementation plan and status
5.5.4.4.
Relative Span Model
❱
5.5.4.4.1.
Implementation plan and status
5.5.4.5.
Module sym tree
❱
5.5.4.5.1.
Implementation plan and status
5.5.4.6.
Macro Expansion as Tracked Query
❱
5.5.4.6.1.
Implementation plan and status
5.5.4.7.
Tuple Struct Constructors
❱
5.5.4.7.1.
Implementation plan and status
5.5.4.8.
Stash Hash-Consing
❱
5.5.4.8.1.
Implementation plan and status
5.5.4.9.
Stash-allocated MEM-map
❱
5.5.4.9.1.
Implementation plan and status
5.5.4.10.
Type Signatures
❱
5.5.4.10.1.
Implementation plan and status
5.5.4.11.
Generic Params as Symbols
❱
5.5.4.11.1.
Implementation plan and status
5.5.4.12.
Per-Kind Symbol Data
❱
5.5.4.12.1.
Implementation plan and status
5.5.4.13.
Diagnostics Rendering
❱
5.5.4.13.1.
Implementation plan and status
5.5.4.14.
Error Sentinel Type
❱
5.5.4.14.1.
Implementation plan and status
5.5.4.15.
IR Reshape
❱
5.5.4.15.1.
Implementation plan and status
5.5.4.16.
Enum Variant Symbols
❱
5.5.4.16.1.
Implementation plan and status
5.5.4.17.
Oracle Test Framework
❱
5.5.4.17.1.
Implementation plan and status
5.5.4.18.
Test Harness External Crates
❱
5.5.4.18.1.
Implementation plan and status
5.5.4.19.
Type Inference
❱
5.5.4.19.1.
Implementation plan and status
5.5.4.20.
Concurrent Type Checking
❱
5.5.4.20.1.
Implementation plan and status
5.5.4.21.
Parsing
❱
5.5.4.21.1.
Implementation plan and status
5.5.5.
Architectural Foundations
❱
5.5.5.1.
Record Maintenance
5.5.6.
Implementation Sequencing
❱
5.5.6.1.
Mini-redis Slices
5.5.6.2.
Deviation History
5.5.6.3.
Coverage History
Research
6.
Research
❱
6.1.
tree-sitter-rust Grammar Reference
6.2.
rustc Binary Operator Typing and Lowering
6.3.
rustc Subtyping and Coercions
6.4.
rustc Macro Expansion Ordering
6.5.
rustc macro_rules
6.6.
rustc Name Resolution
6.7.
rustc Opaque Types and the New Trait Solver
6.8.
Trait Solver Search
Contributing
7.
Maintaining this book
Light
Rust
Coal
Navy
Ayu
Symposiun AGentic Environment (SAGE)
Completed RFDs
RFDs that have been implemented.