Result: done
Files: crates/nikaia/src/contracts/keeps.rs crates/nikaia/src/contracts/mod.rs crates/nikaia/src/contracts/sync.rs crates/nikaia/src/modules.rs crates/nikaia/src/project.rs crates/nikaia/src/prove.rs crates/nikaia/src/check/mod.rs crates/nikaia/src/check/core.rs crates/nikaia-std/src/tools/lends.nika crates/nikaia-std/src/tools/contract_changes.nika crates/nikaia-std/src/tools/check_state.nika crates/nikaia-std/src/tools/check_core_call_on.nika crates/nikaia-std/src/tools/check_core_args.nika crates/nikaia-std/src/tools/check_core_leaves.nika crates/nikaia-std/src/tools/check_lambdas.nika crates/nikaia-std/src/tools/lowered.rs crates/nikaia-std/src/tools/lowered/lends.rs crates/nikaia-std/src/tools/lowered/contract_changes.rs crates/nikaia-std/src/tools/lowered/check_state.rs crates/nikaia-std/src/tools/lowered/check_core_call_on.rs crates/nikaia-std/src/tools/lowered/check_core_args.rs crates/nikaia-std/src/tools/lowered/check_core_leaves.rs crates/nikaia-std/src/tools/lowered/check_lambdas.rs tests/compiler/tests/a_foreign_impl_keeping_beyond_the_column_is_refused.nika tests/compiler/tests/a_foreign_impl_keeping_beyond_the_column_is_refused.stdout tests/compiler/tests/a_trait_column_change_warns.nika tests/compiler/tests/a_trait_column_change_warns.stdout tests/compiler/tests/a_lent_parameter_kept_by_a_trait_method_is_taken.stderr assets/badges/self-hosted.svg
Commit: contracts: NK1264 refuses a foreign keeper, NK1265 warns on a trait column change (#1012)
Body: keeps::infer returns the column’s keepers, found on the impls’ own evidence (graph without the edges into their trait methods), into Noted and Program, with no new ledger field. A foreign trait’s impl that keeps beyond the library column is NK1264, which names the keeping statement. changed_contracts warns NK1265 in both directions and names the impls. A lending caller’s NK2101 names the impl through CheckWorld.keepers.
Part: #1012
Pushed: a39c219f (pushed by drive.nika)
Tests: (g) a_foreign_impl_keeping_beyond_the_column_is_refused and (h) a_trait_column_change_warns pass. tests/compiler –both-settings: 405 passed, including a_trait_method_callback_is_handed_on and the step-1 tests. it: contracts plus the guard set, 84 passed (sequences green). –lib contracts:: modules:: project:: check::, 46 passed. Clippy clean. Neither new test was run against the unfixed compiler: no older binary was on disk, and NK1264/NK1265 did not exist before.
Gate: green
Deviation: the step-1 a_lent_parameter_kept_by_a_trait_method_is_taken.stderr is updated, since its NK2101 now names Keep::take. NK2101 names the impl inside its message (after Keep::ask (path:line: stmt), which keeps known ..., took it), not in a separate note.
Found: nikaia fmt FILE run from the repository root rewrote tools files with tabs and rewrapped them; I restored them by hand. The fmt guard checks only idempotence.
Needs: supervisor rebase and push of a39c219f
Changelog: NK1264 refuses an impl of another package’s trait that keeps a parameter the trait method’s keeps column runs; NK1265 warns when a pub trait method’s column changes, naming the impl (ADR-277 D17, #1012).
Owner: none
Disk freed: none (cache 1.8G, / 4.7G free, no new entry over 100 MB)
Rs2nika: none
