feat(heap-effects): H0 — inert HeapEffectSummary sidecar (extractor facts + Python/Rust solver) - #389
Merged
Merged
Conversation
…is missing Kill-first finding at main a27a827: the only solved summary (MOS / P-037 guarded transfer) cannot prove a call harmless inside a protocol region. Non-disposable methods get no record, borrow_mut collapses into borrow, and the escapes axis has no producer, so a writer and an escaper both solve to transfer=no. Deferring the decision to the core needs a must-understand OwnIR construct (IR3/IR4), i.e. a version bump. Records the missing contract (HeapEffectSummary -> Harmless(callee)) and proposes H0 (inert heap-effect summary domain, facts-only sidecar, no verdict change) and H1 (the wire, pending an owner ruling on OwnIR). No code, fixture, freeze or verdict changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
…acts + Python/Rust solver)
A second summary domain beside MOS, produced and solved end to end and read
by nothing that decides a verdict or a refusal.
- Extractor: `--heap-effects FILE` writes heap-effect SOURCE FACTS to a
separate file after the facts document is final (HeapEffectFacts.cs).
Default-deny IOperation walk: sources, derefs, writes, stores, returns,
calls (callee/dispatch/args), locals, unknown reasons. No solving.
- Core: ownlang/heap_effects.py (reference, `python -m ownlang.heap_effects`)
and own-bridge heap_effects.rs (`own_bridge::dump_heap_effects`): least
fixpoint over the SCC condensation; effects plain < borrow < borrow_mut <
may_escape < unknown, writes {instance,static,indirect} none < may <
unknown, return aliases; Unknown absorbs.
- Parity: tests/fixtures/heap_effects (10 cases, 16 rejection texts),
byte-exact on both engines; 30 pinned kill-fixture summaries.
- Inertness: scripts/heap_effects_gate.py (CI state-protocols job) proves the
facts bytes, exit code and stderr do not move with the flag.
- No OwnIR version, verdict, ProtocolLowering, P-037 or diagnostic change.
The p022 coordinate census is regenerated for the new fixture family.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Что и зачем
Второй summary-домен рядом с MOS: что метод может сделать с памятью, видимой вызывающему. Это параметры, receiver, записи instance/static/indirect и return alias, где Unknown поглощает. Это фундамент для H1 (
Harmless(callee, region-resource)вProtocolLowering). Срез инертный: ни verdict, ни refusal, ни диагностика его не читают.--heap-effects FILEпишет source facts в отдельный файл уже после того, как facts готовы (HeapEffectFacts.cs). Это default-deny IOperation-walk; он ничего не решает.ownlang/heap_effects.py(reference,python -m ownlang.heap_effects) иown-bridge/src/heap_effects.rs(own_bridge::dump_heap_effects). Least fixpoint по SCC-конденсации; эффектыplain < borrow < borrow_mut < may_escape < unknown, записиnone < may < unknown.ProtocolLowering, семантика P-037, T0/perf, существующие диагностики, публичный CLIpython -m ownlang. Единственная правка существующего Rust-кода:dump.rs::emitсталpub(crate).docs/generated/p022-coord-census.md. Census теперь считает и line-слоты новой fixture-семьи.Подробности:
docs/notes/heap-effect-summaries.md. Предыдущий kill-first:docs/notes/protocol-harmless-call-summary-gap.md.Тип изменения
state-protocols)Как проверено
python tests/run_tests.py(rc=0 на чистом дереве)ruff check .иmypycargo fmt --check,cargo clippy --all-targets(новых предупреждений нет),cargo testpython scripts/protocol_gate.py --rust …/own-cli: 0 failures, 19 документов байт-в-байт на обоих CLIpython scripts/heap_effects_gate.py: sidecar сэмплов воспроизводится; 38 прогонов с флагом и без дают идентичные facts-байты, exit code и stderrtests/test_heap_effects_fixtures.py,own-bridge/tests/heap_effects.rs). Дифференциальный фазз на 4000 случайных sidecar'ов (1318 rejection): расхождений 0. Три подсаженных мутанта ловятся и goldens, и фаззом.main(a27a827): экстракторmainпротив этой ветки без флага, 208 C#-входов плюс 4 сканирования директорий × 3 режима флагов. 220/220 совпадают по facts-байтам, exit code и stderr, включая 2 refusal.Связанные issue
Refs P-036 / P-037. Отдельного issue нет.
Чеклист
feat:,fix:,docs:…)🤖 Generated with Claude Code
https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
Generated by Claude Code