Repository navigation
STD_LEAK slice (NanosecondDuration decomposition): std must be perfectly decomposed — a scale-fixed time alias hardcoded in std is a leak. Make std's realization/measurement framework (std/realization*.dag) scale-AGNOSTIC (generic Measure<Time,S,M>); relocate the NANOSECOND scale CHOICE + its reason - #5286
Conversation
…o verification Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Thanks — the finding is factually correct (the alias moved to M2 governs canonical / generic
DESIGN §3 is explicit on direction: "the dispatch that selects a realization is itself realization, so it sits peripheral … never in the interface." The realization/measurement framework stays scale-agnostic and central ( This relocation was the operator-directed resolution of exactly this §3-vs-M2 tension (relayed via parent smart-eagle-107), on the Milliwatt precedent. CI is green; M2 is a review-time heuristic, not a mechanical gate, and applying it to a scale-fixed consumer choice would equally have blocked the merged Milliwatt PR. If the M2 pre-scan should formally exempt "scale-fixed alias relocated to its consumer (parallel to Milliwatt)," that's a worthwhile follow-up to the scan's heuristic — but it does not make this diff a fork. — sent from loyal-deer-302 |
…aim only the arithmetic teeth The witness header claimed Milli-scale instantiations would fail to resolve/type-check if a roll-up fn stayed Nano-hardcoded. Execution-falsified by parent (smart-eagle-107): the <S> scale tag is a phantom type the substrate erases — re-hardcoding to Measure<Time,Nano,Nat> leaves the witness green with 0 dag-compile diagnostics (same no-where-clause substrate gap already cited for <M>). Reworded to assert only what bites (roll-up arithmetic composes off-Nano; perturbing it goes red) and to name the genuine guard as structural (a no-concrete-scale-literal lens), a documented follow-up. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…). Point timing carriers at std.verification and use cost_account_time_count; parameterize RealizationPlan/CostAccount with Nano for CI floor resolve. Co-authored-by: Cursor <cursoragent@cursor.com>
NanosecondDuration/nanosecond_duration moved from std.measure to std.verification (#5286); cost_account_time_nanos renamed to cost_account_time_count in std.realization_schedule; cost_account_measured replaced by cost_account_measured_from_time in std.realization_measurement. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
NanosecondDuration/nanosecond_duration moved from std.measure to std.verification (#5286); cost_account_time_nanos renamed to cost_account_time_count in std.realization_schedule; cost_account_measured replaced by cost_account_measured_from_time in std.realization_measurement. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
#5286 ("NanosecondDuration decomposition") relocated the nanosecond scale CHOICE out of std.measure to std.verification and made the cost ledger scale-generic (CostAccount<S>, RealizationPlan<S>, cost_account_time_count<S> replacing cost_account_time_nanos). #5225's realization_width.dag (landed concurrently) still imported the old names — a semantic merge-skew that left main's CI floor resolve RED (blocking every branch, since the floor scans the whole dsl tree). - nanosecond_duration now imported from std.verification (dropped the unused NanosecondDuration type import). - cost_account_time_nanos -> cost_account_time_count (scale-agnostic Nat count). - thread <S> through shard_balance_slot_for_cost / WidthBoundedRealization / width_bounded_realization / witness_width_fold_preserves_schedule_topology so CostAccount<S> / RealizationPlan<S> are well-formed; width never reads the ledger scale, so S only rides through. Verified: realization_width_witnesses() green by execution. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…). Point timing carriers at std.verification and use cost_account_time_count; parameterize RealizationPlan/CostAccount with Nano for CI floor resolve. Co-authored-by: Cursor <cursoragent@cursor.com>
* Ground Cargo package and dependency versions on SemVer carriers (extdeps/rust). Co-authored-by: Cursor <cursoragent@cursor.com> * Repoint Cargo versions to extdeps.version.semver (not std.types.SemVer). Adds slice-2 semver scheme inhabiting VersionIdentity/VersionConstraint from Co-authored-by: Cursor <cursoragent@cursor.com> #5311; CargoPackageVersion and CargoVersionRequirement alias through it. * Wire stage0/emit_cargo_toml through default_stage0_package_version authority. Adds render_cargo_package_header_prefix shared by emit_stage0_crate_manifest and emit_cargo_toml; witness exercises the emitter header path. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix realization_width imports after NanosecondDuration migration (#5286). Point timing carriers at std.verification and use cost_account_time_count; parameterize RealizationPlan/CostAccount with Nano for CI floor resolve. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: versioning model in extdeps * fix(cargo): ground min_cargo_version as CargoVersionRequirement Edition-2021 floor uses semver requirement wire text (>= 1.56), not a bare version identity. Witnessed in cargo_version_witness_test. Co-authored-by: Cursor <cursoragent@cursor.com> * Split min_cargo_version onto CargoToolVersionFloor carrier. Dependency requirements and cargo binary edition floors are distinct facts; branded CargoToolVersionFloor prevents RegistryDep misuse. Co-authored-by: Cursor <cursoragent@cursor.com> * Ground CargoToolVersionFloor on SemVerConstraint, not bare NonEmptyStr. Distinct brand preserves use-site separation from dependency requirements while staying on extdeps.version.semver authority (review 31090 nit). Co-authored-by: Cursor <cursoragent@cursor.com> * Remove duplicate Nano import from realization_width.dag. Rebase merge artifact; idempotent at resolve but noisy and flagged by review. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Cursor <cursoragent@cursor.com>
…5315) * extdeps/languages/go: Go module versioning model (go.mod authority) Adds `extdeps.languages.go.module` — the single authority for Go module system types (GoModuleVersion, GoModulePath, GoMajorVersionSuffix, GoLanguageVersion, GoToolchainName, GoRequireEntry, GoReplaceEntry, GoExcludeEntry, GoRetractEntry, GoModFile, GoMvsProperty) and the `go_major_suffix_str` derivation. Anchored on go.dev/ref/mod. Adds a by-execution witness (`go_module_versioning_witness_test.dag`) that runs GREEN against the 6 discriminating checks: filename string, v0/v1 empty suffix, v2 and v3 non-empty suffixes, suffix distinctness, and MVS properties list count. Run: true. Parallel to `extdeps/rust/cargo.dag` for the Go module system; the go_manifest_file scaffold in emit.dag is noted as a v1-seed §3 debt with dissolve-on marker. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * §2 decompose GoModuleVersion → GoSemVer; add go_semver_label + witnesses GoModuleVersion was a branded NonEmptyStr — anemic modeling per DESIGN §2. Replaced with GoSemVer {major, minor, patch, prerelease?, build?} (grounded atoms) and a canonical wire-label fn go_semver_label. Pseudo-versions remain a predicate on the prerelease field, not a type fork. All directive types (GoRequireEntry, GoReplaceEntry, GoExcludeEntry, GoRetractRange) updated to use GoSemVer. Scaffold note added for extdeps.version VersionScheme data row pending #5311. Witness count grows 6 → 12 (semver label witnesses cover release, v0, prerelease, build, combined, and distinctness), all green by execution. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: go module versioning model (extdeps/languages/go) * go module: integrate VersionScheme; split GoReplaceTarget coproduct - Add go_semver_to_version_identity (GoSemVer → VersionIdentity via label) - Add go_semver_compare (structural Int ordering, prerelease presence per semver §11) - Add go_module_version_scheme: VersionScheme data row (equality correct; ordering scaffold pending parse_go_semver — dissolve-on marker in file) - Dissolve obsolete #5311 scaffold comment (extdeps.version now on main) - Split GoReplaceEntry.target into GoReplaceTarget coproduct: ModuleRedirect { path, version } | LocalDirRedirect { path } — upstream replace RHS is structurally distinct (module target requires version; local dir target must not have one); collapsing them was §2/§3 violation - Extend witness test: go_semver_to_version_identity + 4 go_semver_compare probes (less/greater/equal/prerelease ordering); 17 witnesses, all green Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix(go): emit-host mins use go-directive wire form, not comparator GoLanguageVersion "1.22" + GoToolchainName "go1.22.5" for emit_host_transport bootstrap — not VersionConstraint ">= 1.22". Witnessed in module test. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix std.realization_width broken imports after main merge NanosecondDuration/nanosecond_duration moved from std.measure to std.verification (#5286); cost_account_time_nanos renamed to cost_account_time_count in std.realization_schedule; cost_account_measured replaced by cost_account_measured_from_time in std.realization_measurement. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com> Co-authored-by: Cursor <cursoragent@cursor.com>
root: LexRuleSet { - it would be nice to have a section for the resulting phrase (in text), and then associate them in a more cosmetic way (#5327)
* WIP: can we make modeled lex rules more elegant somehow? ModeledLexRules { ro
* WIP: can we make modeled lex rules more elegant somehow? ModeledLexRules { ro
* Pilot LexicalPhrase: single authority for bash fixed-token phrases
A fixed-token phrase was authored three ways that could silently drift: a
LexRuleSet of (token_class, literal-text) rules, a parallel ConcreteSyntaxToken
sequence repeating the same classes, and a whole-phrase source-text string equal
to the rule texts concatenated. DESIGN.md §2 horizontal: one concept, derive
every use.
std/compilers/lexing.dag: new LexicalPhrase carrier (ordered (token_class,
fragment) spans) + span/phrase constructors + phrase_to_lex_rules /
phrase_to_source_text projections. target_model.dag (which owns
ConcreteSyntaxToken; import arrow runs target_model -> lexing) gets
phrase_to_fixed_concrete_tokens.
bash.dag: the 7 pure-FixedToken phrases are each authored ONCE as a LexicalPhrase
whose fragment column reads as the shell text; lex/concrete_tokens/source_text
all project from it. Removes the bash_lex_rule helper and two LexRuleSet builders
(-463 lines in bash.dag). Bound-word phrases (bound_words/embedded_quote) stay
literal pending a binding-carrying span (T-6).
Verified by execution: all 11 bash_emit_command_test witnesses green (full
lex -> grammar-row -> byte-identical emit pipeline); a scratch oracle confirmed
each derived source_text is byte-identical to the literal it replaced and the
token classes project (with a discriminating non-member -> false).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* WIP: can we make modeled lex rules more elegant somehow? ModeledLexRules { ro
* Reconcile realization_width to post-#5286 scale-agnostic API
#5286 ("NanosecondDuration decomposition") relocated the nanosecond scale CHOICE
out of std.measure to std.verification and made the cost ledger scale-generic
(CostAccount<S>, RealizationPlan<S>, cost_account_time_count<S> replacing
cost_account_time_nanos). #5225's realization_width.dag (landed concurrently)
still imported the old names — a semantic merge-skew that left main's CI floor
resolve RED (blocking every branch, since the floor scans the whole dsl tree).
- nanosecond_duration now imported from std.verification (dropped the unused
NanosecondDuration type import).
- cost_account_time_nanos -> cost_account_time_count (scale-agnostic Nat count).
- thread <S> through shard_balance_slot_for_cost / WidthBoundedRealization /
width_bounded_realization / witness_width_fold_preserves_schedule_topology so
CostAccount<S> / RealizationPlan<S> are well-formed; width never reads the
ledger scale, so S only rides through.
Verified: realization_width_witnesses() green by execution.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* LexicalPhrase: left-to-right phrase_text authoring form
Per reviewer/operator: author each phrase so the resulting shell text reads
left-to-right like a sentence. phrase_text(text: [...], classes: [...]) — the
`text:` row reads L→R as the phrase, the `classes:` row names each fragment's
token class in the same order. Zipped into TokenSpans by zip_spans (typed over
FreeMonoid so match resolves Cons/Empty; List is an opaque alias to the matcher).
A text/classes desync surfaces RED in the emit witnesses, not a silent zip.
Projections (lex/concrete/source_text) unchanged — byte-identical output.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* Remove dead span/phrase constructors; rely on list ordering
The phrase_text authoring form builds spans via zip_spans directly, so the bare
span()/phrase() constructors had no callers. Drop them — authoring is the single
phrase_text(text:, classes:) form, paired by list order.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* WIP: can we make modeled lex rules more elegant somehow? ModeledLexRules { ro
* WIP: can we make modeled lex rules more elegant somehow? ModeledLexRules { ro
---------
Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
STD_LEAK slice: scale-agnostic realization/measurement framework + relocated nanosecond CHOICE
A scale-fixed time alias (
NanosecondDuration = Measure<Time, Nano, Nat>) hardcoded into the std realization/measurement framework is a §3 leak: the framework should name no scale; the scale CHOICE belongs at the consumer that owns the timing authority (parallel toMilliwatt, homed at its product consumer in #5235).What changed
Framework → scale-AGNOSTIC over
<S>:std/realization_measurement.dag— roll-up algebra (time_measure_{seq,par,is_zero,list_total,list_par},schedule_*critical_path*,cost_account_measured_from_*, the discriminating lens) now operate on genericMeasure<Time, S, Nat>; name no scale.std/realization_schedule.dag—CostAccount<S>,RealizationPlan<S>;cost_account_time_nanos→cost_account_time_count. Schedule-lens fns thread<S>(logic unchanged).std/realization.dag—RealizedStep<S>+ reconcile fns thread<S>(never inspect the scale).std/measure.dag— adds generictime_measure<S>; removesNanosecondDuration+ its constructors (the scale-fixed alias; dead_max/_min/_comparedropped, no consumer).NANOSECOND CHOICE relocated to the timing-authority consumer:
std/verification.dag— now definesNanosecondDuration+nanosecond_duration/_count, with the reason: the nanosecond decision EMERGES here because the timing authority is verification's (budget/measured nanosecond thresholds). Single authority.std/cache_interface.dag,product/compute_fabric.dag— import the alias FROMstd.verification(never re-coin Nano);compute_fabriccarries the "why ns" reason at the host wall-clock observation boundary (PerformanceReceipt).Magnitude
<M>staysNat(honest limitation)A magnitude-generic roll-up needs
+/maxover<M>, but algebra-inhabitance resolves only on concrete numeric nodes (no where-clauses) — the same documented substrate gapGroupCompletion<M>/Measureconstrained-inhabitance carry. Dissolution trigger: when parametric where-clause syntax lands, widen to<M> where M : CommutativeMonoid.§5 proof-by-execution
All affected witnesses green: keystone, schedule lens (load-bearing CI gate), critical-path, reconcile, cache-layer planner, realization, measure carrier. New witness
realization_scale_agnostic_test.dagexercises the full roll-up +CostAccount<S>at Milli scale; it bites on the roll-up arithmetic composing correctly off-Nano (perturbing it goes red). HONEST scope:<S>is a phantom type the substrate erases (no where-clause enforcement, same gap as<M>), so scale-agnosticism is NOT runtime/type-checked — the genuine anti-regression guard is structural (a lens asserting the framework modules contain no concrete scale literal), tracked as a follow-up, not delivered here.Approach approved by parent (smart-eagle-107), including the correction to home the alias at the consumer (verification) rather than keep it in measure.dag.
🤖 Generated with Claude Code