# §8. Decision record > Sema language specification — §8 Decision record. > Generated from `docs/LANGUAGE.md` §8. This is the normative specification; for a guided tour see the Language and Neurosymbolic sections. | # | Decision | Rationale (evidence) | Rejected alternatives | |---|---|---|---| | D129 | **Certified totality on the exact fragment** (§3.6): `ensure total` in a def's signature preamble claims "terminates and yields a value of the return type on every input satisfying the `require` clauses" — `require` clauses are domain refinements. No new keyword: contracts are the claim vocabulary, following `ensure semantics(...)` as the second interpreted clause. Verified by `sema check` AND at module registration (parity, fail-closed): an unprovable claim is a load error; a claim executing from an unverified path (REPL, live patch) is a typed `ContractViolation`; a hot-swap drops the module's verified status (a sibling's proof may depend on the patched body); a patch may not claim totality. The v1 fragment is exact arithmetic: exact-typed signatures (arbitrary-precision `int`, `bool`, `str`, exact collections, recursively-exact structs/enums; floats excluded — non-finite results raise), explicit `!{}` row, no `while`, bounded `loop until`, provably finite iterables, no recursion, callees restricted to claiming defs + exact-fragment `equation`s + a curated builtin whitelist. Partial primitives discharge against preamble `require` facts by normalized AST equality over never-assigned names (`//`/`%` nonzero, `**`/shifts nonnegative, sequence indexing bounds, dict membership); whitelisted mutators are fact-monotone (`append` grows `len`; typed-key dict insertion only adds keys). `/` stays rejected even on ints (exact-rational-then-`f64` rounding can raise). Body-position claims, `total`-named bindings in scope, and claims on `simulate`/`stream`/ported defs are loud errors. `sema doc` renders the **Total** badge only after re-running the verifier. Target spec: termination measures for recursion, exact `QQ` division under facts, float totality via interval analysis, Lean-certified escape hatches. | Koka's `total` ≠ `pure` distinction is the load-bearing tier for a mathematical language, and Sema's `!{}` is only the `pure` analogue (divergence and typed errors remain); certifying the decidable exact fragment — where arbitrary-precision integers make `+`/`-`/`*` genuinely total — turns "mathematical function" from prose into a checked, fail-closed claim with check/run parity, mirroring the policy-examples precedent (§5.8). Explicitly NOT claimed, stated in §3.6: `ResourceLimit`/memory exhaustion (operational faults, as in every proof assistant's extracted code), `ensure` postcondition soundness (runtime-checked), dynamic type errors (the type checker's dimension). | A `total def` keyword modifier (grows the modifier zoo, ripples through lexer/tree-sitter/TextMate/LSP, and duplicates the contract vocabulary); totality-by-construct for `equation` (false — CAS/iterative kernels carry typed non-convergence outcomes; equations verify transitively against the exact math fragment instead); textual guard matching (unsound under aliasing/mutation — normalized AST facts over never-assigned names only); silent totality inference (a refactor could lose the property without breaking anything; claims must be explicit and checked); redefining `!{}` as total (breaks every pure-but-looping def; the tiers are orthogonal). | | D128 | Supervise/heal honesty slice (§5.11): `heal budget=N` is enforced — at most N acceptance-gauntlet attempts per supervise scope (previously hardcoded to one); `restart window=`, `heal window=`, and `heal scope=` stay recorded-only and `sema check` warns on each ("recorded in the journal but not enforced yet"); `lane`/`enter` are removed from the def-body directive whitelist (they were inert vocabulary — the generic unrecognized-directive warning now covers them; `lane` remains legitimate only inside `worker` profiles, §5.17) and `rollout` outside a `heal` block gets a targeted warning; acceptance gates are ordinary user predicates journaled per gate (`decision:heal.gate` `result:pass\|fail\|error`) and the previously documented gate builtins (`passes`/`replay`/`pre_patch_assure`/`new_obligations`/`failing_trace`/`monitors.conforming_after_burnin`) are re-labeled **target spec** — they never existed, so the old flagship example errored every gate and silently self-rejected; the escalation ladder is documented in its real order (restart → heal gauntlet → fallback, with the fallback value journaled and **discarded** — scope recovery, not a return value); rollout stages remain journal-recorded observations (`decision:heal.rollout`); DAP breakpoints on supervise config-clause lines (`restart`/`fallback`/`on_error`) and inside heal bodies now verify **false** with an honest reason — those lines can never fire because config clauses are split out before the attempt loop and heal gates evaluate outside the per-statement hook. | The shipped §5.11 example NameError'd all four gates, so every heal self-rejected while reading as if a proof gauntlet ran — fictional builtins laundering an unimplemented design as a working one; honesty demands enforced-vs-recorded be legible in the checker, the journal, and the debugger (BRIEF §3.8 "never silent"). | Implementing the gate builtins now (requires the frozen-oracle assure snapshot + a replay harness — ROADMAP Phase 2, D14 scope); keeping `lane`/`enter` silently whitelisted (inert no-ops in def bodies); enforcing `window=`/`scope=` prematurely (no wall-clock policy for deterministic runs yet); letting dead-clause breakpoints verify true (a debugger that lies). | | D127 | Effect rows are an **open vocabulary** with a checked call surface (§3.6): declaring any capability (`!{payments.read}`, `!{mysql.query}`) parses, containment-checks, and journals. A custom effect is a *marker* minted by a wrapper/connector module whose public defs carry the custom label plus the real underlying effects, so callers transitively need both and a policy can deny either by path; there is no namespace object behind a custom label (`mysql.query(...)` in a body NameErrors). `sema check` adds a near-miss lint for built-in namespaces in rows (`!{fss.read}` → "did you mean `fs`?"); genuinely distinct custom names stay clean. The docs-site effects catalog is rewritten as the canonical union of the runtime's effect maps (prelude `namespaced_effect`/`effect_op_known`/`builtin_effect`), the native-registry rows, the explicit `check_effect_op*` sites, and the governance capability map, each entry stating where it is checked, whether instances are scope-enforced, and which Cortex capability grants it — plus the honest enforcement model: per-op boundary checks + caller containment (checker and runtime) + policy row verdicts + scoped-instance enforcement only for net endpoints, skill loads, staged exec, and ffi bridges, with governance postures, the taint watermark, the command denylist, and the OS sandbox carrying what labels cannot. | Effect vocabulary is authority *labeling*, not OS confinement — documenting the open-row design next to where each effect is actually enforced prevents both the "closed catalog" misread and label-laundering assumptions (a custom kind cannot confine an `fs.write` holder away from db files); the wrapper pattern is the object-capability discipline applied to rows. | Closing the vocabulary to the built-in set (kills domain capabilities like `payments.*`); erroring on unknown namespaces (breaks the declarative-config escape and custom markers); a dynamic namespace object for custom effects (would swallow the very typos the near-miss lint catches). | | D126 | String-literal parity slice (§5.13): single and double quotes are interchangeable (incl. `'''…'''` triple form); ordinary bodies add the Python-oriented escapes `\'` `\a` `\b` `\f` `\v` `\xHH` `\uXXXX` `\UXXXXXXXX` and `\` continuation (unknown escapes stay loud lex errors; `\N{name}`/octal rejected); new raw `r"…"` and raw-template `rf"…"`/`fr"…"` prefixes keep backslashes literal (a backslash before the delimiter keeps both characters, so a raw string cannot end in a lone backslash) while `rf`/`fr` still interpolate `{expr}` with `{{`/`}}` as the literal-brace spelling; `re"…"` regex literals are now RAW so `\d+` needs no double escaping; prefixes stay lowercase-and-adjacent-only; triple-quoted bodies stay raw. `Tok::FStr` carries the raw flag so the splitter applies the Sema `\{`/`\}` extension only to non-raw f-strings | Prompt templating, command text, and SQL need Python-habit strings without escape fights; regex class escapes were unusable (`re"\d"` was a lex error); raw+interpolation is the standard prompt-template combination; loud unknown escapes preserve the no-silent-no-op ethos | Case-insensitive prefixes (one canonical spelling wins); escape-processing triple strings (would silently change existing docstrings/prompts/LaTeX); `\N{name}` (Unicode name-table dependency) and octal escapes (legacy footgun) | | D125 | Equation `pinv(A)`/`pseudoinverse(A)`, `lstsq(A, b)`/`least_squares(A, b)`, and `cond(A)`/`condition_number(A)` are pure exact-arity SVD-derived operations for finite, nonempty, rank-2 dense-real matrices. All share D121's cutoff $s_{max}\max(m,n)\epsilon$ and a stricter preflighted derived-work budget. For $A\in\mathbb{R}^{m\times n}$, pseudoinverse returns the $n\times m$ Moore-Penrose inverse; least squares accepts one finite length-$m$ right-hand side and returns `(solution, residual_norm, numerical_rank, singular_values)`, selecting the minimum-norm solution and checking $A^T(Ax-b)$ under the backward-error scale $\lVert A\rVert(\lVert A\rVert\lVert x\rVert+\lVert b\rVert)$ using a log-scaled ratio that cannot overflow or underflow merely while forming that denominator; condition number returns spectral $\kappa_2$ and positive infinity for numerical rank deficiency. | These operations form one coherent SVD-derived profile and close the immediate D121 downstream gap without duplicating unstable kernels. A pinned CPython 3.12.12/NumPy 2.4.6 process executes the same 1,000 rectangular, scaled, ill-conditioned, repeated, zero, and rank-deficient matrices with zero rank/classification/value divergences under conditioning-aware relative norm comparators. Every case additionally checks all four Moore-Penrose conditions; boundary tests cover nonfinite, shape, empty, arity-before-evaluation, derived-work failure, and representable `1e200` least squares; cheap RHS validation precedes decomposition; tree-walker and VM results/aliases agree; checker, reflected docs, LSP, and a three-test Silver example are green. The initial oracle exposed and repaired an unstable exact-fit normalization; independent review then exposed and repaired direct-denominator overflow, the missing projector-symmetry conditions, and a loose absolute comparator floor. | Forming $(A^T A)^{-1}A^T$ and squaring the condition number; returning an arbitrary rather than minimum-norm underdetermined solution; treating numerical rank deficiency as a finite condition number; componentwise or absolute-floor matrix comparison; forming the backward-error denominator with overflow-prone direct products; normalizing an exact-fit self-check by its near-zero residual; accepting bool, empty, nonfinite, complex, sparse, batched, symbolic, unit, AD, or device inputs silently; claiming multiple right-hand sides, alternate norms, benchmarks, platforms, or broad linalg completion. | | D124 | Equation dense linear algebra extends `matmul`, `matvec`, and `solve` to finite rank-2/rank-1 complex CPU tensors, with exact finite-real promotion and checked shape/work/nonfinite/singularity/conditioning/residual failures. Equation `sparse(rows, cols, row_indices, col_indices, values)` validates bounded finite-f64 COO triplets and canonicalizes them to sorted duplicate-free CSR; `sparse.matmul` accepts a dense-real vector or matrix; `sparse.solve` explicitly densifies only square systems through 128×128 and delegates to the checked dense LU. Sparse values exit as tagged inspectable `SparseMatrix` records but do not silently re-enter equations. Sparse-sparse fill-in and unimplemented sparse decompositions fail typed. | Complex contractions and sparse matrices are foundational scientific domains, but their resource and representation policy must be explicit. Shared registry metadata drives checking/docs/LSP, 12 kernel tests and 12 tree/VM boundary tests cover canonicalization, promotion, typed errors, arity order, serialization, non-re-entry, and the exact densification ceiling, and one pinned CPython 3.12.12 subprocess executes 400 SciPy 1.17.1 sparse construction/product cases, 300 sparse solves, and 360 NumPy 2.4.6 complex products/solves with zero divergence. | Silent duplicate aggregation; implicit sparse-sparse fill-in; an unbounded dense fallback mislabeled sparse solving; lossy complex promotion; treating an inspectable record as authenticated re-entry; claiming sparse LU/eigen/least-squares, complex inverse/QR/eigh/SVD, batching/devices, symbolic/unit/AD domains, benchmarks, platforms, or broad linalg completion. | | D123 | Equation `interpolate(xs, ys, x)` evaluates and `polynomial_interpolate(xs, ys)` expands the unique degree $\le n-1$ Newton-form interpolating polynomial over 1..=64 distinct knots. Lane selection is exactness-following and never silent: all-exact inputs stay canonical `QQ` under the shared 16,384-bit ceiling (coefficients ascending, exactly one entry per sample point, trailing zeros kept), while any float input selects a strict finite-real `f64` lane where non-finite inputs, intermediates, and results fail typed. Empty samples, length mismatches, duplicate knots, the point ceiling, bools, and symbolic inputs fail typed, and arity is rejected before arguments evaluate. | Polynomial interpolation is the first interpolation-family slice in the scientific ledger, reuses the existing exact/float dual-lane conventions (D112, D120), and its Newton form gives both an $O(n^2)$ preflightable work bound and exact QQ coefficients where the domain is exact. One pinned subprocess matches 260 exact SymPy 1.14.0 cases bit-for-bit and 260 finite-real cases against SciPy 1.17.1 barycentric evaluation, NumPy 2.4.6 `polyfit`, and correctly rounded exact references under scaled forward-error bounds — 520 cases, zero divergence — plus focused tree/VM parity, checker/docs/LSP metadata, and a Silver example. | Lagrange basis re-evaluation per query (no reusable coefficients, worse growth); barycentric-only form (no exact monomial coefficients); silent promotion of huge exact values to `f64` (violates fail-closed exactness); unbounded point counts (unpreflightable work) | | D122 | Equation `prime_nth(index)`/`prime(index)` use one-based positive exact-integer indexing through 100,000; `prime_count(value)`/`primepi(value)` count primes less than or equal to an exact non-negative integer through 2,000,000. All aliases share one deterministic preflighted sieve, reject arity before evaluation, allocate flags fallibly, and return exact integers or typed domain/dtype/profile/resource failures. | Prime indexing and counting are fundamental number-theory operations and close an explicit scientific-ledger gap without adding syntax. Rosser's upper bound makes the nth-prime sieve finite and sufficient. One pinned SymPy 1.14 process now covers 128 seeded/boundary prime pairs in addition to the existing number-theory corpus: 1,152 inputs and 4,864 exact checks total, with tree/VM, registry/checker/docs/LSP, and Silver-example evidence. | Zero-based indexing; repeated trial division for each candidate; unbounded allocation/search; evaluating a surplus undefined argument before arity failure; silently coercing bool/float/non-integral inputs; claiming modular/symbolic/tensor dispatch, large-prime algorithms, benchmark/platform qualification, or broad number-theory completion. | | D121 | Equation `svd(A)` is a pure exact-arity reduced singular-value decomposition for a finite, nonempty, rank-2 dense-real matrix. With $A\in\mathbb{R}^{m\times n}$ and $k=\min(m,n)$ it returns `(U, s, Vt)` with shapes $m\times k$, $k$, and $k\times n$; singular values are finite, nonnegative, descending, and reconstruct $A$ with orthonormal reduced factors. A bounded, scale-normalized one-sided Jacobi algorithm avoids forming $A^T A$, preflights output and worst-case work, reports nonconvergence and derived nonfinite values typed, and normalizes vector signs deterministically. Equation `rank(A)` uses the same singular values and NumPy's default relative threshold $s_{max}\max(m,n)\epsilon$, so nonzero scaling does not change rank. | SVD is the stable basis for rank, pseudoinverse, least squares, conditioning, nullspaces, and PCA-like programs. The previous Gauss-Jordan rank used an absolute `1e-10` pivot cutoff and therefore mislabeled a valid matrix such as `[[1e-12]]` as rank zero. One shared scale-relative decomposition law removes that correctness defect while establishing reusable residual, orthogonality, resource, and oracle evidence. | Computing eigenvectors of $A^T A$ and squaring the condition number; componentwise comparison of non-unique singular vectors; an absolute rank tolerance; returning full matrices without an explicit shape contract; silently accepting empty, nonfinite, bool, complex, sparse, batched, symbolic, or device inputs; claiming `pinv`/least-squares/condition-number completion, AD, benchmarks, or platform qualification from this reduced dense-real slice. | | D120 | Equation-only `floor`/`ceil`/`round`/`trunc`/`fract` are pure one-argument operations over bounded exact `QQ`, finite `f64`, formal symbolic expressions, recursive numeric list/tuple containers, same-evaluation `Approx` evidence, and rank-1/rank-2 dense-real tensors. `round` uses half-to-even; `fract = x - trunc(x)` preserves floating signed zero. Containers keep their kind/shape under a depth-128 and 1,000,000-value budget. Rank-zero/higher-rank tensors, nonnumeric containers, nonfinite lanes, oversized exacts, and invalid symbolic substitutions fail typed. Arity precedes evaluation; variable-dependent AD paths for all five are `NotDifferentiable`; transformed `Approx` methods append `->operation` while residual/iterations/convergence remain upstream evidence. | Rounding spans exact, IEEE, symbolic, tensor, evidence, checker, and bridge semantics, so a scalar-only dispatch arm was not an honest public feature. One explicit contract now drives registry checking, reflected docs, LSP, tree/VM execution, and boundary validation. Pinned CPython 3.12.12 covers 640 `Fraction`/raw-f64 outcomes and pinned NumPy 2.4.6 covers 20,865 rank-1 lanes bit-for-bit; focused rank-2, resource, symbolic, return-annotation, poisonous-arity, signed-zero, and evidence tests pass. | Evaluating surplus arguments before rejecting arity; truncation or half-away rounding mislabeled Python parity; losing signed zero; unbounded recursive containers; silently widening rank-zero tensors; swallowing symbolic substitution errors; laundering a rounded solver value as the raw method output; claiming Unicode floor/ceiling, `round(x, ndigits)`, decimal/interval/dual/complex/sparse/device/higher-rank support, authenticated `Approx` runtime re-entry, benchmarks, platforms, or broad CAS completion. | | D119 | Equation-only `normal_logppf(log_p, loc, scale)` is a pure exact-arity scalar inverse of the Normal log-CDF. Inputs must be finite reals with `log_p < 0` and `scale > 0`; the affine result must be finite or fail typed. Zero, including negative zero, is an endpoint domain error; non-finite inputs fail `NonFinite`. | Near-zero log probabilities reflect through `-expm1(log_p)` so distinct probabilities do not round to one. Representable lower probabilities reuse D118, while underflowed tails use an overflow-safe Mills seed and fixed-point correction followed by at most two residual-improving direct-log-tail refinements with a Mills-ratio derivative. Fused affine scaling avoids false intermediate overflow. A pinned SciPy 1.17.1 `ndtri_exp` oracle checks 1,024 cases from the smallest negative subnormal through `-f64::MAX`; three mpmath 1.3.0 100-digit inversions independently bind an intermediate far-tail region where SciPy loses accuracy. The shared Normal corpus remains 8,198 outcomes; focused tree/VM/checker/docs/LSP/adversarial/example lanes pass. | Implementing `normal_ppf(exp(log_p), ...)` across the whole domain; using `1-exp(log_p)` near zero; subtracting extreme log-CDF/log-density values to obtain a Newton derivative; treating one approximate library as infallible; returning infinities at endpoints; unbounded iteration; silently accepting an unrepresentable affine result; claiming distribution objects/defaults, sampling/RNG, fitting/inference, tensor/batch/symbolic/AD support, benchmarks, platforms, or broad distributions. | | D118 | Equation-only `normal_ppf(p, loc, scale)` is a pure exact-arity scalar Normal inverse-CDF evaluator. Probability, location, and scale must be finite reals, with `0 < p < 1` and `scale > 0`; the result must be finite or fail typed. Endpoint probabilities are domain errors rather than aliases for infinities. | A local inverse series protects near-median ULP accuracy; elsewhere a bounded Acklam rational seed gives a deterministic approximation. At most two residual-improving refinements use D117's direct log-tail functions, and fused affine scaling avoids false intermediate overflow. The shared pinned SciPy 1.17.1/NumPy 2.4.6 oracle checks 1,024 PPF cases, including the smallest positive subnormal, branch boundaries, and location/scale variation, alongside the six Normal evaluators for 7,174 outcomes total; focused tree/VM/checker/docs/LSP/adversarial/example lanes pass. | Returning ±infinity at `p=0` or `p=1`; unbounded Newton iteration; refining through underflowed ordinary CDF/SF; silently returning an unrepresentable finite-input result; adding implicit defaults or a cosmetic distribution object; claiming log-PPF, sampling/RNG, moments/fitting/inference, tensor/batch/symbolic/AD support, benchmarks, platforms, or broad distributions. | | D117 | Equation-only `normal_logcdf(x, loc, scale)` and `normal_logsf(x, loc, scale)` are pure exact-arity scalar Normal log-tail evaluators. Inputs must be finite reals and `scale > 0`; stable direct tail formulas preserve finite extreme-tail logarithms without first materializing an underflowed CDF/SF, while unrepresentable negative log tails fail typed. | Log-tail probability is a fundamental numerical primitive for likelihoods and rare events. The implementation shares D116's standardization and symmetry laws but computes the requested logarithmic tail directly rather than as `ln(normal_cdf(...))` or `ln(normal_sf(...))`. The shared pinned SciPy 1.17.1/NumPy 2.4.6 oracle checks all six Normal operations across 1,024 triples / 6,144 ordinary outcomes plus six stable-overflow references; focused tree/VM/checker/docs/LSP/adversarial/example lanes pass. | Taking `ln` after CDF/SF underflows to zero; silently returning `-inf` for an unrepresentable finite-input result; adding implicit defaults or a cosmetic distribution object; claiming PPF, sampling/RNG, moments/fitting/inference, tensor/batch/symbolic/AD support, benchmarks, platforms, or broad distributions. | | D116 | Equation-only `normal_pdf(x, loc, scale)`, `normal_logpdf(x, loc, scale)`, `normal_cdf(x, loc, scale)`, and `normal_sf(x, loc, scale)` are pure exact-arity scalar Normal evaluators. Inputs must be finite reals and `scale > 0`. Standardization uses a scaled fallback when finite subtraction overflows; derived infinite standardized distance means PDF +0 and CDF/SF saturation, while unrepresentable log-density or density fails typed. Log-PDF is direct and CDF/SF use separate erfc tails. | This is the smallest coherent distribution evaluation surface and establishes a reusable `_` law without pretending equation attributes or distribution values exist. The survival function is not `1-cdf`, preserving upper-tail precision. A pinned SciPy 1.17.1/NumPy 2.4.6 oracle checks 1,024 triples / 4,096 ordinary outcomes plus four stable-overflow references; focused tree/VM/checker/docs/LSP/adversarial/example lanes pass. | A cosmetic first-class object without value/method/codec semantics; implicit defaults; accepting nonpositive scale; `ln(pdf)`; `1-cdf`; an unaudited inverse-normal approximation; claiming PPF/log tails, sampling/RNG, moments/fitting/inference, tensor/batch/symbolic/AD support, benchmarks, platforms, or broad distributions. | | D115 | Equation-only `cross_correlation(left, right)`/`correlate(left, right)` implement full real one-dimensional cross-correlation for two non-empty finite-real lists, tuples, or rank-1 vectors. Results follow increasing lags $-(m-1)..n-1$, equivalently `convolution(left, reverse(right))`; output length is $n+m-1$ and shares D114's 1,000,000-element, 10,000,000-multiply-add, compensated-accumulation, and strict nonfinite/overflow contract. | Cross-correlation is a fundamental signal primitive and reuses one audited direct kernel without conflating it with D113 Pearson correlation. Structural lengths and output/work bounds are preflighted before kernel-owned operand cloning/conversion or output allocation, and the reversed right signal is indexed without a copy. Focused tree/VM/checker/docs/LSP/resource/example lanes pass; a separate kernel oracle matches 512 pinned NumPy 2.4.6 pairs / 32,552 coefficients under coefficient-wise forward-error bounds. | Reversing the wrong operand; calling Pearson correlation; silently normalizing; promoting Unicode `⋆` without parser/tooling support; assuming real semantics define complex conjugation; claiming same/valid modes, axes/batches, FFT, symbolic/sparse/device domains, benchmarks, platforms, or broad transform completion. | | D112 | Exact bounded equation number theory adds `next_prime(n)`, `prev_prime(n)`, and `divisor_count(n)`. Prime navigation is strict, stays within the non-negative $2^{32}-1$ profile, checks at most 1,024 odd candidates, returns typed `DomainError` when no previous prime exists below $n \le 2$, and returns `NotImplemented` if the next prime leaves the profile. Divisor count reuses canonical bounded factorization and checks its multiplicative count. | Prime navigation and divisor count are fundamental companions to public primality/factorization. The existing single pinned SymPy 1.14 process now checks 1,024 deterministic inputs / 4,608 exact outcomes with zero divergence, while tree/VM, registry/checker/docs/LSP, typed boundary failures, and the Silver scientific-domains example share the same contract. | Unbounded prime search; probabilistic answers; returning an out-of-profile integer; defining `prev_prime(2)` by sentinel; recomputing divisors into a list merely to count them; claiming nth/counting primes, large-prime algorithms, symbolic/tensor number theory, benchmarks, platforms, or broad completion. | | D113 | Equation-only finite-real statistics expose `expectation`/`E`, `mean`, population `variance`/`Var`, `std`, `covariance`/`Cov`, Pearson `correlation`/`Corr`, and strict-simplex `entropy`/`H`, `cross_entropy`, `kl_divergence`/`D_KL`, and `js_divergence`/`JS`. Inputs are flat finite-real lists, tuples, or rank-1 vectors of length 1..=1,000,000; population functions use `ddof=0`; information functions use natural logs and require nonnegative mass summing to one within $10^{-12}$. Empty/nonfinite/oversized/mismatched/zero-variance/infinite-support cases fail typed. | These operations form one reusable statistics contract rather than aliases over unsafe private kernels. Arity is preflighted before evaluation, stable accumulation avoids false overflow where possible, every spelling shares registry/checker/docs/LSP metadata, and a focused smoke corpus agrees across both engines. A separate kernel oracle matches 960 outcomes against pinned NumPy 2.4.6/SciPy 1.17.1. | Silent empty→zero; fabricated zero correlation for constant samples; implicit probability normalization; NaN/inf propagation; sample/population ambiguity; treating ordinary axis-aware `math.mean` as the same surface; claiming weights, missing-data policy, sample estimators, distributions, inference/regression, tensor/device statistics, benchmarks, platforms, or broad completion. | | D114 | Equation-only `convolution(left, right)`/`convolve(left, right)` implement full linear convolution for two non-empty finite-real lists, tuples, or rank-1 vectors. The output length is $n+m-1$, capped at 1,000,000; direct work is capped at 10,000,000 multiply-adds; each coefficient uses deterministic compensated accumulation; nonfinite inputs, intermediate products/sums, and results fail typed. | Full rank-1 convolution is the smallest coherent transform slice and reuses the existing bounded dense kernel without inventing a new syntax family. Equation results cross as native Tensor values, so shared first-axis indexing yields dtype-correct scalars or rank-reduced subtensors with negative-index normalization, zero-tail preservation, checked shape/storage arithmetic, and a 100,000-element copy ceiling in tree/VM. Arity is preflighted and a focused smoke corpus covers tree/VM plus registry/checker/docs/LSP; a separate kernel oracle matches 512 pairs / 32,768 scalar outputs against pinned NumPy 2.4.6 under coefficient-wise forward-error bounds. | Keeping the undocumented `conv` alias that conflicts with convex-hull notation; defining empty convolution as an empty vector; silent NaN/inf; promoting Unicode `∗` without parser support; unbounded indexing copies; claiming `same`/`valid` modes, axes/batches, complex/symbolic/sparse/device convolution, FFT/correlation/filtering, benchmarks, platforms, or broad transform completion. | | D111 | `linear_program(c, A, b[, max_iterations])` and `lp` are one bounded finite dense-real standard form: maximize `c·x` subject to `A x <= b`, `x >= 0`. A real two-phase tableau simplex uses Bland's first eligible entering column plus a stable leaving tie-break. Resource ceilings cover variables, constraints, tableau cells, and pivots. The structured verdict distinguishes `Optimal`, `Infeasible`, `Unbounded`, `IterationLimit`, and `NumericalFailure`; every incumbent is replayed against each original constraint with per-row scaling, non-optimal outcomes never receive a fabricated optimum, and an iteration-limited feasible incumbent remains explicitly non-optimal. | A public optimization surface needs honest classification and residual evidence before a larger modeling language. Focused core/adversarial tests, tree/VM runtime parity, registry/checker/docs/LSP metadata, and one pinned SciPy 1.17.1 / NumPy 2.4.6 process over 500 seeded optimal/infeasible/unbounded cases exercise the slice. | Vertex enumeration presented as general LP; unstable pivot ties; global-scale residual checks that let an unrelated huge row hide a violation; NaN or a plausible point standing in for a failure; implicit boolean/scalar/flat-matrix/tensor coercion; claiming minimization modeling, arbitrary bounds/equalities, exact/decimal/interval/symbolic/tensor/sparse/unit domains, dual/infeasibility certificates, sensitivity, interior-point/external adapters, benchmarks, platforms, or production LP completion. | | D110 | Public set/logic support is one bounded explicit `FiniteSet` plus reason-carrying `Truth` domain. Construction/algebra/membership/quantifiers are exact over canonical finite elements; mixed equal representations fail, no scalar/list is silently reinterpreted by an algebra operation, empty indexed intersection is `UnknownUniverse`, and resource ceilings cover elements, retained key cost, power sets, families, and equation comparison work. Unicode logic is strong-Kleene; ASCII `not/and/or/xor` stays ordinary two-valued logic. | Natural-language/formal bridges need Unknown to survive composition and finite sets to be deterministic, auditable values rather than list-shaped conventions. Focused tree/reference-runtime evidence, explicit VM-safe coverage, adversarial bounds, pinned Python/SymPy/PyTorch parity, registry/checker/LSP metadata, and a checked Silver example exercise the slice. | Unknown→false coercion; scalar/list→set algebra coercion; operand-dependent numeric representatives; unbounded quadratic indexed folds; calling this symbolic/infinite/tensor set support; claiming JSON, complement, quotient, partition, supremum, infimum, benchmark, platform, or broad-CAS completion. | | D109 | `import lean; lean.check(source)` is the smallest public formal-engine adapter: an ordinary effectful `!{proc.run}` API pinned to Lean 4.10.0, with 256-KiB source/output bounds, a 15-second deadline, private temporary artifacts, SHA-256 source/executable identity, exact version/process-exit/provenance evidence, and typed reserved-`Verified`/`AuthenticatedConfined`/`CheckedUntrusted`/`Unknown`/`Unavailable`/`Error` results. The checked fragment is comment/string-aware-scanned complete unindented LF-only single-line named `theorem` declarations; `example` is forbidden because Lean 4.10 discards it from the environment, while carriage returns, multiline continuations, `sorry`, axioms, notation/fixity, unsafe/metaprogram/environment commands, native/compiler-trust escapes, scanner-desynchronizing strings, warnings, and process output are also forbidden. Startup captures raw selection I/O-free; source validation and an exact source/pin/policy-bound discovery approval precede resolution/hashing, and an identity-bound execution approval plus revalidation precede artifact or process work. Optional pins require a canonical symlink-free root-owned/non-writable Unix toolchain and inspect every entry. Authentic result objects use in-process origin identity, are immutable, and have no implicit truth value; producer status strings cannot promote provenance, the result type name is reserved, and only `lean.is_verified(value)` consumes origin authenticity. PATH checks are development-only `CheckedUntrusted`. Valid pins return `Unavailable` without execution on every platform because the candidate macOS runner remains public-disabled: its bounded stdin → `/dev/fd/0` transport and certificate v2 close the source-path race, but it retains allow-default read/process/IPC authority, lacks full CPU/memory/process/fd/scratch quotas and an immutable dependency-closure manifest, replays only certificate metadata, and performs no transitive axiom audit. Same-kernel `lean4checker --fresh` replay on 4.10 would not justify implementation-independent `Verified`, while the official comparator does not support 4.10. Every public result has `accepted = false` and `execution_confined = false`; `AuthenticatedConfined` and `Verified` are unreachable, and `lean.is_verified` always returns false. | The adapter refuses to launder a sound kernel behind mutable PATH/wrapper/environment/source-input or nominal/copy/JSON evidence into a proof claim. Conservative non-proof PATH checking remains useful during development, while every production pin fails closed until a qualified isolated runner exists. | A pure equation call; treating stdout/clean process exit, same-kernel replay alone, or copied/JSON fields as a broad proof; any current `AuthenticatedConfined` or `Verified` claim; accepting arbitrary Lean versions; silent fallback; a source-selected executable; accepting non-persisted examples; claiming deny-default confinement, transitive axiom audit, implementation-independent replay, general strings/tactics/macros/imports, complete resource quotas, signed attestation, broad library compatibility, trusted platform provenance, or multi-platform completion. | | D108 | Dense complex tensors add deterministic `sum`, `mean`, and `prod` under D101's signed-axis and `keepdims` shape law, plus D102's three-way-broadcast `where` with a boolean condition and complex/complex branches. Reduce-all returns a complex scalar; axis/`keepdims` returns a complex tensor. Sum/product identities are `complex(0.0, 0.0)`/`complex(1.0, 0.0)`; empty mean, nonfinite intermediate results, invalid axes, ordered reductions, and mixed-dtype `where` fail typed. | Complex scientific pipelines need accumulation and masking before linalg, but neither requires a new dtype or promotion law. Reusing the existing outer×axis×inner traversal and broadcast odometer preserves deterministic order, shape/resource preflight, and real/bool behavior. One gate executes 144 reductions and one broadcast selection against pinned NumPy 2.4.6 and PyTorch 2.12.1, with exact tree/VM value parity. | Pairwise/tree reductions with backend-dependent order; returning NaN for strict empty mean; adding an implicit `where` branch promotion; defining complex order for min/max/arg reductions; claiming complex linalg, AD, sparse/device, benchmarks, platforms, or complete tensor support. | | D107 | Dense tensors add finite `complex` storage beside `f64` and canonical `bool`. Uniform construction uses `dtype="complex"` (required for empty complex tensors). Trailing-axis `+ - * /` accepts complex tensors and finite-real tensors/scalars under one explicit promotion to complex; unary negation and `abs`, plus `math.sqrt/exp/log/ln/sin/cos/tan`, are checked elementwise. Shape/resource bounds are unchanged, division by zero and nonfinite components fail typed, and unaware JSON/foreign boundaries reject complex tensors. | A real complex scalar without array storage leaves scientific model code unable to express batched amplitudes or frequency-domain values. Reusing the existing dense shape/odometer layer keeps dtype orthogonal to shape and avoids paired-real-list encodings. One gate executes 96 deterministic tensor cases against pinned NumPy 2.4.6 and PyTorch 2.12.1, with exact tree/VM value parity and explicit construction/promotion/error/boundary regressions. | Encoding complex elements as adjacent real list entries; silently mixing complex/real payloads at construction; implicit bool promotion; accepting nonfinite components; silently serializing through an unaware foreign codec; claiming complex comparison/order, floor/mod/power, reductions, `where`, contractions/linalg, reshape/indexing, AD, sparse/device, benchmarks, platforms, or complete complex-tensor support. | | D106 | Public exact equation number theory extends D105 with `mod_inverse(value, modulus)`, generalized consistent non-coprime `crt`/`chinese_remainder(moduli, residues)`, `totient(n)`, ascending `divisors(n)`, and `mobius(n)`. Factor-derived functions retain the positive $2^{32}-1$ profile. Modular inputs use the 16,384-bit exact ceiling; CRT is capped at 256 congruences and 1,000,000 Euclidean iterations, returns canonical `(least_nonnegative_solution, lcm)`, accepts modulus one, and rejects inconsistent systems and oversized products with typed failures. | Modular merge and arithmetic functions are a coherent reusable number-theory layer, not project syntax. One pinned SymPy 1.14 process checks 1,024 deterministic inputs / 3,072 exact outcomes with zero divergence, including inverse, generalized CRT, totient, divisors, Möbius, negative residues, modulus one, squareful/squarefree cases, tree/VM parity, checker, registry, reflected docs, and LSP. | Pairwise-coprime-only CRT mislabeled as general; unsorted divisors; approximate inputs; silent inconsistent-system fallbacks; unbounded BigInt Euclid/product growth; claiming gcdex certificates, next/previous prime, divisor counts, large-prime algorithms, symbolic/tensor dispatch, Diophantine solving, benchmarks, platforms, or broad number theory. | | D105 | Public exact equation number theory begins with `is_prime(n)` and `factorint(n)`: non-negative/positive exact integers through $2^{32}-1$, deterministic trial division under 65,536 trials, canonical ascending `(prime, exponent)` pairs, arity-before-evaluation, and typed domain/dtype/out-of-profile/resource outcomes. Registry metadata is shared by checking, reflected docs, and LSP. | Factorization is a core requested symbolic-computation capability, but an unbounded naive kernel would be a denial-of-service surface. A finite profile gives predictable work and exact results; 512 seeded/boundary cases match pinned SymPy 1.14.0 with zero divergence, while tree-walker and VM results/errors are identical. | Probabilistic or silent factor guesses; accepting approximate/fractional inputs; unbounded trial division; treating the 32-bit slice as general number theory; claiming large-prime, Pollard-rho, modular/CRT, Diophantine, certificate, benchmark, or platform completion. | | D104 | Conditional symbolic calculus is explicit about its real-domain obligations. Equation calls `cancel(expr)` and `integrate(expr, variable[, lower, upper])` return `(expression, conditions)`, where conditions are symbolic `nonzero`, `nonnegative`, or `positive` predicates. The bounded exact fragment covers condition-aware cancellation, exact rational powers, QQ polynomial/rational-power antiderivatives, exact finite-point rational limits, and order-12 Taylor series. Additive/removable cancellation cannot erase source singularities; exact results are revalidated against the 16,384-bit ceiling; unsupported forms fail typed. | A CAS rewrite is unsound when `x/x` becomes `1` without retaining `x != 0`, or when a resource failure quietly becomes a formal expression. The implementation pre-collects definedness before cancellation/expansion and the required 11,000-case SymPy gate includes 500 limits and 500 series with zero divergence. | Globally enabling aggressive cancellation; discarding assumptions; evaluating predicates through lossy `f64`; swallowing resource failures; heuristic limits; claiming general elementary/multivariate integration, transcendental/complex/path limits, Laurent/Big-O series, or theorem proofs from this bounded real fragment. | | D103 | Equation dense-real linear algebra exposes checked `det`, `solve`, `inv`, `qr`, and symmetric-only `eigh`. Partial-pivot LU, Householder QR, and bounded Jacobi eigendecomposition independently preflight input/output/work; use scale-stable finite norms; reject singular, ill-conditioned, nonsymmetric, nonfinite, and resource failures with typed evidence; and self-check residuals, orthogonality, triangularity, and eigenvectors. General `eig`/`eigenvalues`/`eigenvectors` remain honestly unsupported. | Dense linalg needs numerical evidence, not only plausible values. One pinned NumPy 2.4.6 subprocess checks 1,000 deterministic conditioned matrices with `n=1..16` and κ₂≤10⁶ across determinant/solve/inverse, 200 QR subsets, 200 symmetric eigen cases, and 100 rank-deficient classifications; it emits explicit evidence/timing with zero divergences. The shared kernels back equation matrices, registry/checker/docs/LSP metadata, and tree-walker/VM results. Extreme `1e308`/`1e-308`, zero-column allocation bypasses, derived nonfinite values, arity-before-evaluation, boolean rejection, and error propagation are regression-tested. | Naive squared norms; allocation before output preflight; NaN-erasing maxima; labeling a symmetric real solver as general eig; coercing boolean matrices to 0/1; collapsing all failures into one domain string; claiming batched/tensor/device/complex/sparse linalg, SVD/LU/Cholesky/expm, performance, or platform completion. | | D102 | Dense tensors have an explicit runtime dtype foundation: `TensorData::F64` and canonical byte-backed `TensorData::Bool`. Rectangular `tensor(...)` construction infers one uniform dtype and accepts an optional matching `dtype="f64"|"bool"`, including empty bool tensors; mixed payloads and mismatches are `DTypeError`, known future dtypes are `UnsupportedError`, and unknown names are `ValueError`. Numeric and boolean trailing-axis comparisons return boolean tensors; `where` performs three-way broadcast with a boolean condition and same-dtype branches; `any`/`all` are signed-axis/`keepdims` boolean reductions with empty identities false/true. Tensor values have structural equality for collection operations, while every implicit tensor truth context fails with `DTypeError` and requires explicit `any(tensor)` or `all(tensor)`. Numeric math, contractions, reductions, embedding providers, and foreign numeric boundaries reject or visibly journal boolean tensors instead of silently treating truth as floating `0/1`. | Predicates and masks need a real semantic domain before tensor programs can be reliable. A tagged payload makes dtype visible at every runtime/interop boundary and keeps boolean storage compact. One shared broadcast odometer underlies comparisons and selection; reduction output shape is resource-checked before allocation and empty broadcast strides cannot overflow. The strengthened gate executes 360 pinned NumPy 2.4.6 numeric/bool comparison, f64/bool `where`, and `any`/`all` cases, requires identical tree/VM values, and covers truth/contract ambiguity, empty bool construction, structural membership, oversized zero-shape broadcasts, reduction resource limits, and typed construction/arithmetic/shape/axis/dtype failures. | Encoding booleans as f64; implicit numeric↔bool or tensor→scalar-truth conversion; truthiness reductions over numeric tensors; accepting requested dtypes cosmetically; silently falling back from an invalid provider; allocating a reduction before checking its output shape; branch dtype promotion without a declared law; claiming integer/complex/sparse/device tensors, batched linalg, tensor indexing/reshape, benchmark/platform, or full tensor completion. | | D101 | The strict dense-f64 reduction family is complete for `sum`, `mean`, `prod`, `min`, `max`, `argmin`, and `argmax` under D100's signed-axis/`keepdims` shape law. Sum/product use `0.0`/`1.0` identities; mean/min/max/arg reductions reject materialized empty slices; every input must be finite; sums/products detect finite-to-nonfinite overflow; min/max preserve values; arg reductions return the first tied index and use scalar `int` when reducing all elements (axis results remain exact-small-index f64 tensors until integer dtype lands). | Scientific tensor programs need the whole reduction family, not a flatten-only sum. One deterministic outer×axis×inner kernel prevents per-operation shape drift. The gate executes 360 seeded NumPy 2.4.6 cases across ranks 1–3, axes `None`/`0`/`-1`, `keepdims`, ties, and empty identities, plus tree/VM cases for every public spelling and typed empty/NaN/overflow failures. Registry rows drive checking, generated docs, and LSP for the new spellings. | Separate loops with different axis semantics; last-index tie behavior; NaN/inf propagation in the strict profile; float axes; returning sentinel indices for empties; silently applying tensor-only `prod`/arg operations to ordinary lists; claiming boolean reductions, integer tensor dtype, sparse/device reduction, performance/platform, or full tensor completion. | | D100 | Dense-f64 `sum` and `mean` are axis-aware reductions. `axis` is an optional signed integer (negative values normalize by rank), `keepdims` is boolean, and omitted `axis` reduces all elements; an axis result preserves row-major order and either removes the axis or replaces it with one. Sum uses the `0.0` identity; mean of a materialized empty reduction is `DomainError`; nonfinite inputs and finite-accumulator overflow fail loudly. Ordinary exact-list reductions retain their prior exact `int`/`QQ` behavior and reject tensor-only keywords. | Flatten-only reductions made matrix/batch code lose shape and could not express standard scientific pipelines. One outer×axis×inner kernel gives bounded deterministic order, shares tree/VM dispatch through the builtin registry, and focused cases cover axes 0/1/-1, `keepdims`, reduce-all, out-of-range axes, empty means, and exact-list compatibility. | Silently flattening every tensor; accepting float axes; returning NaN for an empty mean in the strict profile; making list sums floating; implementing product/min/max/arg reductions without their distinct empty/ordering contracts; claiming the still-missing ≥300-case NumPy reduction oracle, bool dtype, sparse/device, performance, or platform completion. | | D99 | Dense-f64 elementwise arithmetic and binary `math` functions use NumPy-compatible trailing-axis broadcasting: dimensions align from the right and each pair must be equal or one; rank-zero tensors are scalars; zero-sized dimensions remain zero-sized. The resolved product is checked against the one-million-element limit before allocation, incompatible shapes are `ShapeError`, and element-domain/overflow/zero failures retain the resolved flat index. D99 supersedes D89's equal-shape-only tensor restriction without changing scalar behavior or `matmul`. | Scalar-only broadcast forced common `(batch, 1) op (1, features)` programs to materialize repeated tensors and diverged from the requested Python/NumPy model. One stride-zero odometer kernel now serves ordinary operators and binary `math`; 240 seeded add/subtract/multiply cases match executed NumPy exactly across scalar, rank-promotion, singleton-axis, and empty-axis shapes, while runtime regressions require identical tree-walker/VM results and typed incompatible-shape failures. | Pairwise shape special cases; allocating expanded operands; unchecked output products; treating a one-element rank-1 tensor as a scalar; broadcasting contractions such as `matmul`; claiming bool dtype, comparisons, reductions, sparse tensors, device transfer, or full tensor completion from pointwise f64 broadcasting. | | D98 | Public `decimal` accepts only exact decimal strings or integers and carries an explicit significant-digit context: precision `1..=4933`, rounding `half_even` or `half_up`. Construction preserves the exact input; same-context `+ - * /` and resource-bounded integer powers round once to the result context using exact `BigRational` arithmetic; negation/`abs`, `.precision/.rounding`, numeric equality, annotations, and canonical tagged JSON are defined. Context mismatch is `DomainError`; binary floats and implicit mixed arithmetic are rejected. Canonical display intentionally drops trailing-zero significance. | A decimal domain backed by `f64` would make the context cosmetic. Exact rational intermediates plus explicit tie handling make the rounding law testable. The focused gate matches 240 seeded Python 3.12.12 `decimal` results exactly across precisions 7/28/50 and both rounding modes in tree+VM, plus positive/negative tie cases, context identity/rebinding, typed failures, annotations, and strict codecs. | Binary-float construction; implicit context merging; unbounded exponentiation; silent float/int mixing; accepting noncanonical wire values; claiming trailing-zero significance, traps/status flags, ordering/conversion matrix, sqrt/elementary functions, tensors/symbolics, benchmarks, platforms, or full decimal compatibility. | | D97 | Public `modint(value, modulus)` and its explicit `Modular(value, modulus)` alias produce the same exact canonical residue class with `2 <= modulus <= 2^63`. Construction reduces arbitrary bounded Sema integers; same-modulus `+ - * /`, signed-i64 `**`, unary negation, `.value/.modulus/.inverse`, equality, truth, annotations, deterministic string-valued tagged JSON, registry-backed checking, reflected signatures, and LSP completion are defined. Products use `u128`; powers use bounded logarithmic exponentiation; inversion uses extended Euclid. Different moduli and mixed ordinary integers are rejected, non-units have no inverse, and zero division is specifically `DivisionByZero`. | Modular arithmetic needs exact canonical identity and modulus provenance; treating residues as integers loses the ring. The fail-closed gate requires pinned CPython 3.12.12, structurally compares full tagged `(residue, modulus)` values for 320 seeded arithmetic cases plus 102 adversarial constructor cases per spelling, and runs both aliases in tree and VM. It also exercises modulus 2 and $2^{63}$, signed 81-digit inputs, annotations, canonical codecs, arity/keyword/type/shape failures, modulus mismatch, and non-units. | Float-backed residues; rendered-text comparison; silently combining different moduli; implicit integer promotion; overflow-prone `u64` multiplication; reducing noncanonical wire payloads during decode; claiming general finite fields, polynomial rings, CRT, tensor/symbolic dispatch, operation-exclusive benchmarks, three-platform evidence, or broad number-theory completion. | | D96 | Public `quaternion` is a finite approximate Hamilton scalar backed by checked `Quaternion64`: zero-to-four-component construction, same-domain `+ - * /`, unary negation, `abs`/norm, `.w/.x/.y/.z/.conj/.norm/.inverse/.normalized`, vector `rotate`, and shortest normalized `slerp`. Runtime annotations, deterministic `$sema.type="quaternion"` JSON, boundary rejection, and registry metadata for constructor/rotation/interpolation share the contract. Quaternion division is right multiplication by the denominator inverse and zero denominators are `DivisionByZero`; mixed scalar arithmetic is rejected until an explicit promotion law exists. | Quaternion support must preserve noncommutative order and geometric normalization rather than masquerade as a four-vector. The focused gate executes 320 seeded cases against SymPy 1.14.0 for Hamilton algebra and point rotation, requires tree/VM bit identity, and covers rotation/slerp endpoints, annotations, codecs, and typed zero/shape/range/cross-domain failures. | Treating quaternion multiplication as elementwise; silently accepting scalar multiplication without a promotion contract; unnormalized rotation/interpolation; reporting zero division as a generic domain error; claiming axis-angle, powers, tensor/symbolic/AD, performance, platform, or broad geometry completion from this scalar slice. | | D95 | Public `interval` is a finite closed certified enclosure backed by `Interval64`: `interval(point)`/`interval(lo, hi)`, mixed finite-real outward-rounded `+ - * /`, exact-i32 powers, unary negation, `abs`, scalar/subinterval membership, `.lo/.hi/.mid/.width`, and certified `math.sqrt/exp/log/ln`. Runtime annotations, deterministic `$sema.type="interval"` JSON, native registry metadata, and explicit foreign-boundary rejection share the domain contract. | Proof-oriented interval arithmetic requires inclusion, not ordinary tolerance. Algebraic endpoints are derived through exact rationals and rounded outward; transcendental endpoints use bounded rational proofs. The focused gate encloses 1,216 seeded Python results, requires bit-identical tree/VM endpoints, and covers annotations, codecs, membership, and typed invalid-bound/zero/domain/unsupported failures. | Wrapping `libm` results and calling them certified; silently accepting reversed/non-finite bounds; defining interval ordering; exposing uncertified trig; claiming empty/unbounded/disconnected/ball, tensor, symbolic, benchmark, multi-platform, or broad-CAS completion from this finite scalar slice. | | D94 | Public `complex` is a finite approximate scalar backed by checked `Complex64`: `complex()` and one/two-argument construction, mixed finite-real `+ - * /`, unary negation, magnitude, `.re/.im/.conj/.abs/.arg`, and `math.sqrt/exp/log/ln/sin/cos/tan`. C99/Python signed-zero branch selection is preserved. Runtime annotations accept only the public domain; deterministic `$sema.type="complex"` JSON preserves component bits; Python/JavaScript and unaware protocol crossings reject it explicitly. The native registry exposes constructor arity/return metadata to checking, docs, and LSP. | A kernel-only complex type could not participate in Sema programs or prove toolchain parity. The focused gate executes 320 seeded Python `cmath` oracle cases, asserts tree-walker/VM bit identity, branch-cut signs, typed failures, annotation/codec round trips, and foreign-boundary rejection. | Treating complex as two-element lists; silently sending tagged values to unaware workers; permitting non-finite components in the finite profile; claiming complex tensors, symbolic complex algebra/AD, powers, inverse/hyperbolic/special functions, string parsing, benchmarks, or broad-CAS completion from this scalar slice. | | D93 | Equation ASCII calculus calls `jacobian(expr)` and `hessian(expr)` are first-class parser spellings for `MathKind::Diff { Jacobian | Hessian }` and require exactly one target expression. The Unicode/operator surface and ASCII calls lower to the same formal node; extra arguments fail at parse time rather than being ignored. | Jacobian/Hessian were advertised as part of the mathematical surface, but the ASCII call forms could parse as ordinary calls instead of the intended formal differential operators. The parser AST tests, negative arity test, and sema-math kernel tests pin the one-expression contract. | Treating `jacobian(x, y)` as a partially supported multivariate API before the semantics exist; leaving ASCII calls as generic function calls; silently dropping extra arguments. | | D92 | Runtime structural annotations are enforceable but must preserve mutable identity when validation does not change representation. Ordinary function/decorator parameters and returns now enforce exact `QQ` and supported structural annotations (`list`, `dict`, tuple, `Option`, structs/enums, and `Tensor`) while skipping erased generic type variables such as `T` and `list[T]`. `Tensor` annotations accept existing tensors and numeric list/tuple values; concrete list contracts such as `list[f64]` can materialize rank-positive tensors into nested lists. Mutable list/dict/struct parameters return the original object when every member already satisfies the annotation. | Enforcing annotations exposed real bugs: typed dict/list returns were previously unchecked, but naive coercion cloned mutable arguments, so functions like `add_unique(out: list[int])` mutated a copy and GraphRAG retrieval returned empty candidates. Tensor-backed numeric kernels also need to expose public `list[f64]` contracts without forcing every caller to know the internal tensor representation. Focused regressions cover typed dict rejection, Tensor/list conversion, generic erasure, list-of-struct sort/take, mutable argument identity, external Tensor JSON, and the full example suite. | Leaving annotations as comments; cloning every mutable parameter during validation; treating concrete unknown types as erased generics; forcing all tensor-using examples to expose internal Tensor types; accepting unsupported annotations by manufacturing default values. | | D91 | Public `int`/`Int`/`ZZ` is one arbitrary-precision signed domain with a canonical `i64` fast path and automatic BigInt promotion. Literal parsing is capped at 4,300 decimal digits; runtime results at 16,384 bits; and tagged decimal interchange at the derived 4,933 digits. Exact arithmetic, floor/mod, powers, shifts, bitwise operations, equality/order/membership/sort/sum/abs, and equal-numeric hashing share the promoted semantics in the tree-walker and VM. Integer true division forms an exact rational before finite-`f64` rounding; zero-negative/non-real/non-finite powers fail with typed errors. JSON and Python/JavaScript bridges preserve BigInts, while C `i64` and SQLite integer boundaries reject out-of-range values. | Fixed `i64` contradicted the public type contract, lost values above $2^{63}-1$, and made exact CAS/proof work depend on accidental symbolic promotion. Python differential cases, near-ceiling JSON/Python round trips, and 416/416 runtime tests pin arithmetic, resource, and boundary behavior. Keeping source, runtime, and wire ceilings distinct prevents denial-of-service without making a computed value impossible to serialize. | Silent `i64` wrap; float-backed large integers; an unbounded allocation surface; independently converting huge division operands to `f64`; a 4,300-digit wire cap that cannot round-trip a legal runtime value; coercing BigInts through C/SQLite; claiming exact `QQ`, equation-BigInt, typed dictionary keys, or fixed-width runtime identity from this slice. | | D90 | Equation scientific unary calls use one exact-arity canonical table spanning trig/inverse/hyperbolic, exp/log, sqrt/cbrt, abs/sign/recip/angles, and erf/erfc/gamma/lgamma. Numeric evaluation maps scalars, vectors, and matrices without changing shape and reports indexed finite-to-non-finite `DomainError`; symbolic inputs remain formal/exact. Forward AD uses checked formulas, including erf/erfc, while gamma/lgamma return typed `NotDifferentiable` until a checked digamma kernel exists. | A separate ad-hoc equation path had inconsistent function coverage, error spelling, shape handling, symbolic names, and derivatives. One table keeps numeric, formal, and AD semantics aligned; the complete math package and runtime equation integration pass, and the required PyTorch gate checks 900 classifications, 744 value/d1, and 142 d2 cases. | Reusing ordinary runtime dispatch without equation/Sym/AD semantics; returning `ValueError` or tensor NaN; flattening shape; finite-difference derivatives as the language contract; guessing gamma derivatives; claiming complex/dtype/device or general AD completion. | | D89 | Ordinary `math` extends D87 with shape-aware binary and checked-integer dispatch. `atan2`/`hypot`/`copysign`/`pow`/`fmod`/IEEE `remainder`/`nextafter`/`log(x, base)` accept scalars and, after D99, bounded right-aligned equal-or-one trailing-axis tensor broadcasting; mismatches/domain/zero errors are typed and keywords/extra args are rejected. `factorial`/`comb`/`perm`/`gcd`/`lcm`/`isqrt` use checked `i64`; scalar floor/ceil/trunc/ties-even round return checked integers while tensor forms stay elementwise `f64`. | Python scalar/tensor oracle fixtures require distinct remainder semantics, exact integer helpers, explicit broadcasting, and loud overflow/domain/shape behavior. One binary dispatch law prevents per-function tensor drift; D99 matches 240 executed NumPy cases in both engines. | Unbounded or left-aligned broadcasting; treating rank-one singleton vectors as scalars; float-backed combinatorics; wrapping integer overflow; silently accepting keywords/extras; forcing tensor rounding into integer tensors before dtype semantics exist; claiming complex/dtype/device/equation/AD completion. | | D88 | Symbolic values distinguish arbitrary-precision `Exact(BigRational)` from `Approx(f64)`. The bounded exact QQ slice preserves rational arithmetic and integers above $2^{53}$ through expand/substitute/differentiate, rational factorization, linear/quadratic solve, conditional cancellation, polynomial/rational-power integration, finite-point rational limits, and order-12 rational Taylor series; irrational roots remain formal, structural identities—not rendered text—key canonical grouping, source definedness survives removable cancellation, and unsupported forms fail typed. D91 made ordinary and equation integer/decimal/QQ arithmetic bounded-exact. Exact rational source syntax still requires explicit promotion; general assumptions, elementary/multivariate integration, transcendental/algebraic/complex/path limits, Laurent/Big-O series, complex domains, and wider factorization remain open. | `1/3 + 1/6`, large-integer promotion, symbol-name/render collisions, irrational roots, `x/x`, and one-sided poles exposed that a float-only or render-keyed CAS cannot support exact algebra or sound proof inputs. Python `Fraction`, equation QQ fixtures, and the required 11,000-case SymPy gate pin the bounded domain. | `f64` coefficients labeled exact; decimal pretty-print equality; simplifying away source domain conditions; approximating irrational roots in symbolic results; heuristic limit fallback; unbounded expression growth; claiming public QQ or a general CAS from the bounded slice. | | D87 | Ordinary `math` begins scientific completion with an explicit runtime unary dispatch contract. `sinh`/`cosh`/`asinh`/`acosh`/`atanh`, `exp2`/`expm1`/`log1p`, `cbrt`, `trunc`/`fract`, angle conversions, `recip`, and libm-backed `erf`/`erfc`/`gamma`/`lgamma` require exactly one runtime argument and apply elementwise to scalar, Tensor, and Embedding values while preserving shape. A finite input producing a non-finite result is `DomainError`; tensor errors identify the element index. The native signature registry now makes this contract visible to compiler/typechecker, reflected docs, and LSP, while broader per-domain rows remain open. | Python-oracle and nested-expression tests exposed two cross-surface requirements: function arity must fail loudly rather than ignore extras, and scalar domain rules must apply to every tensor element rather than silently retain `NaN`. One dispatch helper plus the native registry keeps runtime and static surfaces aligned. | Scalar-only scientific functions; silently ignoring extra arguments; returning tensor `NaN` where the scalar call errors; claiming binary/complex/reduction/dtype/device/equation/AD completeness from the unary slice. | | D86 | Simulation/world-model semantics remain expressible with existing `struct`, pure transition functions, invariants, `test`/`assure`, and bounded `loop_until`; no simulation keyword is added. `examples/os-simulator-world-model` provides the deterministic fail-closed shell slice, and `examples/dentate-os-simulator` adds 96/96 bounded M6 episodes against one real pinned upstream invocation with a logical clock and 20 risk probes. | Both ports express state, action, validity, transition trace, invariants, bounds, and terminal conditions without new syntax. Their remaining common needs—hidden state, branching/shrinking, debugger projection, and interactive environment APIs—must be designed as general contracts before vocabulary grows. | A `simulation` keyword justified by fixtures alone; host filesystem or wall-clock calls that make worlds nondeterministic; model-driven implicit transitions; claiming a general world-model framework from bounded materializers. | | D85 | Numerical and proof evidence remain explicit at the runtime boundary. Iterative math returns a first-class `Approx` record; non-finite wire values use tagged encodings; hardened solvers only set convergence after finite residual/stationarity/settling checks. `prove_identity` is a bounded checked-`i128` integer-polynomial fragment over the original equation AST with separate producer/checker modules and `ProofResult` outcomes. The Z3 QF_LIA/QF_LRA adapter classifies negation-`unsat` as `UnverifiedUnsat` with integrity-bound `SmtSolverEvidence`; it cannot construct `Proved` without an independently checkable proof object. Exact counterexamples replay locally and `unknown` remains typed. | Stripping approximation metadata let callers confuse a candidate with an answer; serializing non-finite values as `null` destroyed the result; heuristic simplification before proof could make `x/x = 1` appear true; a fake executable returning `unsat` showed that script/digest replay proves provenance, not theorem truth. Only independently replayed native fragments establish the current sound theorem boundary. | Bare solver values; `NaN`/infinity as `null`; CAS equality, solver exit, or successful tests labeled as proof; calling script/provenance replay a certificate; treating bounded polynomial/SMT fragments as a universal theorem system. | | D84 | Run evidence is session-owned and bounded: each interpreter creates an exclusive `.sema/runs/` manifest/journal/seal, children carry parent/track ids, over-limit events become typed gaps, and explicit close/sync is available to Rust/Python/Node owners. Exact appended bytes are SHA-256 hashed in memory and verified by re-read at finalization; records form a per-record SHA-256 chain. Ordinary events use bounded mixed static/dynamic FIFO batches, while lifecycle/decision/error events force live barriers. `sema debug serve` is loopback/token confined; source-snapshot v4 and execution-provenance v4 pin a domain-separated parser/AST-index source digest, immutable source/origin bytes, recomputable top-level and nested statement/expression/equation node IDs, and independent declaration/nested-AST digests validated by the TypeScript UI. Captured check-family and semantics events carry paired canonical source/expression IDs on exact unique matches; missing, ambiguous, and mutable-healing matches stay unlinked. Replay and event projection enforce the same link validity. DAP `attach` fails closed until genuine governed attach exists. This remains an observation-spine slice, not the final unified trace/replay ABI, general producer correlation, time travel, or an externally anchored audit store. | A shared truncating journal lost exactly the parent/child evidence agent fan-out needs, and repeated backend/UI provenance drift showed why fixtures and the embedded bundle must consume the producer's real versioned contract. A debugger needs a race-free bounded source before a rich UI, and DAP program output must never share protocol bytes. In-process SHA-256 readback catches same-length mutation while the trusted digest exists; a self-contained chain can still be rewritten after exit and needs an immutable/signing anchor for durable authenticity. | Shared append/truncate journals; flushing every ordinary event; an unauthenticated local HTTP port; backend/UI schema drift; guessing node IDs from spans without the captured parent/ordinal; treating DAP `attach` as `launch`; treating an unanchored hash chain as durable post-process authenticity; claiming general time travel from bounded linked checks. | | D83 | Python-compatible floor division `//` is a first-class multiplicative operator in ordinary code and equation blocks. Integer results round toward negative infinity, floating results remain floating, tensors apply the operation elementwise, zero divisors raise `DivisionByZero`/`DomainError`, and signed modulo retains the invariant `a == (a // b) * b + a % b`. Lexer, ASTs, parsers, runtime/VM fallback, math engine, EBNFs, tree-sitter (which already advertised `//`), TextMate, and tests are one surface. The C bridge no longer publishes or trusts a persistent `.sema/native` cache: supported declaration-derived signatures compile verified bytes through a unique private artifact, load and unlink it, and reuse the handle only within that interpreter. Governed and DAP execution reject this in-process ABI until an isolated native worker exists. | A user-supplied example identified `//` as a basic missing operator; the audit then proved the editor grammar accepted syntax the reference compiler rejected. The full Python quotient/remainder law removes ambiguity for negative operands. The full-suite baseline also exposed a real cross-architecture cache collision in `hybrid-interop`, and follow-up review showed that even a content-addressed pathname leaves a verification-to-`dlopen` race and that in-process native code cannot honor a governed isolation boundary. | A `math.floor(a / b)` library spelling (wrong integer/error semantics and loses operator parity); truncation toward zero (breaks Python parity and the signed-modulo identity); basename/mtime, architecture-addressed, or even digest-addressed persistent native caches on the unsafe load path; pretending an in-process dynamic library is policy-confined. | | D82 | Native `@inject(...)` dependency injection (§5.53) + `source ... as ` config sub-namespacing (§5.15). `@inject(name: Type, ...)` (or the shorthand `@inject(Type, ...)`) on a `def` fills the named/trailing parameters from the runtime-managed singleton (`suite_instance`, cached — the SAME instance across all call sites, Spring-style); callers omit those args (`run_deep("q")`), so a config/component threads through a pipeline without appearing in every signature. `inject_trailing` supplies each omitted dep as a keyword arg by parameter name (robust across positional/keyword calls); an explicit argument overrides it; injected params must be TRAILING (a loud `sema check` + runtime error otherwise); the checker marks them optional so public arity drops. Injection resolves under the config/DI boundary, so the decorated fn's effect row need not gain `fs.read`/`env.read`. `@inject` is a native (lowercase) decorator resolved by the runtime, distinct from user (PascalCase-by-convention) `def` decorators (D70). `source ... as ` nests that source's overlay under `` (`cfg..a.b`), so multiple sources/configs never collide at the root. | sema-search review: even with dynamic dotted config, threading `cfg: SearchConfig` through every `run_*`/`write*` step (and passing it at every call) is exactly the parameter plumbing DI exists to remove — the caller of `run_deep` should not know about `cfg`. Managed-singleton injection at the signature (Java Spring `@Inject`/`@Autowired`) is the requested ergonomic; sub-aliasing avoids root-key collisions when several configs inject into one scope. | A hidden env/global read for the dependency (untracked, untyped); a user-library `@inject` (the runtime must own singleton lifecycle + boundary effects); injecting non-trailing params by silent reordering (chosen: require trailing + loud error); tree-sitter as grammar source-of-truth (the hand-parser + EBNF sketch are — tree-sitter regen for the `@inject(name: Type)` arg form is a pending build step). | | D81 | §5.34 `http.serve(port, handler, host?)` gains an optional explicit bind **host** (default `127.0.0.1`; pass `"0.0.0.0"` to serve in a container behind a gateway), and `std.web` adds `serve_on(app, host, port)` (`serve(app, port)` delegates with the default). The host is a plain argument the caller supplies (typically from config), so the native op reads no env. | Containerized Sema web apps were unreachable through Docker port-forwarding because `http.serve` hard-bound `127.0.0.1`. Reading `SEMA_HTTP_HOST` inside the native op was rejected: a `!{net.listen}` row would then observe process env without declaring `env.read`, breaking the effect model — the bind host must be caller-supplied, keeping the only env read at the declared config boundary (sema-search sets `cfg.server.host=0.0.0.0` via its config env source). | Reading env inside the native op (hidden, ungoverned env read); adding `env.read` to `http.serve`'s effect mapping (breaks every existing caller). | | D80 | §5.18 project module discovery walks `src/` **recursively** — files may be grouped in subfolders (PHYSICAL grouping only: the module id stays the file *stem*, globally unique, so a duplicate stem is a loud error) — and a sibling `tests/` directory is discovered for `check`/`assure` only, never for a plain `run`. One shared `loader::discover_project_modules(root, include_tests)` backs the run loader, `check_project`, and `assure`'s `parse_project`, with deterministic stem-sorted order. Imports resolve by last path segment, so `from .` and the folder-qualified `from .<sub>.` both resolve to the same stem (the folder segment self-documents location). | The sema-search review wanted a growing flat `src/` grouped into logical subfolders + an end-to-end test in `tests/`; the loader read only `root/src/*.sema` non-recursively and discovery was triplicated. Physical-only grouping (unique stems) avoids the churn/collision risk of true dotted module identities; keeping `tests/` out of `run` stops a deployed program parsing test-only modules. | True nested module identities (`resolve_imports` uses `path.last()` — a larger rework); loading `tests/` in the general `run`/deploy path. | | D79 | §5.15 **schemaless (dynamic) config**: a `config` suite declaring only `source` directives (no fields/groups/requires) injects the merged overlay tree AS its value — a nested, dot-accessible record inferred from the YAML/JSON files (`build_config_group`: on `declared.is_empty()` it materializes the merged `Dict` into nested `Value::Struct` via `dict_to_record`, skipping the unknown-key guard + coercion; scalars keep the parser-inferred int/float/bool/str, nested maps recurse, lists map element-wise). `sema-lsp` completes `cfg.` fields by reading the config's `source` file (narrow in-LSP YAML/JSON key scanner, no runtime dep; head var resolved by param type, sole-config fallback restricted to config-ish names), so design-time IntelliSense needs no hand-written schema. Typed configs (declared fields) are UNCHANGED — the dynamic branch fires only on a fieldless config. | sema-search review: hand-declaring a full typed schema JUST to get dotted access + IntelliSense was the friction ("do we need this explicit declaration?"); users want to point at a YAML/JSON and get `cfg.a.b.c` + a field preview without a schema, accepting no compile-time field typing. | A new `Value::Record` variant (invasive across every match arm); overloading `Value::Dict` dot-access (breaks dict methods `.get`/`.keys`); reading the source file inside the runtime for the LSP (couples editor tooling to runtime internals). | | D78 | §5.15 config `source` directives are LIVE (were inert tier-0, "defaults only"): `source yaml/json [optional]` reads+parses a file (new std-only `yaml` value parser mirroring `json`), `source env prefix "P"` overlays P-prefixed env vars (suffix `__`→nested dotted path, single `_` kept), `source cli ` overlays `path=value` strings; precedence defaults < file < env < cli, deep-merged onto the declared config tree, then dotted-accessed (`cfg.a.b.c`) + injected (`inject T`). Overlay scalars are type-coerced to the declared field type (lossless int↔float, scalar→str, parsed string→scalar); an incompatible type OR an unknown *file* key is a loud `ConfigValidationError` (env/cli ignore unknowns — shared namespace), a missing required file errors unless `optional`, malformed → `ConfigError`. Source reads run under a synthetic one-effect config-boundary frame (`fs.read`/`env.read` attributed to the config decl, not the injecting caller) while policy+governance still apply; path/prefix exprs eval under the caller row (no effect smuggling). `yaml.decode`/`yaml.parse` also exposed as native ops. | Native typed config with dotted access + Hydra-shaped injection was designed but inert — a program saw only its declared defaults; sema-search (and any config-driven app) needs real file/env config instead of hand-rolled string dot-path readers over `json.decode`. Same "make the flagship surface real" pass as D74–D77. | Keeping sources inert (a silent no-op, §5.9); a full YAML 1.2 parser (config subset only — errors loudly on anchors/aliases/tags/merge/multi-doc/tabs); leaking config-source effects into every `inject` caller's row; silently ignoring unknown file keys or coercing incompatible types (defeats dynamic type safety); a `toml` source reader + full `args`/`option()` CLI parsing (deferred — `toml` errors with a pointer, `source cli` overlays only an explicit list). | | D77 | `simulate def` return-schema hints are built structurally from `def.ret`: a struct expands to `{"field": type, …}` and a `list[T]` to `[]`, recursively (cycle-detected via a `seen` path set, len-16 backstop), so nested/list returns (`list[Fact]`, `TableSet`) tell the model the exact shape. Complement: in `coerce_to_type` a `list[T]` field ALWAYS decodes to a list (a non-array JSON value → empty list, never a non-iterable). | A flat "respond with JSON of type list" hint let the model guess field names, so real `list[Fact]` extraction validated to zero facts and a `TableSet`'s deeply-nested rows returned empty/non-iterable — the emitted schema must be as deep as the declared type. | A fixed shallow depth cap (truncates legitimate nesting like Table→Row→cells); pushing schema shape into per-app prompt text (the generation seam must be structural, not hand-rolled per call) | | D76 | A `@provides(...)` capability provider runs under its OWN declared effect row, not the immediate caller's. `dispatch_provider` pushes the provider's row as the active frame before the call (`call_provider_fn`), so the caller-containment check trivially passes while the provider's own `check_effects` and every per-op check still enforce + journal that row. | A provider is a capability implementation the runtime invokes, so it legitimately holds effects the caller lacks — the documented pattern `@provides("embed") def … !{proc.run}` (or `@provides("generate")` reading env / calling the model) was `Denied` because the internal dispatch inherited the (often empty) caller frame. | Making providers pure/effect-free (defeats the point — they wrap Python/net/ffi); bypassing effect enforcement entirely for providers (loses per-op governance + journaling) | | D75 | `http.serve` (§5.34) reads the full request — headers + Content-Length body, across packets — and exposes `{method, path, query, body, headers}` (header names lowercased) to the handler, which returns EITHER a `str` (→ 200 `application/json`) OR a dict `{status?, content_type?, headers?, body?}` for full control of the status line, content type, and extra response headers. Enables real REST parity: `X-API-Key` auth 401s, 400/422 validation, CORS headers, and base64-in-JSON payloads (e.g. a rendered PDF field). | The prior parser read only the GET request line (no body, no headers) and hardcoded `200 OK application/json`, so a `POST` API with auth/validation was impossible; a JSON research API is the motivating app (sema-search). Backward compatible (string return unchanged). | Raw binary response body (base64-in-JSON matches the reference API and `Value` has no bytes type); a full framework router | | D74 | `simulate def`/`simulate operator` execute through the real generation seam. When a generate backend exists (a `@provides("generate")` provider or a configured real GGUF model), the runtime renders a prompt (stable `[sema:simulate fn=]` marker + `sem` descriptor + input values + a return-type schema hint), generates via the shared `agent_generate` seam, and decodes the returned JSON into the declared return type (`coerce_to_type`), then runs the `ensure`/repair pass. No backend → a loud `SimulationUnavailable`, unless the deterministic engine is explicitly opted in (`[engine] deterministic = true` / `SEMA_DETERMINISTIC=1`), under which the schema-fill runs byte-identically for hermetic tests — never a silent fallback for a configured-but-failed backend. A backend that yields no output / non-JSON / a shape mismatch is a loud `SimulationFailed`, never a silent deterministic fill. | The flagship neurosymbolic construct was a pure mock schema-fill that ignored `@provides` and the real model, so `simulate def` could be neither model-backed nor tested with a fixture provider — a hollow proof for a research app whose cognitive steps are all `simulate def`. Now real, testable, and fail-loud. | Prompt-substring fixture selection (brittle; use a stable fn marker); silent fallback to a deterministic fill on decode failure (masks a broken fixture/model — dishonest) | | D73 | Declarative `bridge` blocks run REAL foreign code (§5.10): `python.inline`/`python.isolated` execute the `.py` file / inline `begin python` block in the persistent Python worker (D58); `js.component` imports the `.ts`/`.js` in a persistent Node worker (Node ≥23 strips types, no build step); `c.abi` compiles a verified source snapshot, or copies a SHA-256-verified prebuilt library, into a private unique artifact, dlopen's it through declaration-derived typed trampolines (one/two float vectors plus length, or homogeneous f64/i64 scalars), immediately unlinks it, and reuses the handle only within that interpreter. Governed and DAP executions reject in-process C until an isolated native worker exists. Args/returns marshal through the supported codec, then boundary `require`/`ensure`/`check` re-validate. Unsupported/unavailable adapters fail typed in every mode, and plain ports without an admitted translation fail `PortedError`; foreign returns are never synthesized. | The interop example must actually load and run TS/Python/C, not synthesize plausible numbers (a tamper test proved the old path fabricated results); the warm Python worker (D57/D58) already exists, Node type-stripping removes the TS build step, and compiling C on demand keeps the artifact platform-correct; a real crossing that still passes through Sema's contracts is the whole "governed adoption membrane" thesis. Private unlinked C artifacts remove shared-cache and verification-to-path races without pretending same-UID in-process native code is confined. | Keeping the tier-0 synthesize/kernel stub (fabricated returns); non-strict degradation to a guessed value; persistent native caches on the unsafe load path; pretending in-process C is governed or DAP-safe; a subprocess-per-call Python/JS bridge (slow/stateless); a full libffi general C marshaller before shipping the common numeric shapes | | D1 | Pythonic indentation, not a superset; PEG + soft keywords; editions from v0.1 | Adoption empirics + LLM prior transfer + Mojo/Codon precedent ([12 §1–2](./research/12-syntax-dx.md)) | Braces family; Python superset; exotic syntax | | D2 | `~=` returns graded `Sim`; branch coercion requires calibration; regions type `statistical(α)` | Fuzzy-bool casts are the SymbolicAI defect class ([01 §3](./research/01-symbolicai.md)); conformal threshold certificates ([05 §4.1](./research/05-pl-theory-guarantees.md)) | Bare-bool `~=`; global provenance-semiring propagation (kept as research track, Q2) | | D3 | `semantics()` denotes a pinned judge in the type: (judge hash, calibration id, α); protocol evaluation, never one raw judge | Ill-posedness + hallucination inevitability ([05 §1.4](./research/05-pl-theory-guarantees.md)); judge reliability-without-validity ([arXiv:2606.19544](https://arxiv.org/html/2606.19544)) | NL predicate as ambient truth; single-judge semantics; `holds()` rename | | D4 | Contracts in the public signature; failed values are typed-failed and cannot flow; `check` (graded) vs `ensure` (fatal); Findler–Felleisen blame everywhere | Enforcement-not-advice ([01 §6](./research/01-symbolicai.md)); contracts as cache firewalls ([09 §3.2](./research/09-verification-testing.md)); BAML check/assert ([04 §2.2](./research/04-ai-native-languages.md)) | Advisory contracts; contracts as comments/decorators outside the type | | D5 | `simulate def` adopts MTP (`by` + `sem` + meaning IR as public cached artifact) + contracts, budgets, `untrusted` labeling, uncertainty field | Published, user-studied 3.2× result ([arXiv:2405.08965](https://arxiv.org/abs/2405.08965)); Apple on-device constrained decoding ([04 §2.1](./research/04-ai-native-languages.md)) | Prompt-template DSL (LMQL died); LLM-as-VM (Universalis, anti-thesis); runtime-only retry (DSPy Assert deprecation) | | D6 | **Brief conflict:** verification default-on, `testable` keyword retired; `assure bronze/silver/gold`; red/amber/green with mutation-adequacy gate | Weak suites launder wrong LLM code (EvalPlus, [arXiv:2305.01210](https://arxiv.org/abs/2305.01210)); PBT 50× mutant density ([OOPSLA 2025](https://dl.acm.org/doi/10.1145/3764068)); opt-out beats opt-in ([12 §2.3](./research/12-syntax-dx.md)) | Opt-in `testable` keyword (the brief); line-coverage gating | | D7 | Effects-and-handlers spine; `policy` = capability/effect restriction + Cedar-shaped decision layer with compile-verified examples; typed effects, never string matching | One mechanism covers policy/replay/mock/batch ([05 §3.3](./research/05-pl-theory-guarantees.md)); every string gate is respellable ([03](./research/03-harness-archaeology.md)) | Runtime-only interception (Cortex-harness style); Rego-class Turing-complete policy language | | D8 | Keep `monitor` **against** the rename advice of [12 §2.3](./research/12-syntax-dx.md) | Sema has no Hoare-monitor construct, so no intra-language collision; "model monitoring" is the dominant meaning for the target audience; corpus-wide consistency. Collision documented in the spec's disambiguation note | `tracked` / `observed` / `distribution` (revisit at user testing, Q1) | | D9 | **Brief conflict:** split `native` (bind) / `ported` (translate with differential gate) | Bind ecosystems, translate self-contained code only ([07](./research/07-interop.md)); Java `native` precedent ([12 §2.3](./research/12-syntax-dx.md)); type-constrained decoding for translation ([PLDI 2025](https://arxiv.org/abs/2504.09246)) | One overloaded `native`; on-the-fly translation | | D10 | **Brief conflict:** healing is supervision-scoped (`supervise`/`heal`) with restart-first triage and a deterministic gauntlet, not a global mode | OTP structural-recovery evidence + self-repair-needs-external-feedback evidence ([10](./research/10-self-healing-drift.md); [arXiv:2306.09896](https://arxiv.org/abs/2306.09896)) | Program-wide `heal` flag; LLM-judged patch acceptance | | D11 | Trust lattice `untrusted < validated < trusted` on all values; generative outputs born untrusted; endorsement only via contracts/verifiers/human approval | CaMeL/FIDES ([arXiv:2503.18813](https://arxiv.org/abs/2503.18813), [arXiv:2505.23643](https://arxiv.org/abs/2505.23643)); ocap-clean-from-day-one requirement ([08](./research/08-policy-governance.md)) | Pure control-flow confinement without value labels; full Jif-style IFC annotations | | D12 | Session-typed `protocol` declarations for multi-turn generative exchanges; structured concurrency only | Structure is deterministic even when payloads are stochastic ([05 §3.4](./research/05-pl-theory-guarantees.md)) | Untyped agent loops; MCP schemas as the top-level abstraction | | D13 | Models are pinned first-class values with roles and calibrations; no floating refs, ever | AION artifact discipline ([02](./research/02-aion-os.md)); judge identity = program semantics ([05 §6.2](./research/05-pl-theory-guarantees.md)) | String model names resolved at runtime; provider-default "latest" | | D14 | **Brief conflict:** BRIEF §3.8's "extend/grow the codebase" half is scoped out of v1 — `heal` is repair-only (patch-scoped `code.patch`, zero endorsement); sanctioned growth = descriptor-space regeneration at `simulate` sites + human-approved patch-scope widening (§5.11) | Intrinsic self-modification without external grounded feedback degrades results ([arXiv:2306.09896](https://arxiv.org/abs/2306.09896), [arXiv:2310.01798](https://arxiv.org/abs/2310.01798)); a general write capability breaks healing's escalation-proof-dead-end property ([08](./research/08-policy-governance.md)); feedback metatheory unresolved (Q4) | Program-growing healer with general `code.gen` authority; LLM-judged feature additions | | D15 | Monitor-or-decay holds per calibrated decision site; the compiler derives input monitors, shared per `(judge, calibration)` pair, where none is declared; footprint charged to SMG budgets and reported by `sema doctor` (§5.9) | S(α) is honest only under an active anytime-valid monitor ([05 §6.7](./research/05-pl-theory-guarantees.md)); per-site hand-written declarations tax authors into `best_effort`; sharing bounds monitor count by judge+calibration pairs at O(1) sketch cost ([10](./research/10-self-healing-drift.md), [11](./research/11-semantic-memory.md)) | Mandatory per-site declarations; silent S(α) without monitors; per-site unshared monitors by default | | D16 | `sem` descriptors and refinements are native at field, struct, function, operator, and bridge boundaries | Pydantic/LLMDataModel field descriptions are the right authoring shape, but optional library validation cannot gate dataflow; Sema needs descriptors in canonical flattening, diagnostics, constrained decoding, stack traces, and repair context | Only out-of-line `sem Type.field`; comments/docstrings as schema descriptions; field-only descriptors | | D17 | User-defined operators are typed functions with contracts/effects/policy, and `simulate operator` is the semantic-overload form | SymbolicAI proves overloaded semantic operators are ergonomic, but its runtime fallback and fuzzy bools hide failure; Sema makes dispatch, effects, postconditions, and monitor obligations compile-visible | Library metaclass mixins; arbitrary parser-level custom symbols before user testing | | D18 | Foreign code uses typed `bridge` membranes by default: normal native files plus Sema `expose def` signatures; inline `begin`/`end` blocks are small trusted glue only | Adoption requires existing Python/TS/C code to remain usable, but guarantees only hold at typed membranes; the bridge keeps native toolchains while giving Sema contracts, descriptors, policy, diagnostics, and re-validation | Making mixed-language `.sema` files the default; single-purpose `.semapy`/`.semats` extensions that lose host-language editor/tooling support; pretending inline foreign code is fully confined | | D19 | Interpolation, regex matching, `match`, and SQL templates are native typed constructs with provenance, captures, validation, and database effects | Pattern extraction and query composition are where many semantic bugs and injections happen; Sema needs compiler-visible templates, typed captures, SQL ASTs, policy effects, and semantic checks instead of opaque strings | Raw SQL/string concatenation; library-only regex extractors; untyped switch/case over strings; Scala-style custom extractors before the base pattern IR is validated | | D20 | Prompt templates and model contexts are native typed constructs: `template` returns `Prompt[T]`, and `context` is a state machine over role-scoped prompt slots | LLM applications are mostly context construction; making prompts opaque strings recreates framework-level context management and hides roles, placeholders, validators, token budgets, injection boundaries, and state diffs from the compiler | Jinja/Mustache as the primary prompt surface; raw prompt strings passed to models; unrestricted template metaprogramming before v0.1 | | D21 | Compact group forms are accepted for repetitive policy rules and bridge exposes, but they desugar to the same canonical AST as repeated one-line declarations | Sema programs will be token-heavy around policies, examples, and membranes; compact blocks reduce noise while preserving local diagnostics, formatter stability, and compiler-visible boundaries | Significant-layout magic across unrelated declarations; hidden bridge aggregation across languages; separate semantics for compact forms | | D22 | Configuration, CLI args, and dependency injection are native declarations with typed provenance, lifetimes, and compile-checked graph resolution | ML and governed-agent programs drown in parameter plumbing, config overlays, and runtime service wiring; making these library conventions hides model sampling settings, environment/CLI sources, singleton lifetimes, and authority-bearing constructors from the compiler | Python `argparse` plus globals; string-key DI containers; Spring-style ambient singletons; reading env/config anywhere in application code | | D23 | Tap collectors are native: `collector` declares typed aggregation channels and reserved `|>` records the left value while returning it unchanged | Experimentation, plotting, tracing, and MLOps need pervasive capture of scalars, tensors, strings, and objects; if capture is hand-written logging or overloaded pipe magic, it becomes control-flow noise and a source of run-breaking bugs | Overloadable pipe operator; ad hoc logging calls; unbounded in-memory metric lists; plotting libraries monkey-patching values | | D24 | Native parallelism uses one contextual `parallel` syntax, typed `=>` lambdas, deterministic merge defaults, and optional `worker` profiles; `parallel [comprehension]` replaces the redundant `par` alias | Data-parallel comprehensions, transforms, searches, reductions, streams, and model batches should share one language construct with effect inference, policy inheritance, cancellation, collector propagation, and compile-time race diagnostics; a second spelling adds vocabulary without adding semantics | Raw threads/futures/async plumbing as the primary surface; a `par` alias; GIL-style global lock; unordered-by-default parallel maps; implicit auto-parallelization without a visible marker | | D25 | Modules and visibility are native: Pythonic `import`/`from...import` against manifest package roots, `pub` per declaration, module-private default; module = attachment unit for assure/policy/monitor budgets (§5.18) | "Public signature", module-level `assure`, GOVERNANCE's policy layering, and verification cache keys all load-bear on a module concept the spec previously left undefined; Sema-to-Sema imports cannot be outsourced to bridges | Python runtime import semantics (`sys.path`, `importlib`); wildcard imports; file-scope visibility; implicit re-export | | D26 | `dict[K,V]`/`set[T]`/comprehensions/slicing native and homogeneous; one `Iterable`/`Iterator` protocol for `for`/`parallel`/`Stream`; dict/set canonical flattening in sorted order (§3.1) | The Pythonic-surface bet guarantees LLMs emit dict literals and comprehensions on day one; collections cannot live across an FFI bridge without losing trust labels, policy meet, and flattening; order-independent flattening is a Sema-specific replay/embedding obligation | Heterogeneous collections (Codon divergence list); library-only collections via bridges; JSON via stringly subscripting instead of typed `JsonValue` boundaries | | D27 | Methods in `struct`/`enum` bodies; traits with laws-as-contracts, header or `impl` conformance, coherence rules; `Semantic` is a trait, "protocol" exclusively means session types (§3.9) | Trait laws make obligations like reducer associativity `assure`-checkable instead of asserted; FFI adapters and prelude conformance need out-of-line `impl`; the Semantic-vs-`protocol` naming collision was unflagged in-doc | `class` retention; structural duck typing; blanket impls/specialization in v0.1; separate ad hoc mechanisms for iteration/hashing/associativity | | D28 | Bindings immutable by default with `mut` opt-in; value semantics for structs/collections; invariant re-check on guarded-field writes; mutation re-labels trust by meet (§3.8) | The trust lattice and contracts sit on the binding model; without stated mutation semantics, label laundering through aliasing and stale-invariant aggregates are unfalsifiable; value semantics is what makes the no-GIL capture rule sound | Pervasive shared mutability (Python semantics); Rust-grade borrow checking (cost unjustified for the target audience); immutable-only purism (hostile to the ML authoring base) | | D29 | Events are native: `event` payload declarations, `emit` under an `event.emit` effect, static `subscriber` declarations with bounded queues, journal-integrated exactly-once-per-run delivery; prelude lifecycle events (`Alert`, `HealEvent`, …) use the same construct (§5.19) | The corpus improvised eventing three ways (ambient `alert`/`quarantine` sinks, watcher tasks with manual `cancel`, approval polling); harness programs are event-driven, and pushing eventing through bridges forfeits trust labels, policy meet, replay, and structured cancellation — the four properties Sema exists for; `monitor` must stay statistics-only or its anytime-validity story dies | Callback/listener registration APIs; unbounded or fire-and-forget queues; `monitor` doubling as pub-sub; dynamic runtime `subscribe()` in v0.1 (reserved, Q12); in-core cross-process brokers | | D30 | No unwinding exceptions: failures are `Error`-trait values in `Result`/sums, handled by generalized `expect`/`except`, propagated by blame- and trust-preserving `?`; `unwrap` is a checked abort, rejected under `assure gold` (§5.20) | Principle 2's "cannot flow into non-handling code" requires a defined handling construct; unwinding is invisible to effect rows and hostile to replay and Findler–Felleisen blame; 14 typed error values existed with no general catch | Python `try/raise/finally`; Go tuple returns; error codes; exceptions-as-control-flow | | D31 | No colored functions: `async`/`await` do not exist; concurrency is structural (`scope`/`spawn`/`parallel` over non-blocking effect handlers); async surfaces appear only in foreign SDK shells at the membrane | The runtime is already non-blocking under structured concurrency (RUNTIME §4); a vestigial `async` grammar token invited LLM emission of an unspecified construct, violating the constrained-decoding story | Vestigial `[ "async" ]` in the def production; asyncio-style user plumbing; function coloring | | D32 | One `with as x:` scoped-binding construct unifies resources (`Scoped` trait), policy scoping, and model rebinding; deterministic journaled release; no user destructors (§5.21) | Resource lifecycle was stepped in by the SQL section ("the connection") with no acquisition/release story; effect-handler scoping is the mechanism the runtime already uses, and nondeterministic finalization breaks replay | Python context-manager dunders; RAII destructors; `defer` statements | | D33 | No `schema` keyword — the `struct` is the schema; compiler-derived wire schema artifact (JSON Schema + decoding grammar); `parse[T]`/`decode[T]`/`serialize` prelude surface with a round-trip law; one wire mapping for decode, `state`, journal, events, and bridges; runtime-owned staged decode-and-repair ladder (syntax → shape → types/refinements → semantics) with minimal-diff field patching, bounded by `retries` + `budget`, oscillation-detected, `RepairExhausted` on exhaustion (§5.22) | One source of truth per shape (D16); structured-output repair belongs to the runtime, not user try/catch round-trips (BAML schema-aligned parsing [04 §2.2](./research/04-ai-native-languages.md); Apple constrained decoding [04 §2.1](./research/04-ai-native-languages.md)); intrinsic self-repair needs external grounded feedback ([arXiv:2306.09896](https://arxiv.org/abs/2306.09896)); DSPy Assert deprecation shows library-level retry fails ([04 §2.3](./research/04-ai-native-languages.md)) | Separate `schema` declarations (Pydantic-model drift); exception-driven parse APIs; unbounded retry loops; retry decorators invisible to effects/budgets/policy/replay; a second ad-hoc serializer per subsystem | | D34 | Authored `test` declarations are native verification entry points (`test "name": block`): statement-position `ensure`/`check` as the assertion vocabulary, record-replay execution under pinned seeds, excluded from release codegen, gated by the same mutation-adequacy lint as synthesized tests; red-verdict counterexamples materialize back into `test` declarations (§5.7) | Every mainstream language ships native test entry points (Rust `#[test]`, Zig `test`, Go); Sema's verify engine needs a first-class authored-evidence leg, and reusing contract clauses as assertions keeps one semantics for all expectations; D6 unchanged — verification stays default-on and weak authored suites cannot launder green (EvalPlus, [arXiv:2305.01210](https://arxiv.org/abs/2305.01210)) | Reintroducing opt-in `testable` (D6); a separate assert/matcher DSL; library-convention test discovery (pytest-style name magic); fixtures/parameterized-test machinery in v0.1 (trait `law`s + L1 generators cover property-shaped needs) | | D35 | Semantic assertions are the statement-position contract forms, no new keyword: hard = `ensure semantics(...)` / any calibrated coercion in ensure position (calibrated-only, `ContractViolation` with judge evidence, joins union-bound α accounting, monitor-or-decay applies); soft = statement-position `check semantics(...)` (graded `Sim` evidence, never blocks); `assert` is a reserved, rejected token with a machine-applicable fix-it to `ensure`/`check` (§5.4) | One assertion semantics for deterministic and semantic predicates keeps contracts, tests, repair (R3), and monitors on the same machinery; Python `assert` strips under `-O` and unwinds, so a partial alias would teach authors and code-emitting models the wrong semantics; a targeted fix-it diagnostic is the LLM-ergonomic correction channel (TOOLCHAIN P3) | A native `assert` keyword aliasing `ensure`; Python-compatible `assert expr, "msg"`; a matcher/expectation DSL; debug-only unchecked assertions (guarantee-map dishonesty) | | D36 | Reflection is read-only over sealed ABI artifacts (`reflect(T)` → `TypeInfo` with descriptors/contracts/rows/judges/wire schema; `Semantic` + serializable + build-stable prompt rendering, so reflection splices into any template/context); staged code is native typed data: `Code[T]` typestate with `T`'s effect row as the static bound, `compile()` = pure resident-compiler admission (endorses `untrusted → validated`, never `trusted`), `run()` = `code.exec()`-gated execution on a fuel-metered tier-0 interpreter with dynamic `EffectViolation` enforcement and contract membranes; guarantee ceiling `checked`/`best_effort` at `run` sites; `Code[T]` never mutates the program (§5.23) | The user-facing ask ("generate and run code without a build") decomposes into always-on analysis (P1's resident query engine, <100 ms warm path) + optional codegen (tier-0 interpreter vs Cranelift is a scheduler choice); §3.5's `code.exec`-needs-explicit-grant door was designed for exactly this customer; rows-in-function-types (§3.1) make dynamic code statically bounded; D10/D14 stay intact because staged values are data, not source mutation | Python `eval`/`exec` (unbounded, invisible to effects/replay); mutating reflection / monkey-patching (breaks ABI, constrained decoding, static tooling); trusting staged code after N green runs; making every staged run pass the full heal gauntlet (kills interactive latency; the gauntlet stays the *persistence* bar) | | D37 | Error-flow ergonomics without try/catch/finally: the flat mapping (try→`expect`, catch→`except` arms, finally→`with`, rethrow→`?`, repair→`supervise`/decode-repair, delegate-to-party→`emit`) plus prelude combinators `.or`/`.or_else` (discard journaled as handled-by-default), `.map_err` (membrane conversion), `.context` (readable propagation frames); nested `expect` beyond two levels is a style lint (§5.20) | The cascade pain is real but is a *shape* problem: unwinding handlers force nesting, flat typed arms + one-character propagation don't (Rust `?`/anyhow-context and Zig `errdefer` precedents); cleanup-in-handlers is the finally bug class `with`'s deterministic release already kills (D32); origin tracking must be journal-native, not wrapper-object convention | Reintroducing `try/catch/finally` (D30 unwinding rejection stands); Go `if err != nil` manual plumbing (the cascade tax in another shape); silent `.or` defaulting (evidence loss); exception-translation macros | | D38 | `service` = typed remote interface, the fourth membrane: signature-only methods over wire-mappable types, derived `net.connect()` rows (remoteness visible, policy-confinable, rows as upper bounds so in-process `bind` needs no refactor), §5.22 wire ABI both directions with contract blame across the wire, handshake keyed on wire-schema artifact hashes (`VersionSkew`, never silent coercion), `Remote(E)` carries the peer's typed error with blame/origin/journal-ref intact, `@idempotent`-gated transport retry, defect-list round-trips between Sema peers, `repair` only for generative peers, deadline propagation (§5.24) | RPC seamlessness and honesty are separable: call sites read like module calls while effects, deadlines, and partial failure stay in the types — the classic distributed-systems lesson (CORBA/DCOM location transparency hid exactly what kills you); the wire machinery already existed (§5.22), services just make it the ABI; interface-in-language / transport-in-runtime is the same division D29 drew for events | Invisible location transparency; stringly REST/JSON clients; in-language transport bindings (HTTP framing, discovery, mesh — deployment concerns); exactly-once promises; a distinct IDL file (the `struct`+`service` declarations *are* the IDL — one source of truth, D33's logic) | | D39 | First-class streams: one `Stream[T]` type with three producers (`stream def` generators with `yield`, `parallel stream` stages, service streaming methods) and one consumer protocol; the unit doctrine (element type = unit of meaning, transport unit = runtime-owned framing/batching/chunking); affine scoped stream values; fallibility in the element type (`Stream[Result[T, E]]`) with the terminator law (broken ≠ finished, one terminal `Err`, never a silent stop); wire rule (`ServiceError` convertible into `E` at service boundaries); windowing adapters (`window`/`batch`/`take`/`lift`/`collect`) as the re-unitizing surface; element-granular `decode[Stream[U]]` and `simulate stream def` with per-element ladder + α; bounded-memory law O(queue + window); pull-based credit backpressure (§5.25) | Unbounded and huge data (audio, video, token streams, datasets) must flow without materializing, and the unit question has a principled answer: types carry meaning, the runtime carries bytes (Arrow batching, chunk reassembly — RUNTIME §8.2); pull + credits gives backpressure by construction (reactive push retrofits it); affine frames + pull-order journaling answer Q10's replay objection; the element-type error channel makes "can this pipe break?" a type-level fact | Push-based Rx-style reactive surface; `async` generator coloring (D31 stands); user-visible byte chunking; `Channel[T]` as the stream surface (Q12); exactly-once element delivery; implicit blanket fallibility wrappers | | D40 | Native debugging as a journal view: `breakpoint` = marker-not-effect (zero row impact, inert unless a session attaches; attach is the governed, journaled act), `breakpoint when expr`/`when semantics(...)` semantic breakpoints (judge on the session's budget, no α obligation — observation never gates dataflow), typed prompt-ready `DebugSnapshot` (trust-aware redaction; same value for DAP humans, healing loops, `sema doctor`, and LLM handoff), always-on per-stage pipeline counters + debug-profile drop digests (`sema debug why ` = "which filter ate my element"), session-side stage breakpoints, post-mortem time travel over the journal with backwards stepping as cursor moves, state edits fork a debug-tainted branch excluded from evidence (§5.26) | The journal already records the dominant nondeterminism (model calls with prompt/seed/output) — TOOLCHAIN §6.1's Replay.io-position substrate — so omniscient, deterministic, post-mortem debugging is a view, not new machinery; pipeline debugging pain is a provenance problem (labels + lineage), not a stepping problem; snapshots must be model-consumable because the healer and doctor are LLM consumers of the same state | printf-and-rerun on stochastic programs; debug builds that change semantics; effectful breakpoints that poison rows and purity; unredacted snapshot export; debugger mutation as evidence-preserving; bespoke debugger protocols over DAP | | D41 | Logging/console native: a log record is a typed prelude event (`log.Record`) on the §5.19 bus, journaled; `log.*`/`print`/`alert` prelude calls with normative levels, automatic module-path namespacing, deferred rendering; two-tier masking on by default (sound label-driven redaction + best-effort credential scrubbing, disabling = journaled policy grant); zero-config profile defaults (pretty console dev, rotated JSONL server) rendered via the §5.22 mapping; routing/interception/OTel purely by config + `subscriber` — redirection is routing, never redefinition; `@log`/`@trace` decorators for inline-free function logging and journal spans; `observe.record`/`observe.export` reused, no vocabulary growth (§5.27) | Logging is every language's afterthought tax (primitive → framework → masking bolted on); making records events inherits interception, replay, bounded queues, and export instead of reimplementing them; credential safety must be default-on and honestly tiered (labels are sound, patterns are not); the §5.16 exporter machinery and §6 journal already own transport and OTel projection | `printf` as the primitive; logger-object DI frameworks; monkey-patchable `print`; string-first records; OTel-native internal representation; a second serializer/config system for logs; regex masking sold as sound | | D42 | Native mathematical formalism via ONE construct: `equation` blocks where math notation is the syntax (decl form + inline statement form), Unicode + ASCII spellings token-equivalent, pure by construction (`!{}` row, no generative/effectful calls), `^`=power inside blocks only; quantifiers over finite domains, big operators, forward-autodiff `∇`/Jacobian/Hessian, numeric `∫`/`lim`/`Fix`, `argmin`/`argmax` with `s.t.` constraints, sets/logic/linear-algebra/probability kernels lowered to native Rust; iterative-solver results typed `Approx[T]` with provenance; atlas operators without v0 kernels = typed `math.NotImplemented` at compile time (§5.28, FUNDAMENTAL_MATHEMATICAL_OPERATORS.md) | Papers-to-programs without rewriting is a real adoption wedge for the robotics/dynamics forcing function; one block keyword scales to the whole operator atlas where keyword-per-operator cannot; purity makes equations the deterministic column (fuse/parallelize/differentiate freely, verify cheaply); honest approximation typing prevents laundering solver output as exact math | Keyword-per-operator vocabulary explosion; runtime-parsed LaTeX strings; CAS-by-default symbolic semantics (Q19); implicit multiplication; global `^` repurposing | | D43 | Ergonomics cluster (§5.29): `lambda p: e` alongside `=>`; one `*args` (tuple) + one `**kwargs` (dict) per signature, typed and in the public signature; `...expr` spread into list/set literals and call positionals (syntactic, not a value); generic `[T]` params on def/struct/enum/impl, **erased at runtime** | The Pythonic-surface bet requires idiomatic variadics/lambdas/spread on day one for LLM emission; generics add signature expressiveness + tooling without a second guarantee regime (contracts + effect rows remain the guarantee story), so erasure is the honest v0.1 choice | Block-lambda syntax; positional-only/keyword-only markers; reified/monomorphized generics (defer to AOT backend); `**`-unpacking at call sites | | D44 | Semantic operations first-party (§5.30, SymbolicAI lineage): the `~` sigil family — `~[query]` subscript, `~=`/`~!=`, `~<`/`~>`/`~<=`/`~>=`, `~in`, `~+`/`~-`, `~and`/`~or`/`~xor`/`~not` — all deriving `model.invoke`; a `semantic` namespace of primitive verbs (filter/rank/map/extract/summarize/translate/classify/query/combine/correct/unique/similar/select); a **coercion protocol** (`embed`/`sem_text` methods let a type pick its own representation, so `image_a ~= image_b` is vector cosine); a scoped `with pipeline(pre=[..], post=[..])` running preprocess → infer → postprocess → validate with a bounded self-repair loop reusing the §5.22 ladder; strict view default, semantic view marked. Sigil hygiene: bitwise NOT respelled `bitnot`, strict `xor` added, so logic gates stay complete at strict/bitwise/semantic tiers | SymbolicAI's core innovation is Sema's reason to exist but cost a Symbol wrapper + `.sem`/`.syn` modes + ~60 processor classes + never closed the validation loop; marking the *operation* keeps model calls legible; the coercion protocol is the honest form of SymbolicAI's implicit auto-casting (the type decides, the operator adapts, a step may itself call a model); reclaiming `~` for semantics forces (and clarifies) a complete three-tier logic story | Magic `Symbol`/mode flag; silently semanticizing strict operators; ~60 processor classes; validation-as-exception without feedback (the SymbolicAI gap); overloading `~` for both bitwise-NOT and semantics | | D47 | Real model backend (§5.33): `sema-model` crate — pure-Rust local GGUF inference on candle, GPU via Apple Metal (CPU fallback), no Python; `sema infer` CLI subcommand; behind the `real-model` cargo feature so default builds link no ML stack; the built-in deterministic engine is the explicit hermetic opt-in (`[engine] deterministic = true` / `SEMA_DETERMINISTIC=1`, RUNTIME §2.2) and never a silent fallback for a configured real backend, the real engine is what you point at a downloaded model | The deterministic engine needs a real counterpart to be credible; candle keeps it pure-Rust/single-binary (no PyTorch/GIL); feature-gating preserves fast portable default builds; verified end-to-end on an M3 Max (TinyLlama-1.1B loads on metal-gpu, generates coherent text) | Python/PyTorch bridge; linking candle by default (compile cost + portability loss); a bespoke inference kernel instead of GGUF+candle | | D48 | Explicit stdlib imports (§5.35): library modules (`math`, `io`, `http`) require an `import`; effect capabilities (`fs`, `net`, …) stay ambient because the `!{...}` row already declares them; `log` stays an ambient diagnostic like `print`; missing import is a NameError with a hint, not a silent stub; `import x as y` aliases the module | Two orthogonal axes — API surface (import) vs authorization (effect row); explicit deps are legible and let an optimized impl be swapped in behind the name; erroring (vs permissive stub) surfaces real dependency bugs | Importing effect verbs too (redundant with effect rows); requiring `import log`; permissive fallback for a missing import | | D59 | The `sema` package manager (§5.45): `sema add/remove/list` uses pinned uv 0.9.17 + CPython 3.12.12 + fixed PyPI, accepts exact direct `name==version` only, requires complete hashes and wheels, and failure-atomically commits the project-local venv/lock/tool metadata/manifest/config; remove rebuilds the whole remaining lock and list validates it without pip. Three local Python distribution candidates pass sdist-rebuild/install smokes but are neither reserved nor published | Ecosystem access requires reproducibility and provenance, not a permissive pip wrapper; one staged full-state transaction prevents resolver, environment, and config drift | Pip fallback; URLs/VCS/ranges/floating versions/source builds; ambient resolver configuration; partial uninstall; claiming universal compatibility or an unpublished channel | | D60 | Native Sema packages (§5.46): one `sema add ` transaction bounded-copies a symlink-free `sema-pkg.toml` + `src/*.sema` package into private `.sema/packages/` state and atomically couples directory + manifest; remove does the same. VCS/URL, hosted registry, mixed native/PyPI, and multi-native transactions reject until their provenance/atomicity contracts exist | Sema needs first-class native packages without treating an unverified transport as package identity; reuse the existing import resolution | Python-only manager; unpinned `git+`; path escapes/symlinks; multi-source partial commits; vendoring into `src/`; a bespoke module scheme | | D61 | Native embeddings via candle BERT (§5.43): `[models] embed` = an HF repo id + real-model feature → `~=`/similarity/`embed()` run on a real candle BERT model on the GPU, zero Python; runtime resolves only bounded pre-fetched cache artifacts into private snapshots and fails typed when configured artifacts are absent/invalid; an unconfigured capability keeps the built-in hash embedder; one `embed_seam` | The most-used capability (semantic ops) deserves a real model; proves the seam for a second, architecturally-different model without granting runtime download/cache-write authority; verified real semantics (related 0.62 vs unrelated 0.0) | Hash-only embeddings; runtime downloads; a bespoke embed path; making it default (gated) | | D62 | Documentation via reflection (§5.47): **docstrings** (triple-quoted string as the first statement of a module/def/struct/enum, dedented like cleandoc, raw so LaTeX survives) + `sema doc` reflecting the AST (signatures/params/returns/effects/fields/variants) → Markdown; prose carries Markdown/LaTeX/admonitions/examples; `--skills` emits skill frontmatter so docs load as model context, `--html` renders with KaTeX | Docs must not drift (reflect them); a docstring costs no per-line marker and headings/paragraphs are plain Markdown; unlike a comment it's a real runtime-reflectable value (the debugger's self-repair substrate); Pythonic | `##` per-line comments (token-heavy, no heading/paragraph split — user rejected); `#!#` fenced comment block (still per-line `#`, not reflectable); a doc DSL; hand-maintained tables; human-only docs | | D63 | `trace` keyword (§5.48): on a caught/uncaught error the runtime captures it + call frames; `trace(e)`/`trace()` reflects the frames' functions (signatures/effects/docstrings) into a `Trace` (`.kind/.message/.frames/.interfaces/.report/.markdown`); uncaught errors auto-print the `.markdown` repair packet | Debugging must be first-class for models, not an afterthought; shares the §5.47 reflector so an error carries interfaces + intent, not just a line; a keyword (like `traceback`) beats a library call; the stack trace a user sees is already the agent's self-repair context | A plain-string stack trace (no interfaces/docs); a library fn; exceptions/unwinding (errors are typed values §5.20); print-only-on-uncaught (programs need it mid-flight to self-heal) | | D64 | Debugger: `sema repl` (interactive console — expressions/persistent defs, `:doc` reflection, `:trace`) + `sema dap`/semad (DAP server: breakpoints, step over/in/out, call stack w/ positions, Locals per frame, `evaluate` via the real evaluator) + VS Code `sema` debug type; single-threaded re-entrant pause, zero cost when detached (§5.48) | An IDE debugger + REPL are table stakes; re-entrant on the existing tree-walker avoids making values `Send`; `evaluate` reusing the interpreter means inspected == executed; shares the reflector so a stop carries the same context as `trace` | A separate debug interpreter (would drift from the real one); a threaded adapter (Rc/RefCell values aren't `Send`); a bespoke wire protocol (DAP is what IDEs speak) | | D65 | Sequence correctness (bug-fix pass): Python-style slicing `xs[a:b:c]` (negative indices, clamping, negative step, step≠0) on lists/strings/tuples; `sorted`/`min`/`max` order numbers numerically and strings lexically and raise `TypeError` on mixed / `ValueError` on empty (no more treating non-numbers as 0.0); undefined names strict — a bare undefined *value* is a `NameError`, permissive extern stubs only in *call* position | Slicing is table-stakes Pythonic; silent mis-sorting and NaN-from-`0.0` are hidden errors; a typo'd value must not silently become a callable | No slicing (a real gap); numeric-coercion sort (mis-orders strings, hides mixed); stub-all-undefined (hides typos) | | D66 | Prompt-composition debugging (§5.14) + width casts + streaming + multimodal: `Prompt.warnings`/`.notes`/`.debug`/`.roles` (hard lints auto-journaled, advisory notes on demand); real reduced-precision width casts (f16/bf16/f8, i8/u8/… round through the format); `generate_stream` live token streaming; `compose(messages)` resolving image/audio to text via the config seams | Wrong prompts must be visible before the call; widths must be observable for ML; users must see partial output; a text model should still "see/hear" via the framework's small on-device models | Opaque prompt strings; cosmetic width types; block-until-done generation; requiring a multimodal model for any image/audio | | D67 | Model scheduler (§5.50): `generate_batch` distributes requests across one warm local instance plus at most eight remote API endpoints; remote shares run concurrently across bounded threads, local work stays on the main thread; round-robin, order-preserving, at most 32 prompts/flush; in-process HTTP(S), zero redirects, strict endpoint/effect policy, five-second/256-KiB per-call bounds, strict single-terminal-assistant schema, aggregate budget preflight, attempt metering, and typed atomic failure | Batching/distribution must be automatic (substrate, not a user thread API); the single-threaded interpreter still parallelizes I/O-bound remote calls; remote authority, resource use, accounting and partial failure must remain explicit | Exposing threads/queues/futures; process-per-request or subprocess `curl`; async-colored API (D31); redirects; dropping or replacing failed remote calls silently | | D68 | Static type checker (§3.1) + verification engine (§5.7) + constraint solver (§5.51): `sema check` catches arity/field/literal/return type errors conservatively (both sides certain, zero false positives); `sema assure` runs `test` blocks, fuzzes `ensure` properties (counterexamples), mutation-tests at gold; `solve:`/`solve all:` finite-domain backtracking. Contract-depth guard stops self-referential-property recursion | The language claims static typing + default-on verification + neurosymbolic — these make all three real; conservative typing avoids false positives; a self-contained FD solver covers discrete search without an SMT dep | A dynamically-only-checked "static" language; `assure` that only lints effect rows; neurosymbolic claimed on `~=`/CAS alone without discrete search | | D69 | Custom capability providers (§5.52): a `@provides("cap")` Sema function overrides any model backend (embed/generate/transcribe/caption/ocr/vqa); seams select a registered provider definitively, otherwise native candle then default; provider bodies wrap Python/native/HTTP so no Rust reimplementation; the re-entrancy guard may reach the configured lower backend only after its own effect/policy authorization; provider failure or invalid output is typed and terminal | Users must extend/override backends in Sema, not Rust; a decorator is reflected + typed + effect-carrying (vs a config string); selecting a provider grants no implicit fallback authority | Rust-only backends; config-string-only indirection; silent provider-fault swallow or fallback; recursive provider dispatch | | D70 | User-defined decorators (§5.53): any Sema function is a decorator — `@name`/`@name(args)` wraps a def; the decorator is `def d(fn, args, ...) -> any` and proceeds with `call(fn, args)`; stacks bottom-up; can transform/short-circuit; aspect decorators (policy/container) still apply on the inner fn; `Value::Decorated` chain built at load time. Applies to top-level, nested, AND struct/enum methods (method sees explicit args; self+fields bound in scope; mutation persists) | Users need their own decorators (memoize/retry/authorize); the `(fn, args)` around-advice protocol fits the runtime (no `*args` closures needed); load-time rebind keeps it reflected + type-checked at call sites; `call` doubles as dynamic dispatch; methods wrap a receiver-bound closure so the same protocol works uniformly | A fixed built-in decorator set; Python `dec(fn)->fn` closures (Sema lambdas are single-expr, no varargs); a dedicated decorator type; top-level-only decorators | | D71 | Effect-operation calls are checked (§3.6): calling an unrecognized op on a known effect namespace (`fs.raed(...)`) raises `NameError` at the call site instead of journaling + returning None; each namespace has a recognized callable surface (superset of the canonical §3.6 vocabulary). Effect *rows* stay open (`!{fs.raed}` still parses) | A silent None on a typo'd effect call was the last silent-ignore; a call must name a real op like any builtin, while capability declarations stay extensible | Closed effect-row vocabulary (rows must stay open/extensible); keeping the silent-None boundary; erroring on unknown *namespaces* too (left to the generic boundary) | | D72 | Effect namespaces are fully real + configurable (§3.6): `path`/`fs`/`env`/`memory`/`proc`/`code`/`ui` via std; `net.*` real HTTP+HTTPS via ureq/rustls with a full options bag (`headers`/`bearer`/`auth`/`query`/`timeout_ms`/`retries`/`retry_backoff_ms`/`redirects`) and `request`/`fetch` returning `{status,headers,body}`; `db.*` real embedded SQLite by default, selected by a `[db] url` DSN (`sqlite://`/`:memory:`/path) or `[db] path`, or fully replaced by a `@provides("db")` backend (`(op, sql, params)`) for Postgres/MySQL/REST (ready psycopg/mysql bridges shipped in `stdlib/py/`) | "No stubs" — every effect performs its real operation; users must be able to swap the HTTP knobs and the SQL server without editing Rust, so backends plug in via config + the existing provider pattern, and the common Postgres/MySQL glue ships pre-written | Feature-gating TLS/SQL (default build would stub); a fixed SQLite-only db; a body-only HTTP client with no retry/redirect/header control; a bespoke db-driver registry instead of reusing `@provides` | | D58 | Persistent Python worker + object handles (§5.44): one warm Python process reused across calls; non-JSON results (numpy arrays, class instances, modules) become object handles; `obj.attr`/`obj.method()` dispatch natively to the worker; numpy/torch scalars coerced to values; worker protocol owns stdout so library prints can't corrupt it | Real class/type use (not just functions) is the "seamless" bar; a warm process removes the per-call reload cost; handle dispatch makes Python objects first-class Sema values | Subprocess-per-call (slow, stateless); functions-only bridge (no classes); coercing arrays to lists (loses methods) | | D57 | Sema→Python bridge (§5.44): `python.call(module, func, args)` runs real Python (JSON-marshaled), interpreter from config/env; underpins `native import python.x`; v0 is a subprocess, embedded CPython (PyO3) is the next increment behind the same surface | Reusing Python's ecosystem is adoption-critical (the swappable-library story); a working subprocess bridge proves the direction now; keeping the call site stable lets the transport upgrade to zero-copy later | Reimplementing Python libs; blocking on embedded-CPython before shipping any reuse | | D56 | Real model behind the config registry (§5.43): with `real-model` + `sema.toml [models] generate/tokenizer`, a real local GGUF model drives the agent loop + compaction through one `agent_generate` seam; project-relative artifacts are opened no-follow, bounded and privately snapshotted, the loaded instance is reused, and any configured load/inference failure is typed and terminal. An unconfigured generate capability fails typed (`ModelUnavailable`, D74); the deterministic engine is the explicit `[engine] deterministic = true` / `SEMA_DETERMINISTIC=1` opt-in, and every modality/capability plugs into the same rule | §5.38's registry must be real to matter; one seam keeps all capabilities uniform; verified end-to-end (real model on metal-gpu drives the loop); config-gated so default builds stay fast (no ML stack); explicit configuration must never be laundered into fabricated success | A bespoke path per capability; making the real model the default (build cost); path reopening races; falling back after configured model failure | | D55 | Persistent MCP sessions (§5.42): `mcp.connect`→handle, reuse across `mcp.tools`/`mcp.call`, `mcp.close`; live child owned by the runtime's session registry (not exposed to the program), killed on close/exit; one-shot string form retained | Spawn-per-call is wasteful in a loop; the runtime must own OS-handle lifecycle (leak-safe); back-compat keeps the simple case simple | Exposing OS handles to programs; leaking sessions; forcing sessions for one-off calls | | D54 | Native tool calling (§5.41): a Sema function *is* a tool — `tools.run(request, [fns])` introspects name/params/`sem`-doc into a schema and drives the agentic loop (execute real fns, feed results back); model-agnostic `` text protocol (open-source gold standard) with provider-native adapters behind the same surface; guardrails = bounded steps, unknown-tool/error recovery, same-call loop detection, tool-result truncation; MCP/skills fold into the same path; tool effect rows still apply | Tool calling is an afterthought everywhere — the function already declares name/params/effects, so introspect it; text protocol works on any model (native = adapter); guardrails are what every real agent needs; governed-function tools inherit effect-checking for free | Separate schema DSL; native-format-only (locks out OSS models); unbounded loop; dumping huge results into context | | D53 | Robustness / graceful degradation (§5.40): stream+tool ops are crash-proof by construction (char-safe truncation, saturating/clamped arithmetic) + a `catch_unwind` net; per-item failures (bad window, tool error, unknown tool, step-limit, call-loop) are recovered with a safe fallback; every degradation is journaled + printed to stderr (never silent); `SEMA_STRICT=1` turns them into hard typed errors for debug | A mid-stream error must never vaporize the session (the #1 user complaint); recover-and-surface beats crash-or-hide; a debug switch gives strictness without sacrificing production resilience; conservative token estimates avoid the dangerous under-count | Crash on a bad estimate; silent-drop; hiding recoveries; no way to make issues hard-fail in tests | | D52 | Native skills + MCP (§5.39): two stdlib modules — `skills` (load Markdown skills w/ frontmatter, merge into context, register to a model) and `mcp` (real stdio JSON-RPC client: tools/list + tools/call; `as_skills` adapts MCP tools into the same skill-registration path); back-compatible with existing skill/MCP formats; no new syntax | Every harness re-implements skill/tool wiring; capabilities are data + a verb, so they need no grammar; back-compat reuses the whole ecosystem; one uniform registration path (skills = MCP) keeps it simple | New syntax for skills/tools; a bespoke Sema-only skill format; MCP schemas as the top-level abstraction (D12: protocol types subsume them) | | D51 | Smart defaults + config layer (§5.38): built-in engines back the *grounded* ops with no config (hash-embed for `~=`/`embed`, extractive summarize for `stream` compaction); model-backed generate/simulate/judge need a `@provides` provider, a real GGUF (when linked), or the explicit `[engine] deterministic` opt-in, else they fail loud; optional `sema.toml` overrides engine params, stream compaction defaults, and a capability→model registry (embed/generate/summarize working; ocr/vision/stt/tts adapter-designed); `config.get`/`config.model`/`config.temperature` read it | Replacing the harness means good out-of-the-box behaviour AND full tunability; a declarative file is diffable/tool-readable/overridable without recompiling; a swappable registry (per D48) keeps every capability replaceable | Config only via code; mandatory config (kills out-of-the-box); a single hard-coded model | | D50 | Native long-stream compaction (§5.37): `stream` stdlib module — `fold`/`fold_file` (streaming fold with automatic budget-triggered compaction, O(window+budget) memory), `search` (semantic top-k over windows), `map` (per-window fn). Engine-driven compaction (real model summarizes; else the grounded extractive summarizer, no opt-in needed); model/context-size agnostic | The context-window problem is universal and harnesses re-solve it per-tool, outside any language and unusable on-device; making it a primitive gives constant-memory book-scale processing for any model in one call; measured 2.8M-token book → 127-token digest at 3.4 MB RSS | External-harness compaction (status quo); a syntax construct (grammar bloat); holding all windows (defeats constant memory) | | D49 | Opt-in bytecode VM (§5.36): tree-walker stays the reference/default; `SEMA_VM=1` runs compilable functions on a slot-based stack VM with function-granularity fallback to the tree-walker; value ops delegate to the same Interp helpers (fast path only where it provably matches); parity-tested whole-program incl. GraphRAG + cross-language; ~1.35–1.45× on interpreted compute | Beating CPython needs slot resolution + flat dispatch, not more builtins; partial-but-safe (fallback) lets it ship incrementally; delegating semantics guarantees no divergence; also the substrate for interop/transpilation | Replacing the tree-walker outright; a VM that reimplements value ops (divergence risk); defaulting to the VM before it's comprehensive | | D46 | Native tensors + stdlib bindings (§5.32): first-class n-dim `Tensor` (dense f64, CPU backend, accelerated backend swappable); NumPy/PyTorch-shaped elementwise ops + scalar broadcast + `matmul`, all shape-checked with typed `ShapeError` (dimension safety; static checker is Q20); `**` exponentiation added to the runtime (right-assoc, Int-preserving); host-stdlib bindings under namespaces — `math` (constants + elementwise funcs), `io` (fs/stdio), and native `list`/`dict`/`set` method sets; `embed(str)` -> vector; tensors bridge the equation engine both ways | Arrays are core to the code↔AI thesis, not a library afterthought; dimension safety belongs in the language (mismatches should be errors, not silent misalignment); binding the host stdlib avoids reimplementing libm/collections while keeping Sema syntax; `**` fills a real arithmetic gap without touching `^` (bitwise) | Tensors as a bridged third-party type; silent shape broadcasting; reimplementing libm/std collections; overloading `^` for power | | D45 | Symbolic algebra in equations (§5.31): a string literal in an equation is a symbol; arithmetic on a symbol builds a symbolic tree; verbs sym/simplify/expand/diff/factor/solve/subst; `diff` uses product/chain/power rules over elementary functions; `solve` exact for linear+quadratic, typed error beyond; symbolic values render back to the runtime as strings (sema-math/src/symbolic.rs) | The CAS side of the SymbolicAI vision made real; resolves Q19 for the univariate/elementary case; symbolic is opt-in (numeric stays default per D42) so no expression swell; bounding solve to linear/quadratic keeps it honest (no wrong-branch simplification) | CAS-by-default; free vars auto-becoming symbols; claiming general solving/integration |</sub>