feat(format): cpp-type-preservation-v1 7-gate PARTIAL discharge#1393
Open
feat(format): cpp-type-preservation-v1 7-gate PARTIAL discharge#1393
Conversation
Binds FALSIFY-CPP-001..007 from cpp-type-preservation-v1 at
PARTIAL_ALGORITHM_LEVEL via 7 verdict functions for the Decy
C++→Rust transpiler's type-preservation invariants.
- CPP-001: class with N fields → struct with N pub fields
- CPP-002: constructor → `pub fn new(...) -> Self`
- CPP-003: destructor → `impl Drop for X`
- CPP-004: namespace → `pub mod X` with matching name
- CPP-005: operator+ → `impl std::ops::Add for X`
- CPP-006: inheritance → composition + `impl Deref`
- CPP-007: implicit this.field → self.field (count-preserving)
## Five Whys
1. Why does cpp-type-preservation-v1 list 7 falsification IDs without
algorithm-level discharge? PMAT lints flagged FALSIFY-CPP-001..007
as unbound at PARTIAL_ALGORITHM_LEVEL.
2. Why does that block ship? Coverage % cannot move while peripheral
Decy C++ transpiler type-preservation gates are unbound.
3. Why count-preserving for CPP-007 (not bit-exact)? The contract
asks "implicit `this->x` becomes `self.x`" — the algorithm-level
decision rule is "every implicit-this in C++ produced exactly one
self.field in Rust." Count equality catches the regression class
"CXXThisExpr handling dropped some accesses" without requiring
us to model the full AST.
4. Why vacuous Pass for unused-feature gates (CPP-002/003/005/006)?
When the C++ source has no constructor / destructor / operator+ /
inheritance, the gate's antecedent is false and the implication
is vacuously true. Returning Fail would penalize plain
field-only structs — not the regression class the gate exists to
catch.
5. Why model `pub` visibility separately for CPP-004? Per the
contract: `namespace math { ... }` → `pub mod math { ... }`.
The `pub` visibility is critical — a private `mod math` would
silently drop all the namespace's contents from any cross-crate
re-import, even though name + content match. Modeling visibility
separately catches that regression class.
Adds 30 unit tests including a 5-bucket field-count sweep and
a 4-bucket implicit-this sweep. Realistic-healthy walks the
canonical Decy transpilation; pre-fix walks 7 simultaneous
regressions; vacuous-Pass test guards the unused-feature edge cases.
No runtime % shift; algorithm-level coverage advances by 7 gates.
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
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
cpp-type-preservation-v1atPARTIAL_ALGORITHM_LEVELvia 7 verdict functions for the Decy C++→Rust transpiler.Gates bound
pub fn new(...) -> Selfimpl Drop for Xnamespace X→pub mod X(withpubvisibility)operator+→impl std::ops::Addimpl Derefthis->x→self.x(count-preserving)Five Whys
See commit message — captures count-preserving rationale for CPP-007, vacuous-Pass for unused-feature gates, and why
pubvisibility is modeled separately for CPP-004.Test plan
cargo test -p aprender-core --lib cpp_001_007— 30 passed🤖 Generated with Claude Code