core: close Program proof and allocation boundaries - #463
Conversation
…ells `AdmittedFiniteJointOrderV1` stored one flat tuple slice, so an empty admitted order was representable and the evaluation path carried a runtime `state_count == 0 -> InternalInvariant` guard to reject it. The guard proved nothing about the type; it only re-checked a property the constructor already enforced. Split the order into `first + rest`. Non-emptiness becomes structural, `state_count()` is total, and the `InternalInvariant` branch in `prepare_program_evaluation_buffers` is deleted rather than left dead. The `joint_state_count: Option<usize>` parameter disappears with it: cell counts are now derived from the epoch itself. The same pass stops reserving an exhaustive-conflict buffer that no constraint can ever fill. `can_conflict` is false when every compiled constraint is report-only, so a report-only program no longer reserves `cases x constraints x states` cells and no longer reports `ResourceExhausted` for a conflict it cannot produce. `OwnerV1::evidence_cell_bounds` exposes the same arithmetic as a pure preflight, with `EvidenceBoundsErrorV1::CardinalityOverflow` as the only closed failure. It creates no Session and mutates no state. Verified locally on the CI-pinned toolchain: full workspace tests green, `cargo fmt --all --check` and `cargo clippy --workspace --all-targets -- -D warnings` clean. Co-Authored-By: Claude <noreply@anthropic.com>
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
WalkthroughPR добавляет публичное preflight-вычисление границ evidence, меняет хранение состояний joint-порядка, обновляет расчёт буферов оценивания и усиливает проверку compile-fail документации тестами. ChangesПланирование границ evidence
Проверка compile-fail fences
Estimated code review effort: 3 (Moderate) | ~20 minutes Sequence Diagram(s)sequenceDiagram
participant OwnerV1
participant CompiledProgram
participant EvaluationCounts
OwnerV1->>CompiledProgram: evidence_cell_bounds(scenario_count)
CompiledProgram->>EvaluationCounts: checked_program_epoch_evaluation_cell_counts
EvaluationCounts-->>CompiledProgram: selected и exhaustive_conflict counts
CompiledProgram-->>OwnerV1: EvidenceCellBoundsV1 или CardinalityOverflow
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
|
@coderabbitai review |
✅ Action performedReview finished.
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
crates/labcolors-core/src/program_session.rs (1)
1626-1659: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winДобавить комментарий к условию резервирования
conflict_cells.Логика верна:
conflict_cellsреально используется только в веткеevaluate_program_sessionсjoint_selection(без него код всегда берёт толькоbuffers.take_selected()), поэтому дополнительная проверкаepoch.joint_selection.is_some()наряду сcounts.exhaustive_conflict != 0оправдана и предотвращает лишнюю аллокацию. Но само по себе сочетание двух условий неочевидно без пояснения — читатель может решить, что проверкаjoint_selection.is_some()избыточна, разexhaustive_conflictи так равен 0 приcan_conflict == false.As per coding guidelines, "Комментарии в коде должны объяснять почему и инвариант, а не пересказывать оператор."
✏️ Предлагаемый комментарий
let mut conflict_cells = Vec::new(); + // `conflict_cells` is only ever populated by the joint-selection branch + // of `evaluate_program_session`; skip reserving it otherwise, even when + // `exhaustive_conflict` is nonzero for a non-joint hard constraint. if epoch.joint_selection.is_some() && counts.exhaustive_conflict != 0 {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@crates/labcolors-core/src/program_session.rs` around lines 1626 - 1659, Добавьте поясняющий комментарий непосредственно перед условием резервирования в prepare_program_evaluation_buffers: conflict_cells используется только при evaluate_program_session с включённым epoch.joint_selection, поэтому проверка joint_selection.is_some() сохраняется для предотвращения ненужной аллокации даже при ненулевом counts.exhaustive_conflict.Source: Coding guidelines
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@crates/labcolors-core/src/joint.rs`:
- Around line 130-133: Добавьте комментарий перед веткой
`first_tuple.ok_or(FiniteJointOrderErrorV1::EmptyOrder)?`, объясняющий, что
проверка `authored.len() >= 1` перед циклом гарантирует установку `first_tuple`,
поэтому ошибка `EmptyOrder` недостижима при текущем инварианте; сохраните
типизированную проверку вместо паники.
In `@crates/labcolors-core/src/program_session.rs`:
- Around line 1494-1517: Добавьте рядом с вычислением state_count комментарий,
объясняющий инвариант: отсутствие joint_selection означает единственную
фиксированную конфигурацию, поэтому число состояний равно 1. Не изменяйте
поведение unwrap_or(1) и остальную логику подсчёта.
---
Outside diff comments:
In `@crates/labcolors-core/src/program_session.rs`:
- Around line 1626-1659: Добавьте поясняющий комментарий непосредственно перед
условием резервирования в prepare_program_evaluation_buffers: conflict_cells
используется только при evaluate_program_session с включённым
epoch.joint_selection, поэтому проверка joint_selection.is_some() сохраняется
для предотвращения ненужной аллокации даже при ненулевом
counts.exhaustive_conflict.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 2b5f5ffc-7936-49ab-a9d6-dbe93612b7ea
📒 Files selected for processing (5)
crates/labcolors-core/src/generic_boundary_tests.rscrates/labcolors-core/src/joint.rscrates/labcolors-core/src/program.rscrates/labcolors-core/src/program_session.rscrates/labcolors-core/tests/program_boundary.rs
|
@coderabbitai review |
✅ Action performedReview finished.
|
|
Superseded by the reviewed cumulative squash merge #465 ( |
1 participant
DAG
Draft stacked PR. Base:
agent/public-program-api/ #461 at92f8376. Do not merge before #461.Что изменено
Зачем
Предыдущая граница оставляла два proof-вакуума: отрицательный compile-fail sentinel мог пережить вставку live-кода, а максимальный размер evidence allocation не был доступен и доказан через единую Program-формулу. Этот slice закрывает оба без transport/client semantics и без расширения recipe-архитектуры.
Проверки
cargo +1.96.0 fmt --all --checkcargo +1.96.0 clippy --workspace --all-targets --locked -- -D warningscargo +1.96.0 test --workspace --locked— Core 764 passed / 6 ignored; все workspace suites и doctests greengit diff --checkSummary by CodeRabbit
evidence_cell_bounds(scenario_count)(verified/conflict) без создания и изменения сессии.EvidenceCellBoundsV1иEvidenceBoundsErrorV1с диагностикойCardinalityOverflow.