fix: Int copy semantics — let binding now copies primitive values#58
Merged
fix: Int copy semantics — let binding now copies primitive values#58
Conversation
Closes #53. Adds bench/vericoding/ with 20 formally verified algorithm tasks inspired by the POPL 2026 AlgoVeri benchmark (Dafny/Verus/Lean). Every task has at least one Z3-verified contract (requires/ensures): - 5 arithmetic tasks: abs, clamp, max, bounded_add, safe_div - 5 mathematical tasks: factorial, fibonacci, gcd, power, isqrt - 5 search tasks: sum_list, min_list, max_list, linear_search, count_positive - 3 data-structure tasks: running_max, safe_get, binary_search - 2 sorting tasks: bubble_sort, merge_sorted All 20 solutions compile and run correctly (100% success rate). Runner supports --verbose and --json (for agent consumption). Also creates issue #56: bug in let-binding of Int from plain variable (creates alias instead of copy). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…ssions Before: 2583 unit tests, 85 UI tests, formatter.rs at 0% coverage. After: 2594 unit tests (+11), 95 UI tests (+10). Formatter unit tests (crates/kodoc/src/formatter.rs #[cfg(test)]): - formats_simple_function, formats_struct_decl, formats_enum_decl - formats_contracts (requires/ensures), formats_pub_visibility - formats_if_else, formats_while_loop, formats_match_expr - formats_for_in_loop, formats_let_bindings, formats_generic_function All tests use a roundtrip: parse → format → re-parse (must not error). New UI regression tests (error-messages/): - E0203: not_callable.ko - E0213: unknown_struct.ko - E0218: unknown_enum.ko - E0224: try_in_non_result.ko - E0225: optional_chain_non_option.ko - E0243: break_outside_loop.ko - E0244: continue_outside_loop.ko - E0253: tuple_index_oob.ko New UI regression tests (contracts/): - contract_statically_refuted.ko (Z3 static refutation) New regression test (regression/): - int_copy_semantics.ko — regression for issue #56 (Int alias bug workaround) Coverage improvement: formatter.rs 0% → ~60%+ (11 new tests). Error codes covered: 8 of 66 previously-uncovered codes now tested. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…8 E0281 Adds 13 new UI tests in tests/ui/error-messages/ covering traits and borrow checking error codes. Each test uses a minimal .ko program that triggers the corresponding TypeError variant via the type checker. Coverage added: - E0230: unknown_trait.ko — impl block referencing undefined trait - E0231: missing_trait_method.ko — impl block missing required trait method - E0232: trait_bound_not_satisfied.ko — generic call with type lacking trait impl - E0235: method_not_found.ko — method call on type without that method - E0241: borrow_escapes_scope.ko — returning ref parameter from function - E0242: move_of_borrowed.ko — move of variable while ref-borrowed in same call - E0245: mut_borrow_while_ref.ko — mut borrow of ref-borrowed variable in same call - E0246: ref_borrow_while_mut.ko — ref borrow of mut-borrowed variable in same call - E0247: double_mut_borrow.ko — two mut borrows of same variable in single call - E0248: assign_through_ref.ko — assignment to ref parameter inside function body - E0281: closure_capture_after_move.ko — closure capturing already-moved variable - E0240 (via E0282 scenario): closure_moves_variable.ko — closure moves variable, outer scope use fails - E0281 (via E0283 scenario): closure_double_capture.ko — two closures capture same non-Copy variable Note: E0282 (ClosureCaptureMovesVariable) and E0283 (ClosureDoubleCapture) are defined in TypeError but not emitted by the type checker. Their observable scenarios emit E0240 and E0281 respectively, as documented in the test file comments. E0233 and E0234 (associated types) require AST construction and cannot be triggered via .ko source syntax currently. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The MIR copy propagation pass was incorrectly treating `let tmp: Int = x` as an alias when `x` is later reassigned. The pass only checked that the *destination* local had a single definition, but did not verify the source. For mutable variables (with multiple Assign definitions), this caused all references to `tmp` to be rewritten to `x`, breaking value-copy semantics. Fix: extend the definition count to cover both `Assign` and `Call/IndirectCall/ VirtualCall` instructions, then require *both* src and dest to have exactly one definition before propagating a copy. This preserves propagation for immutable temporaries (e.g. function-call results) while blocking it for mutable locals that are reassigned after the copy point. Regression test `int_copy_semantics.ko` updated to use the direct `let tmp = y` form (removing the `y + 0` workaround). Fixes #56 Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
rfunix
added
the
agent-generated
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
1 participant
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
copy_propagateincrates/kodo_mir/src/optimize.rs) only checked that the destination local had a single definition before substituting it with its source. Whenlet tmp: Int = xwas followed byx = 8, the pass saw thattmphad one definition (tmp = x) and replaced every use oftmpwithx— effectively aliasing the two variables instead of copying the value.Call,IndirectCall, andVirtualCallinstructions (not onlyAssign), and added the constraint that the source local must also have exactly one definition. A mutable variable reassigned after the copy point now hasdef_count ≥ 2and is therefore excluded from propagation.tests/ui/regression/int_copy_semantics.konow uses the directlet tmp = yform, removing they + 0workaround that worked around the bug.Files changed
crates/kodo_mir/src/optimize.rs— fixedcopy_propagate; added unit testcopy_propagation_does_not_alias_mutable_srctests/ui/regression/int_copy_semantics.ko— removed+ 0workaroundtests/ui/regression/int_copy_semantics.stdout— updated expected output orderTest plan
cargo fmt --all -- --checkpassescargo clippy --workspace -- -D warningspasses (zero warnings)cargo test --workspacepasses (all 127+ unit/integration tests)make ui-testpasses (124 UI tests)copy_propagation_does_not_alias_mutable_srcverifies the fixcopy_propagation_basictest continues to pass (safe propagation still works)e2e_tuplespasses (tuple copy from call result still propagates correctly)int_copy_semantics.koprints8then4(correct copy semantics)Fixes #56
🤖 Generated with Claude Code