crates.sage_ir.crate
9 anchors
| Anchor | Implementation | Tests |
|---|---|---|
| crates.sage_ir.crate (9) | 9 TODO | 9 TODO |
explicit_restrictions | TODO | TODO |
A language restriction is explicit at its semantic boundary. An
intentionally unsupported Rust construct states what is excluded, why Sage
excludes it, its user-visible impact, and the response at the responsible
phase. That response is normally a diagnostic or conservative incomplete
result; any temporary semantic approximation, such as | ||
identity_before_detail | TODO | TODO |
Semantic identity precedes semantic detail. A definition’s semantic identity is created and retained independently from its signature, members, fields, body, and other lazily computed facts. Symbol-bearing item definitions use their symbol; generic parameters, fields, and locals use their appropriate scoped identity family. Downstream semantic values refer to that identity rather than reconstructing it from those details. This is the pipeline-wide consequence of Symbols form the uniform semantic identity family. | ||
incremental_evidence | TODO | TODO |
Incremental guarantees are verified as executions and semantic reads, not timings. Evidence distinguishes a tracked function body which executed from a memoized request and records owned external-metadata reads separately. Independent scheduling order and elapsed time are excluded unless a specific ordering or count is itself the invariant. | ||
narrow_demands | TODO | TODO |
Demand follows the narrowest semantic boundary. Asking for one semantic product requests only the interfaces and metadata needed for that product. In particular, checking a caller may read a callee signature but never the callee body. This is the pipeline-wide consequence of Cross-item dependencies stop at semantic interfaces. | ||
reexecution_and_invalidation | TODO | TODO |
Reexecution and downstream invalidation are distinct. A coarse input change may cause a cheap producer or keyed lookup to execute again. When its semantic result is equal, backdating must stop the change before expensive consumers; the architecture does not claim that every unrelated edit prevents all upstream execution. | ||
represented_completeness | TODO | TODO |
Unrepresented source never becomes negative evidence. Published
symbols from an incomplete phase may support their own positive facts, but
omitted or unsupported source cannot justify a false proof, failed lookup,
or exhaustive ground | ||
restrictions_and_gaps | TODO | TODO |
Deliberate restrictions define Sage’s supported language contract and explain its limits. Temporary implementation gaps in otherwise supported Rust appear as TODO entries on the relevant specification anchors, with their limitations and evidence. Such gaps do not silently narrow the supported contract; RFDs record plans for closing them. | ||
semantic_query_boundaries | TODO | TODO |
Query boundaries follow stable semantic products. Each public tracked query has a semantic key and returns the narrowest independently reusable product at that key. Temporary algorithm state is kept inside its owning query rather than exposed merely to obtain finer-grained memoization. | ||
terminal_incompleteness | TODO | TODO |
Phase incompleteness is a terminal semantic outcome. A phase distinguishes a complete result from a conservative result limited by user error, unsupported functionality, unavailable facts, or an explicit resource bound. It never presents such a result as computation which merely needs more scheduling. This is the pipeline-wide consequence of Incompleteness is an explicit terminal outcome. | ||