Repository navigation
[codex] Add gate 52 structural cost receipt #2578
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
8 commits
Select commit
Hold shift + click to select a range
baf4b2c
Add gate 52 structural cost receipt
briansrls 94b5f5a
Clarify gate 52 fixture cost decomposition
briansrls f4512c0
WIP: R3 gate #52: cross target optimization cost structurally derived
briansrls f430de9
Merge remote-tracking branch 'origin/main' into session/nimble-eagle-79
briansrls f288122
Merge remote-tracking branch 'origin/main' into session/nimble-eagle-79
briansrls ac688d9
WIP: R3 gate #52: cross target optimization cost structurally derived
briansrls 89a936c
Merge origin/main into gate 52 branch
briansrls 58d7dc7
Make gate 52 field lookup lazy
briansrls File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -12,16 +12,21 @@ | |
| //! and assert the claim program lowers to `Behavior::Loop` so the fold is exercised on the compile | ||
| //! path, not only carried as inert text. The first cross-target-optimization claim (#51) is | ||
| //! executable through the symbolic-cost lens: the host test proves a constant arithmetic subtree has | ||
| //! cost `1` before the folded literal target (`3`) is applied. The second claim (#52) keeps the | ||
| //! cost-related `BinaryDimensionReportEquals` shape and stays `NotYetImplemented` until generic | ||
| //! `DimensionReport<C>` evaluation lands. | ||
| //! cost `1` before the folded literal target (`3`) is applied. Gate #52 keeps the cost-related | ||
| //! `BinaryDimensionReportEquals` shape at the generic runner boundary and adds a host-side | ||
| //! executable receipt that composes `Lens<SymbolicCost>` with `LanguageSpec` realization rows. | ||
|
|
||
| use std::sync::OnceLock; | ||
|
|
||
| use v3_compiler::compile_to_dag; | ||
| use v3_compiler::dag::Dag; | ||
| use v3_compiler::dag::{ArithmeticOp, Behavior, OperatorKind, SymbolicCost}; | ||
| use v3_compiler::dag::{ | ||
| sequential, ArithmeticOp, Behavior, ComparisonOp, Dag, DeclarationId, OperatorKind, | ||
| SymbolicCost, TransformTarget, | ||
| }; | ||
| use v3_compiler::emit_rust::emit_rust; | ||
| use v3_compiler::generated_full_bootstrap_dag; | ||
| use v3_compiler::lens_cost_symbolic::{symbolic_cost_of, SymbolicCostLookup}; | ||
| use v3_compiler::realization_cost::{RealizationCostKey, RealizationCostTable}; | ||
| use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner}; | ||
| use v3_compiler::CompileError; | ||
|
|
||
|
|
@@ -30,6 +35,7 @@ use crate::common::run_on_larger_stack; | |
| const FIXTURE_SOURCE: &str = include_str!("../fixtures/r3_free_consequences_second_batch.dag"); | ||
| const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag"; | ||
| const SUITE_NAME: &str = "r3_free_consequences_second_batch_suite"; | ||
| const GATE_52_PROGRAM_FILE: &str = "r3_free_consequences_gate52_cost_structurally_derived.v3"; | ||
| /// Byte-sync authority for gate #48 `TestClaim.source` (`include_str` ↔ embedded `.dag` string). | ||
| const GATE_48_PROGRAM_AUTHORITY: &str = | ||
| include_str!("../fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3"); | ||
|
|
@@ -118,13 +124,261 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() { | |
| } else { | ||
| assert!( | ||
| matches!(&result.result, ClaimResult::NotYetImplemented(_)), | ||
| "expected {expected_name} to stay author-now/fire-later on BinaryDimensionReportEquals, got {:?}", | ||
| "expected {expected_name} `.dag` predicate to stay at the generic BinaryDimensionReportEquals boundary; \ | ||
| gate #52's executable receipt lives in `cross_target_optimization_cost_structurally_derived_receipt`, got {:?}", | ||
| result.result | ||
| ); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| #[test] | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. BLOCKING: Adding a new host-side Rust receipt under src/v3/compiler/tests expands hand-written Rust, so INVARIANTS.md P5 requires exactly one PR-body or planning-artifact receipt before this lands. |
||
| fn cross_target_optimization_cost_structurally_derived_receipt() { | ||
| run_on_larger_stack(|| { | ||
| let boot = generated_full_bootstrap_dag(); | ||
| let rust_language = named_id(&boot, "rust_language"); | ||
| let int_decl = named_id(&boot, "Int"); | ||
| let table = RealizationCostTable::for_language(&boot, rust_language) | ||
| .expect("Rust LanguageSpec realization-cost table should build"); | ||
|
|
||
| let user = compile_to_dag( | ||
| "\ | ||
| fn countdown(n: Int) -> Int = | ||
| if n == 0 then 0 else countdown(n - 1) + 1 | ||
|
|
||
| let demo: Int = countdown(3) + 1 | ||
| ", | ||
| GATE_52_PROGRAM_FILE, | ||
| ) | ||
| .expect("gate #52 representative program compiles"); | ||
| let emitted = emit_rust(&user).expect("gate #52 representative program emits to Rust"); | ||
| assert!( | ||
| emitted.contains("fn countdown") | ||
| && emitted.contains("(countdown(&(((*(p0)) - 1))) + 1)") | ||
| && emitted.contains("let demo: i64 = (countdown(&(3)) + 1);"), | ||
| "gate #52 must exercise the emitted target program, got:\n{emitted}" | ||
| ); | ||
|
|
||
| let countdown = find_bind_value(&user, "countdown"); | ||
| let algebra_cost = match symbolic_cost_of(&user, &countdown) { | ||
| SymbolicCostLookup::Hit(cost) => cost, | ||
| SymbolicCostLookup::Miss => panic!("symbolic_cost_of Miss for `countdown`"), | ||
| }; | ||
|
|
||
| let realized_rows = realized_primitive_rows_from_program(&boot, &user, int_decl); | ||
| assert_eq!( | ||
| realized_rows | ||
| .iter() | ||
| .map(|row| (row.name, row.op)) | ||
| .collect::<Vec<_>>(), | ||
| expected_gate_52_realization_rows(&boot, int_decl) | ||
| .iter() | ||
| .map(|row| (row.name, row.op)) | ||
| .collect::<Vec<_>>(), | ||
| "gate #52 fixture should derive Add/Add/Eq/Eq/Sub primitive row identities from the program DAG" | ||
| ); | ||
| let realized_costs = realized_rows | ||
| .iter() | ||
| .map(|row| realization_cost(&table, int_decl, row.op)) | ||
| .collect::<Vec<_>>(); | ||
| assert_eq!( | ||
| realized_costs, | ||
| vec![1, 1, 1, 1, 1], | ||
| "gate #52 fixture should derive Add/Add/Eq/Eq/Sub primitive costs from Rust LanguageSpec rows" | ||
| ); | ||
|
|
||
| let observed_target_cost = compose_observed_structural_cost( | ||
| algebra_cost.clone(), | ||
| &table, | ||
| int_decl, | ||
| &realized_rows, | ||
| ); | ||
| let expected_structural_cost = compose_expected_structural_cost( | ||
| algebra_cost, | ||
| &table, | ||
| int_decl, | ||
| expected_gate_52_realization_rows(&boot, int_decl), | ||
| ); | ||
|
|
||
| assert_eq!( | ||
| observed_target_cost, expected_structural_cost, | ||
| "gate #52 target-cost reading must equal Lens<SymbolicCost> composed with LanguageSpec realization costs" | ||
| ); | ||
| assert!( | ||
| mentions_linear(&observed_target_cost), | ||
| "gate #52 receipt should preserve the recursive program's structural linear bound, got {observed_target_cost:?}" | ||
| ); | ||
| }); | ||
| } | ||
|
|
||
| #[derive(Debug, Clone, Copy, PartialEq, Eq)] | ||
| struct RealizedPrimitiveRow { | ||
| name: &'static str, | ||
| op: DeclarationId, | ||
| } | ||
|
|
||
| fn realized_primitive_rows_from_program( | ||
| boot: &Dag, | ||
| program: &Dag, | ||
| int_decl: DeclarationId, | ||
| ) -> Vec<RealizedPrimitiveRow> { | ||
| let mut rows = Vec::new(); | ||
| for transform in program | ||
| .nodes() | ||
| .iter() | ||
| .filter_map(Behavior::as_transform) | ||
| .filter(|transform| transform.span.file == GATE_52_PROGRAM_FILE) | ||
| { | ||
| let Some(row) = operator_row_for_transform(boot, &transform.target, int_decl) else { | ||
| continue; | ||
| }; | ||
| rows.push(row); | ||
| } | ||
| rows.sort_by_key(|row| row.name); | ||
| rows | ||
| } | ||
|
|
||
| fn compose_expected_structural_cost( | ||
| algebra_cost: SymbolicCost, | ||
| table: &RealizationCostTable, | ||
| int_decl: DeclarationId, | ||
| rows: Vec<RealizedPrimitiveRow>, | ||
| ) -> SymbolicCost { | ||
| // Mirrors the gate #52 fixture's lowered program DAG exactly: one recursive decrement | ||
| // (`n - 1`), two equality transforms for the conditional path, and two additions | ||
| // (recursive body plus `demo + 1`). | ||
| rows.into_iter() | ||
| .map(|row| realization_cost(table, int_decl, row.op)) | ||
| .fold(algebra_cost, |acc, primitive_cost| { | ||
| sequential(acc, SymbolicCost::ConstantCost { _0: primitive_cost }) | ||
| }) | ||
| } | ||
|
|
||
| fn expected_gate_52_realization_rows( | ||
| boot: &Dag, | ||
| int_decl: DeclarationId, | ||
| ) -> Vec<RealizedPrimitiveRow> { | ||
| [ | ||
| operator_realization_row(boot, "rust_int_add", int_decl), | ||
| operator_realization_row(boot, "rust_int_add", int_decl), | ||
| operator_realization_row(boot, "rust_int_eq", int_decl), | ||
| operator_realization_row(boot, "rust_int_eq", int_decl), | ||
| operator_realization_row(boot, "rust_int_sub", int_decl), | ||
| ] | ||
| .into() | ||
| } | ||
|
|
||
| fn realization_cost( | ||
| table: &RealizationCostTable, | ||
| int_decl: DeclarationId, | ||
| op: DeclarationId, | ||
| ) -> i64 { | ||
| table | ||
| .cost(&RealizationCostKey::Operator { | ||
| target: int_decl, | ||
| op, | ||
| }) | ||
| .unwrap_or_else(|| { | ||
| panic!("missing Rust LanguageSpec realization cost for operator row {op:?}") | ||
| }) | ||
| .value() | ||
| } | ||
|
|
||
| fn compose_observed_structural_cost( | ||
| algebra_cost: SymbolicCost, | ||
| table: &RealizationCostTable, | ||
| int_decl: DeclarationId, | ||
| rows: &[RealizedPrimitiveRow], | ||
| ) -> SymbolicCost { | ||
| rows.iter() | ||
| .map(|row| realization_cost(table, int_decl, row.op)) | ||
| .fold(algebra_cost, |acc, primitive_cost| { | ||
| sequential(acc, SymbolicCost::ConstantCost { _0: primitive_cost }) | ||
| }) | ||
| } | ||
|
|
||
| fn operator_row_for_transform( | ||
| boot: &Dag, | ||
| target: &TransformTarget, | ||
| int_decl: DeclarationId, | ||
| ) -> Option<RealizedPrimitiveRow> { | ||
| let row = match target { | ||
| TransformTarget::Operator(OperatorKind::Arithmetic(ArithmeticOp::Add)) => "rust_int_add", | ||
| TransformTarget::Operator(OperatorKind::Arithmetic(ArithmeticOp::Sub)) => "rust_int_sub", | ||
| TransformTarget::Operator(OperatorKind::Comparison(ComparisonOp::Eq)) => "rust_int_eq", | ||
| _ => return None, | ||
| }; | ||
| Some(operator_realization_row(boot, row, int_decl)) | ||
| } | ||
|
|
||
| fn operator_realization_row( | ||
| boot: &Dag, | ||
| row: &'static str, | ||
| int_decl: DeclarationId, | ||
| ) -> RealizedPrimitiveRow { | ||
| let row_decl = boot | ||
| .declaration_by_name(row) | ||
| .unwrap_or_else(|| panic!("missing `{row}` OperatorRealization row")); | ||
| assert_eq!( | ||
| field_ref(boot, row, "target"), | ||
| int_decl, | ||
| "`{row}` should realize the bootstrap Int target" | ||
| ); | ||
| assert!( | ||
| row_decl.value_body.is_some(), | ||
| "OperatorRealization row should have a structural body" | ||
| ); | ||
| RealizedPrimitiveRow { | ||
| name: row, | ||
| op: field_ref(boot, row, "op"), | ||
| } | ||
| } | ||
|
|
||
| fn find_bind_value(dag: &Dag, name: &str) -> v3_compiler::dag::PortId { | ||
| dag.nodes() | ||
| .iter() | ||
| .filter_map(Behavior::as_bind) | ||
| .find(|bind| bind.name == name) | ||
| .unwrap_or_else(|| panic!("bind `{name}` not found")) | ||
| .value | ||
| } | ||
|
|
||
| fn named_id(dag: &Dag, name: &str) -> DeclarationId { | ||
| dag.declaration_by_name(name) | ||
| .unwrap_or_else(|| panic!("missing declaration `{name}`")) | ||
| .id | ||
| } | ||
|
|
||
| fn field_ref(dag: &Dag, decl_name: &str, field_name: &str) -> DeclarationId { | ||
| let decl = dag | ||
| .declaration_by_name(decl_name) | ||
| .unwrap_or_else(|| panic!("missing declaration `{decl_name}`")); | ||
| let Some(v3_compiler::dag::ValueBody::Structural { fields }) = decl.value_body.as_ref() else { | ||
| panic!("`{decl_name}` should have a structural body"); | ||
| }; | ||
| fields | ||
| .iter() | ||
| .find_map(|(key, value)| { | ||
| (key == field_name).then(|| match value { | ||
| v3_compiler::dag::FieldValue::Reference(id) => *id, | ||
| other => { | ||
| panic!("`{decl_name}.{field_name}` should be DeclarationRef, got {other:?}") | ||
| } | ||
| }) | ||
| }) | ||
| .unwrap_or_else(|| panic!("`{decl_name}` missing field `{field_name}`")) | ||
| } | ||
|
|
||
| fn mentions_linear(cost: &SymbolicCost) -> bool { | ||
| match cost { | ||
| SymbolicCost::LinearCost { .. } => true, | ||
| SymbolicCost::SumCost { _0: terms } | SymbolicCost::ProductCost { _0: terms } => { | ||
| terms.iter().any(|term| mentions_linear(term.as_ref())) | ||
| } | ||
| _ => false, | ||
| } | ||
| } | ||
|
|
||
| #[test] | ||
| fn cross_target_optimization_constant_fold_consistent_has_symbolic_cost_witness() { | ||
| run_on_larger_stack(|| { | ||
|
|
||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BLOCKING: This imports v3_compiler::realization_cost, but the supplied diff adds no such module and git ls-tree origin/main -- src/v3/compiler/src/realization_cost.rs returned no blob, so the crate will not compile.