Skip to content
Merged
Show file tree
Hide file tree
Changes from 14 commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
287f4fb
docs(audit): subvalue bounded lattice claim
briansrls May 2, 2026
4abdf05
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
60658df
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
1734b9f
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
c49d4b1
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
3cc4994
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
094522a
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
4c6aff3
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
791813b
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
6c19da5
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 2, 2026
795ddfe
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
1d4aa93
WIP: snappy-koi-58
briansrls May 3, 2026
2b78d33
chore: apply cargo fmt
briansrls May 3, 2026
b6bb23d
WIP: snappy-koi-58
briansrls May 3, 2026
ad92101
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
f5fab4d
WIP: snappy-koi-58
briansrls May 3, 2026
2661617
WIP: snappy-koi-58
briansrls May 3, 2026
72daff4
chore: apply cargo fmt
briansrls May 3, 2026
3b486cb
WIP: snappy-koi-58
briansrls May 3, 2026
9a09f28
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
32b8584
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
44a82d8
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
19034d5
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
78e04e8
Merge remote-tracking branch 'origin/main' into codex/subvalue-bounde…
briansrls May 3, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -537,7 +537,7 @@ Surfaced by paired Exploratory Analysis (gpt-5-5-pro main@8cd5359; 9 findings ag

#### B. Exploratory findings — sharpened tracked items

- **`??` and `%` declared in dag-syntax authority but absent from v3 token/parser/operator surface** (sharpened from operator-ontology-three-coexisting-authorities at ROADMAP:424-425): `dsl/extdeps/languages/dag/syntax.dag:99-115` declares `OperatorSpec` rows for `??` (`NullCoalesce` binop) and `%` (`Mod` binop). v3's token taxonomy at `src/v3/std/tokenize.dag:15-60` has `Question` but no `QuestionQuestion`; has `Slash` but no `Percent`. Punctuation list at `:95-123` matches. `src/v3/compiler/parse_tables.dag:173-243` covers `||`, `&&`, comparisons, `+ - * /` but no `%` or `??`. v3 operator ontology at `src/v3/std/substrate.dag:223-253` has Add/Sub/Mul/Div + comparisons + And/Or; no Mod or NullCoalesce. `src/v3/compiler/operators.dag::from_symbol:5-18` no branch. The parse-table cross-validation comment at `parse_tables.dag:149-166` claims cross-validation against `dag_operators` — visibly violated. **Dissolution**: short-term either remove unsupported rows from `dag_operators` until v3 supports them, OR add the full chain (token + parse + OperatorKind + algebra-field mapping + lowering/inference) in one PR. Long-term: T-Ground-Services parser-grammar slice derives parser rows from syntax authority — concrete scope item for that lane. Surfaced 2026-05-01 (Exploratory Finding 4). Owner: R3 Substrate (operator ontology) + R3 Grounding (T-Ground-Services).
- **`??` and `%` declared in dag-syntax authority but absent from v3 token/parser/operator surface — RESOLVED 2026-05-03 (Grounding parser-grammar slice)** (sharpened from operator-ontology-three-coexisting-authorities at ROADMAP:424-425): unsupported `dag_operators` rows for `??` (`NullCoalesce` binop) and `%` (`Mod` binop) were removed from `dsl/extdeps/languages/dag/syntax.dag`; the v3-supported `.dag` binary operator set is now exactly `||`, `&&`, comparisons, `+`, `-`, `*`, and `/`, with `|>` / `.` remaining tokenized parser forms whose `binop` is `none`. Regression coverage now requires every `dag_operators` row with a binary `binop` to have matching `TokenKind` coverage, a `BinaryOpRow` in `src/v3/compiler/parse_tables.dag`, and an `operators.dag::from_symbol` mapping; tokenizer authority also rejects parser-only shared operators. **Future scope:** reviving `%` or `??` is additive, not debt cleanup, and must land the full chain together (token + parse + `OperatorKind` + algebra-field/lowering/inference semantics) after the R3 Substrate operator-ontology decision. Surfaced 2026-05-01 (Exploratory Finding 4); resolved by deletion + executable cross-validation gate.

- **`CollectionOps` / `StringOps` / `MapOps` duplicate algebra operation surfaces as target-string templates** (sharpened from language-fact-duplication / LanguageSpec-dual-authority at ROADMAP:365 + :424): `dsl/std/algebra.dag:301-326` declares `FreeMonoid<T>` carrying `concat`, `empty`, `length`, `map`, `filter`, `fold`, `flat_map`, etc. as algebraic operations; `:328-349` declares `PartialFunction<K,V>` carrying `lookup`, `empty`, `insert`, `merge`, `keys`, `values`. `dsl/std/languages.dag:281-318` then declares per-target `CollectionOps`, `StringOps`, `MapOps` records with `count: String` / `first: String` / `fold: String` / `empty_list: String` etc. — second operation ontology parallel to FreeMonoid + PartialFunction. **Dissolution**: realize operations should reference `DeclarationRef` / method contracts for algebra fields. Target templates can remain render-data, but identity is "realization of `FreeMonoid<T>.fold` for Rust", not a second `fold: String` field. Surfaced 2026-05-01 (Exploratory Finding 7). Owner: R3 Grounding (T-Ground-LanguageSpec + algebra method contracts).

Expand Down
8 changes: 3 additions & 5 deletions dsl/extdeps/languages/dag/syntax.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ import std.syntax {
ExprBody, BlockBody, TypeBody, ValueBody, NoBody,
ServiceBody, ResourceBody,
OperatorSpec, SyntaxSpec,
BinOp, Add, Sub, Mul, Div, Mod,
Eq, Ne, Lt, Gt, Le, Ge, And, Or, NullCoalesce,
BinOp, Add, Sub, Mul, Div,
Eq, Ne, Lt, Gt, Le, Ge, And, Or,
LiteralValue, LitBool, LitNull
}

Expand Down Expand Up @@ -92,12 +92,11 @@ data dag_non_name_keywords: Map<String, Bool> = {
}

// Operator precedence table.
// ?? < || < && < cmp < add < mul < |> < .
// || < && < cmp < add < mul < |> < .
// |> and . have binding power entries but their binop field is unused
// (the expression loop handles them as pipe/field-access, not binary ops).

data dag_operators: List<OperatorSpec> = [
OperatorSpec { symbol: "??", left_bp: 3, right_bp: 4, binop: NullCoalesce, algebra_field: none },
OperatorSpec { symbol: "||", left_bp: 5, right_bp: 6, binop: Or, algebra_field: none },
OperatorSpec { symbol: "&&", left_bp: 7, right_bp: 8, binop: And, algebra_field: none },
OperatorSpec { symbol: "==", left_bp: 9, right_bp: 10, binop: Eq, algebra_field: none },
Expand All @@ -110,7 +109,6 @@ data dag_operators: List<OperatorSpec> = [
OperatorSpec { symbol: "-", left_bp: 13, right_bp: 14, binop: Sub, algebra_field: none },
OperatorSpec { symbol: "*", left_bp: 15, right_bp: 16, binop: Mul, algebra_field: none },
OperatorSpec { symbol: "/", left_bp: 15, right_bp: 16, binop: Div, algebra_field: none },
OperatorSpec { symbol: "%", left_bp: 15, right_bp: 16, binop: Mod, algebra_field: none },
OperatorSpec { symbol: "|>", left_bp: 17, right_bp: 18, binop: none, algebra_field: none },
OperatorSpec { symbol: ".", left_bp: 19, right_bp: 20, binop: none, algebra_field: none }
]
Expand Down
2 changes: 1 addition & 1 deletion src/v3/compiler/src/regen_parse_tables_emit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ pub fn render_parse_tables_generated_rs(
/// - `And` ← bp 7/8 (`&&`)
/// - `Comparison` ← bp 9/10 or 11/12 (`== != < <= > >=`)
/// - `Additive` ← bp 13/14 (`+ -`)
/// - `Multiplicative` ← bp 15/16 (`* / %`)
/// - `Multiplicative` ← bp 15/16 (`* /`)
///
/// If the shared authority introduces an operator at a bp outside these
/// bands, regen fails closed (`BinaryOpLevel` does not yet cover it).
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ src/v3/std/effects.dag 53 97984 1acdbeaa68acfd2e
src/v3/std/emit_model.dag 43 77647 4b063e9a5ddc50a1
src/v3/std/extdeps_bootstrap_fixtures.dag 4 14463 909ca7a1c1705e89
src/v3/std/go_method_template_contracts.dag 5 110898 7eb5c9f1296f4a45
src/v3/std/induction.dag 56 88794 546f74c63c189c50
src/v3/std/induction.dag 56 88794 e405e1549cf2fe08
src/v3/std/integer_diagnostic_order.dag 6 8124 5d7b31594a5b3d5c
src/v3/std/lens.dag 6 9852 28d5539a5b28716e
src/v3/std/list.dag 19 40269 8c648d4a4fd05c21
Expand Down
24 changes: 1 addition & 23 deletions src/v3/compiler/tests/integration/sg1_tokenize_authority_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,6 @@ fn shared_operator_boundary_is_explicit_and_fail_closed() {
.collect();

let mut shared_tokenized_kinds = BTreeSet::new();
let mut parser_only_patterns = BTreeSet::new();
for pattern in &shared_operators {
match classify_shared_operator_for_tokenizer(pattern) {
SharedOperatorTokenizerBoundary::Tokenized { kind } => {
Expand All @@ -262,23 +261,9 @@ fn shared_operator_boundary_is_explicit_and_fail_closed() {
);
shared_tokenized_kinds.insert(kind.to_string());
}
SharedOperatorTokenizerBoundary::ParserOnlyDebt { reason } => {
assert!(
!reason.is_empty(),
"parser-only shared operator `{pattern}` should carry a dissolution note"
);
parser_only_patterns.insert(pattern.clone());
}
}
}

assert_eq!(
parser_only_patterns,
BTreeSet::from([String::from("%"), String::from("??")]),
"SG-1a banks exactly two parser-only shared operators today; changing that boundary \
must update the ratchet and the scaffold rationale together"
);

let mut covered_punct_kinds = shared_tokenized_kinds;
for decl in dag.declarations() {
let Some(name) = &decl.name else {
Expand Down Expand Up @@ -329,7 +314,6 @@ fn keyword_spelling_for_token_kind(kind: &str) -> String {

enum SharedOperatorTokenizerBoundary {
Tokenized { kind: &'static str },
ParserOnlyDebt { reason: &'static str },
}

fn classify_shared_operator_for_tokenizer(pattern: &str) -> SharedOperatorTokenizerBoundary {
Expand All @@ -348,15 +332,9 @@ fn classify_shared_operator_for_tokenizer(pattern: &str) -> SharedOperatorTokeni
"||" => SharedOperatorTokenizerBoundary::Tokenized { kind: "PipePipe" },
"|>" => SharedOperatorTokenizerBoundary::Tokenized { kind: "PipeArrow" },
"." => SharedOperatorTokenizerBoundary::Tokenized { kind: "Dot" },
"??" => SharedOperatorTokenizerBoundary::ParserOnlyDebt {
reason: "null-coalescing remains outside the v3 tokenizer punctuation subset",
},
"%" => SharedOperatorTokenizerBoundary::ParserOnlyDebt {
reason: "modulo remains outside the v3 tokenizer punctuation subset",
},
other => panic!(
"shared syntax operator `{other}` must be classified as tokenizer punctuation or \
explicit parser-only debt"
removed until v3 supports it end-to-end"
),
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,9 @@
//! emission over `List<Token>`; see `parse_tables.dag` header.

use v3_compiler::compile_to_dag;
use v3_compiler::dag::{FieldValue, LiteralBits, TypeConnective, ValueBody};
use v3_compiler::dag::{FieldValue, LiteralBits, OperatorKind, TypeConnective, ValueBody};
use v3_compiler::diagnostics::Diagnostic;
use v3_compiler::operators;
use v3_compiler::parse_for_test;
use v3_compiler::parse_tables::soft_keyword_ident_spelling;
use v3_compiler::render_parse_tables_generated_rs;
Expand Down Expand Up @@ -144,6 +145,86 @@ fn binary_op_rows_cover_every_operator_token_the_parser_dispatches_on() {
);
}

#[test]
fn dag_binary_operators_have_token_parse_table_and_operator_mapping() {
let tables_dag = compile_to_dag(PARSE_TABLES_DAG, "src/v3/compiler/parse_tables.dag")
.unwrap_or_else(|e| panic!("parse_tables.dag should compile: {e:?}"));
let tokenize_dag = compile_to_dag(TOKENIZE_DAG, "src/v3/compiler/tokenize.dag")
.unwrap_or_else(|e| panic!("tokenize.dag should compile: {e:?}"));

let token_kind_decl = tokenize_dag
.declaration_by_name("TokenKind")
.expect("TokenKind declaration in tokenize.dag");
let TypeConnective::Disj {
variants: token_variants,
} = &token_kind_decl.connective
else {
panic!("TokenKind should lower to a Disj");
};
let token_variant_names: std::collections::BTreeSet<String> =
token_variants.iter().map(|v| v.label.clone()).collect();

let binary_op_row_type_id = tables_dag
.declaration_by_name("BinaryOpRow")
.expect("BinaryOpRow declaration")
.id;
let mut rows_by_symbol = std::collections::BTreeMap::new();
for decl in tables_dag.declarations() {
if decl.meta_tag != Some(binary_op_row_type_id) {
continue;
}
let name = decl.name.as_deref().unwrap_or("<anonymous>");
let Some(ValueBody::Structural { fields }) = &decl.value_body else {
panic!("`parse_tables.dag::{name}`: BinaryOpRow should carry structural fields");
};
let token_variant = string_field(fields, "token_variant", name);
let operator_symbol = string_field(fields, "operator_symbol", name);
assert!(
rows_by_symbol
.insert(operator_symbol.clone(), token_variant.clone())
.is_none(),
"duplicate BinaryOpRow coverage for operator symbol `{operator_symbol}`"
);
}

for spec in shared_dag_operator_specs(SHARED_SYNTAX_DAG) {
let Some(binop) = spec.binop else {
continue;
};
let expected_token = token_kind_for_shared_dag_operator(&spec.symbol);
assert!(
token_variant_names.contains(expected_token),
"`dag_operators` symbol `{}` expects TokenKind::{expected_token} in tokenize.dag",
spec.symbol
);
let row_token = rows_by_symbol.get(&spec.symbol).unwrap_or_else(|| {
panic!(
"`dag_operators` binary operator `{}` has no BinaryOpRow in parse_tables.dag",
spec.symbol
)
});
assert_eq!(
row_token, expected_token,
"`dag_operators` binary operator `{}` maps to TokenKind::{expected_token}, but \
parse_tables.dag routes TokenKind::{row_token}",
spec.symbol
);
let Some(operator_kind) = operators::from_symbol(&spec.symbol) else {
panic!(
"`dag_operators` binary operator `{}` has no operators.dag::from_symbol mapping",
spec.symbol
);
};
let actual_binop = operator_kind_binop_name(operator_kind);
assert_eq!(
actual_binop, binop,
"`dag_operators` binary operator `{}` records binop `{binop}`, but \
operators.dag maps it to `{actual_binop}`",
spec.symbol
);
}
}

#[test]
fn every_top_level_item_kw_row_token_variant_is_a_token_kind_variant() {
let tables_dag = compile_to_dag(PARSE_TABLES_DAG, "src/v3/compiler/parse_tables.dag")
Expand Down Expand Up @@ -657,3 +738,122 @@ fn primary_atom_rows_cover_exactly_the_tokens_parse_primary_atomic_arm() {
`parse_primary` after the prefix pass"
);
}

struct SharedDagOperatorSpec {
symbol: String,
binop: Option<String>,
}

fn shared_dag_operator_specs(source: &str) -> Vec<SharedDagOperatorSpec> {
extract_balanced_section(source, "data dag_operators", '[', ']')
.split("OperatorSpec")
.skip(1)
.filter_map(|entry| {
let body = entry.split_once('}').map(|(body, _)| body).unwrap_or(entry);
if !body.contains("symbol:") {
return None;
}
let symbol = string_literal_after(body, "symbol:")
.unwrap_or_else(|| panic!("OperatorSpec entry missing string `symbol`: {body}"));
let binop = ident_after(body, "binop:")
.unwrap_or_else(|| panic!("OperatorSpec `{symbol}` missing `binop` field"));
Some(SharedDagOperatorSpec {
symbol,
binop: (binop != "none").then_some(binop),
})
})
.collect()
}

fn token_kind_for_shared_dag_operator(symbol: &str) -> &'static str {
match symbol {
"==" => "EqEq",
"!=" => "NotEq",
"<" => "Lt",
"<=" => "Le",
">" => "Gt",
">=" => "Ge",
"+" => "Plus",
"-" => "Minus",
"*" => "Star",
"/" => "Slash",
"&&" => "AmpAmp",
"||" => "PipePipe",
other => panic!(
"`dag_operators` binary operator `{other}` is not supported by the v3 token/parser/operator chain; \
delete the row until the full chain lands"
),
}
}

fn operator_kind_binop_name(op: OperatorKind) -> &'static str {
match op {
OperatorKind::Arithmetic(arith) => match arith {
v3_compiler::dag::ArithmeticOp::Add => "Add",
v3_compiler::dag::ArithmeticOp::Sub => "Sub",
v3_compiler::dag::ArithmeticOp::Mul => "Mul",
v3_compiler::dag::ArithmeticOp::Div => "Div",
},
OperatorKind::Comparison(comp) => match comp {
v3_compiler::dag::ComparisonOp::Eq => "Eq",
v3_compiler::dag::ComparisonOp::Ne => "Ne",
v3_compiler::dag::ComparisonOp::Lt => "Lt",
v3_compiler::dag::ComparisonOp::Le => "Le",
v3_compiler::dag::ComparisonOp::Gt => "Gt",
v3_compiler::dag::ComparisonOp::Ge => "Ge",
},
OperatorKind::Logical(logical) => match logical {
v3_compiler::dag::LogicalOp::And => "And",
v3_compiler::dag::LogicalOp::Or => "Or",
},
}
}

fn string_field(fields: &[(String, FieldValue)], label: &str, decl_name: &str) -> String {
fields
.iter()
.find_map(|(k, v)| (k == label).then_some(v))
.and_then(|v| match v {
FieldValue::Literal(LiteralBits::String(s)) => Some(s.clone()),
_ => None,
})
.unwrap_or_else(|| panic!("`{decl_name}`: missing string `{label}` field"))
}

fn extract_balanced_section<'a>(source: &'a str, anchor: &str, open: char, close: char) -> &'a str {
let anchor_idx = source
.find(anchor)
.unwrap_or_else(|| panic!("missing `{anchor}` in shared syntax fixture"));
let tail = &source[anchor_idx..];
let open_rel = tail
.find(open)
.unwrap_or_else(|| panic!("missing `{open}` after `{anchor}` in shared syntax fixture"));
let start = anchor_idx + open_rel;
let mut depth = 0usize;
for (offset, ch) in source[start..].char_indices() {
if ch == open {
depth += 1;
} else if ch == close {
depth -= 1;
if depth == 0 {
return &source[start + open.len_utf8()..start + offset];
}
}
}
panic!("unterminated `{anchor}` section");
}

fn string_literal_after(source: &str, label: &str) -> Option<String> {
let tail = source.split_once(label)?.1.trim_start();
let tail = tail.strip_prefix('"')?;
let end = tail.find('"')?;
Some(tail[..end].to_string())
}

fn ident_after(source: &str, label: &str) -> Option<String> {
let tail = source.split_once(label)?.1.trim_start();
let end = tail
.find(|c: char| !(c.is_ascii_alphanumeric() || c == '_'))
.unwrap_or(tail.len());
Some(tail[..end].to_string())
}
Loading