Add property-based tests for Weave rebase and attribute-scope invariants

[coderabbitai]

Summary

Add substantive property-based tests or a bounded state model for the stateful behaviour documented by the weave-git-merge skill.

The current tests validate fixed documentation strings and one global rebase flow. They do not validate the ordering invariants for multi-commit rebases or the fallback behaviour across Git attribute scopes.

Rationale

A silently invalid resolution in an early rebase commit can become the ours stage for later commits. Attribute-scope fallbacks also depend on the operation type and the active Git attribute source. Static documentation checks cannot establish these invariants.

Affected areas

• tests/test_weave_git_merge_skill.py
• skills/weave-git-merge/SKILL.md
• skills/weave-git-merge/references/behaviour.md
• Any test fixtures or helper modules needed to model rebase replay and attribute scopes

Required changes

Add either Hypothesis tests or a bounded state model. Cover these dimensions:

• Operation types: rebase and merge.
• Attribute scopes: repository-tracked .gitattributes, local .git/info/attributes, and the global core.attributesFile.
• Stage validity: base (:1:), ours (:2:), theirs (:3:), and the resolved working file.
• Multi-commit replay transitions, including propagation when an early replay result is structurally invalid.
• Fallback behaviour that disables only the intended attribute source and verifies the effective merge attribute.

Use generated or enumerated sequences to assert the documented safety properties. Do not rely only on fixed prose assertions.

Acceptance criteria

• Tests cover every operation type and attribute scope listed above.
• Tests cover valid and invalid index-stage combinations.
• Tests model at least two replay transitions and verify that invalid early output cannot be accepted as a safe later ours stage.
• Tests verify the expected fallback result for each supported attribute scope.
• The tests fail when transition order, stage validity, or fallback scope handling is changed incorrectly.
• Existing documentation tests remain intact.

Backlinks

• Pull request: Detect and recover from silent Weave rebase corruption (#81) #92
• Request comment: Detect and recover from silent Weave rebase corruption (#81) #92 (comment)

Requested by: @leynos

[coderabbitai]

🔗 Related PRs

leynos/df12-documentation-skills#4 - Roadmap and Verification Refinements [closed]
#25 - Add TypeScript verification skills [open]
#80 - Add practical Weave Git merge skill [open]
#92 - Detect and recover from silent Weave rebase corruption (#81) [open]
leynos/comenq-coderabbit#2 - Require tagging, per-thread replies, and pre-merge reconciliation (#1) [open]

---

📝 Issue Planner

_{Check the box below or use the @coderabbitai plan command to generate an implementation plan and prompts that you can use with your favorite coding assistant.}

---

🧪 Issue enrichment is currently in open beta.

You can configure auto-planning by selecting labels in the issue_enrichment configuration.

To disable automatic issue enrichment, add the following to your .coderabbit.yaml:

issue_enrichment:
  auto_enrich:
    enabled: false

💬 Have feedback or questions? Drop into our discord!

[leynos]

@CodeRabbit plan

[coderabbitai]

Coding Plan

Summary

• Encode the documented rules as a deterministic pure-Python model in a new tests/weave_git_merge_model.py support module.
• Drive the model with plain @given property tests in a new tests/test_weave_git_merge_properties.py, covering operations, scopes, stage validity, and multi-commit replay.
• Ground the model with one real-Git two-commit chained-replay test in tests/test_weave_git_merge_procedures.py.
• Reconcile the skill documentation and add anchoring contract assertions, keeping every existing documentation test intact.

Follow-up agent prompt

Implement the plan for property-based Weave rebase and attribute-scope tests.

1. Create tests/weave_git_merge_model.py. Model three concerns as separate pure-Python functions: attribute-scope fallback (effective merge attribute per scope and bypass), stage validity (which of :1:/:2:/:3: exist and are trusted), and multi-commit replay transitions (commit N ours derives from commit N-1 result; a clean-exit corrupt early result must be flagged unsafe and never accepted as a safe later ours). No Git calls.

2. Create tests/test_weave_git_merge_properties.py. Use `from hypothesis import given, settings` and `from hypothesis import strategies as st`. Define SCREAMING_SNAKE_CASE module-level strategies. Add properties for: fallback per scope (correct bypass yields unspecified, wrong bypass does not), the core.attributesFile absent-versus-unset pitfall, stage validity (only existing stages parse; parsing :3: never rescues non-parsing :2: in a multi-commit rebase), and replay safety over sequences of length two or more (invalid early output never accepted as safe later ours; reordering changes the accepted outcome).

3. Extend tests/test_weave_git_merge_procedures.py with a real-Git two-commit chained-replay test. Build a two-commit topic branch that touches the conflicting file twice, reuse one cmd_mox spy across both invocations with a closure counter (corrupt then valid), assert spy.call_count == 2, and confirm the corrupt first replay propagates into the second replay's ours stage.

4. Reconcile skills/weave-git-merge/SKILL.md and references/behaviour.md so each modelled invariant is stated explicitly. Add matching contract assertions to tests/test_weave_git_merge_skill.py. Do not change existing contract assertions.

Follow en-GB-oxendict (-ize/-yse/-our) spelling. Run the full test suite and confirm existing documentation tests still pass.

Design Choices

Design Choice 1: Choose the modelling technique for the stateful invariants

Options Considered:

1. Pure-Python bounded behavioural model as the system under test, exercised by plain @given property tests over generated sequences.
2. Hypothesis RuleBasedStateMachine that drives real Git repositories and the cmd_mox driver double per generated step.
3. Plain @given tests that shell out to real Git for every generated example.

Chosen Option: 1

Rationale: A pure-Python model runs fast, stays deterministic, and encodes the documented rules directly, so an incorrect change fails the invariants. It matches the existing plain @given convention. Ground it with one real-Git behavioural test so the model tracks actual Git behaviour.

💡 User Tips

Regenerate the plan with different choices with @coderabbitai <feedback>.

Implementation Steps

Phase 1: Build the bounded behavioural model

Encode the documented rules as a small, deterministic Python model. Treat the model as the system under test. Keep the three concerns — attribute-scope fallback, stage validity, and multi-commit replay — as separate, composable functions. Each function must mirror one documented rule set, so an incorrect change to a rule breaks a property in Phase 2.

Task 1: Create the model support module

Add a new test-support module that holds the model. Follow the tests/typos_rollout_test_support.py support-module convention.

• Create tests/weave_git_merge_model.py.
• Define enumerations for operation type (rebase, merge) and attribute scope (tracked, clone-local, global).
• Define a lightweight replay-state type that records, per replayed commit, the base/ours/theirs inputs, the driver exit code, and whether the produced output is structurally valid.
• Keep the module free of Git calls; it models documented behaviour only.

Task 2: Model attribute-scope resolution and fallback

Encode the documented bypass matrix and the effective merge attribute per scope.

• Add a function that returns the effective merge attribute (weave or unspecified) for a given scope and applied bypass.
• Encode that the global scope becomes unspecified only under the core.attributesFile=/dev/null override.
• Encode that the tracked and clone-local scopes become unspecified only under a later path-specific !merge rule, and remain weave under the /dev/null override.
• Encode the core.attributesFile pitfall: an absent setting means the default global path applies, not the absence of a global rule.

Task 3: Model stage validity

Encode which index stages exist and which are trusted.

• Add a function that reports the valid stage set (:1:, :2:, :3:) for a given operation and case, including cases that lack a base.
• Encode that only existing stages may be parsed.
• Encode that during a multi-commit rebase, stage :2: is not a trusted baseline, because it can hold an earlier corrupt replay.

Task 4: Model multi-commit replay transitions

Encode the sequential replay transition function with propagation.

• Add a function that folds a sequence of replay outcomes into per-commit states, where commit N's ours input derives from commit N-1's produced result.
• Encode that a clean-exit but structurally invalid early result propagates into the later ours stage.
• Encode the andon rule: a structurally invalid replay must be flagged unsafe and must never be accepted as a safe later ours stage.

🤖 Prompt for AI agents

Build the pure-Python behavioural model that encodes the documented
`weave-git-merge` invariants. This model is the system under test for the
property tests in Phase 2, so match each documented rule precisely.

- Create `tests/weave_git_merge_model.py`, following the
`tests/typos_rollout_test_support.py` support-module convention. Do not call Git
from this module; model documented behaviour only.
- Define enumerations for operation type (`rebase`, `merge`) and attribute scope
(`tracked`, `clone-local`, `global`).
- Define a lightweight replay-state type that records, per replayed commit: the
base/ours/theirs inputs, the driver exit code, and whether the produced output
is structurally valid.
- Add a function for attribute-scope fallback that returns the effective `merge`
attribute (`weave` or `unspecified`) for a given scope and applied bypass. The
global scope becomes `unspecified` only under the
`core.attributesFile=/dev/null` override. The tracked and clone-local scopes
become `unspecified` only under a later path-specific `!merge` rule, and stay
`weave` under the `/dev/null` override. Encode the `core.attributesFile`
pitfall: an absent setting means the default global path applies, not the
absence of a global rule.
- Add a function for stage validity that reports the valid stage set (`:1:`,
`:2:`, `:3:`) for a given operation and case, including cases without a base.
Only existing stages may be parsed. During a multi-commit rebase, stage `:2:` is
not a trusted baseline, because it can hold an earlier corrupt replay.
- Add a function for multi-commit replay transitions that folds a sequence of
replay outcomes into per-commit states, where commit N's `ours` input derives
from commit N-1's produced result. A clean-exit but structurally invalid early
result must propagate into the later `ours` stage. Apply the andon rule: flag a
structurally invalid replay as unsafe, and never accept it as a safe later
`ours` stage.

Phase 2: Add property-based tests over the model

Add a dedicated property-test module that generates enumerated sequences and asserts the documented safety properties against the model. Cover every operation type, every scope, valid and invalid stage combinations, and at least two replay transitions.

Task 1: Create the property-test module and strategies

Add the property tests alongside the model. Follow the _properties.py naming and strategy conventions.

• Create tests/test_weave_git_merge_properties.py.
• Import Hypothesis as from hypothesis import given, settings and from hypothesis import strategies as st.
• Define module-level, SCREAMING_SNAKE_CASE strategies for operation types, scopes, replay-outcome sequences, and stage-combination cases.
• Apply @settings per test only where needed; the model is pure Python, so a deadline override is not required.

Task 2: Assert attribute-scope fallback properties

Verify the fallback result for each supported scope.

• Assert that, for every scope, the documented bypass yields unspecified.
• Assert that the wrong bypass for a scope does not yield unspecified (for example, /dev/null against a tracked or clone-local rule).
• Assert the core.attributesFile absent-versus-unset property holds for the global scope.

Task 3: Assert stage-validity properties

Verify valid and invalid index-stage combinations.

• Assert that generated cases only ever parse stages that exist.
• Assert that a parsing stage :3: never marks a non-parsing stage :2: as safe during a multi-commit rebase.
• Assert that base-absent cases never expose a :1: stage.

Task 4: Assert multi-commit replay safety properties

Verify replay ordering and propagation over at least two transitions.

• Generate replay-outcome sequences of length two or more.
• Assert that a structurally invalid early result is never accepted as a safe later ours stage.
• Assert that a corrupt early replay marks the sequence unsafe even when later replays parse cleanly.
• Assert that reordering the transition sequence changes the accepted outcome, so incorrect ordering fails the property.

🤖 Prompt for AI agents

Add a property-test module that exercises the Phase 1 model with generated
sequences, covering every operation type, every scope, valid and invalid stage
combinations, and at least two replay transitions.

- Create `tests/test_weave_git_merge_properties.py`, following the
`_properties.py` naming and strategy conventions.
- Import Hypothesis as `from hypothesis import given, settings` and `from
hypothesis import strategies as st`.
- Define module-level, `SCREAMING_SNAKE_CASE` strategies for operation types,
scopes, replay-outcome sequences, and stage-combination cases. Apply `@settings`
per test only where needed; the model is pure Python, so a `deadline` override
is not required.
- Add attribute-scope fallback properties: for every scope, the documented
bypass yields `unspecified`; the wrong bypass for a scope does not yield
`unspecified` (for example, `/dev/null` against a tracked or clone-local rule);
the `core.attributesFile` absent-versus-unset property holds for the global
scope.
- Add stage-validity properties: generated cases only ever parse stages that
exist; a parsing stage `:3:` never marks a non-parsing stage `:2:` as safe
during a multi-commit rebase; base-absent cases never expose a `:1:` stage.
- Add multi-commit replay safety properties over generated sequences of length
two or more: a structurally invalid early result is never accepted as a safe
later `ours` stage; a corrupt early replay marks the sequence unsafe even when
later replays parse cleanly; reordering the transition sequence changes the
accepted outcome, so incorrect ordering fails the property.

Phase 3: Ground the model in real Git and preserve documentation tests

Add one real-Git behavioural test that grounds the model's replay assumptions. Reconcile the documentation so the invariants are stated explicitly. Keep every existing documentation test intact.

Task 1: Add a real-Git two-commit chained-replay test

Extend the behavioural suite with a genuine multi-commit rebase where the driver is invoked once per replayed commit.

• Update tests/test_weave_git_merge_procedures.py.
• Extend the _diverge helper path to build a two-commit topic branch where both commits touch the conflicting file.
• Reuse a single cmd_mox spy across both invocations with a closure-held counter, returning corrupt content on the first replay and valid content on the second.
• Assert spy.call_count == 2, inspect spy.invocations[0] and spy.invocations[1], and confirm the corrupt early result propagates into the second replay's ours stage.

Task 2: Reconcile documented invariants and anchor contract assertions

Ensure the documentation states the modelled invariants explicitly, then anchor them with contract assertions.

• Review skills/weave-git-merge/SKILL.md and skills/weave-git-merge/references/behaviour.md.
• If a modelled invariant is implicit, add concise wording that states it plainly; do not restructure the documents.
• Add new in skill / in behaviour contract assertions to tests/test_weave_git_merge_skill.py for any new wording.
• Keep every existing contract assertion unchanged.

🤖 Prompt for AI agents

Ground the model in real Git behaviour and reconcile the skill documentation,
without touching existing documentation tests.

- Update `tests/test_weave_git_merge_procedures.py`: extend the `_diverge`
helper path to build a two-commit topic branch where both commits touch the
conflicting file. Reuse a single cmd_mox spy across both invocations with a
closure-held counter, returning corrupt content on the first replay and valid
content on the second. Assert `spy.call_count == 2`, inspect
`spy.invocations[0]` and `spy.invocations[1]`, and confirm the corrupt early
result propagates into the second replay's `ours` stage.
- Review `skills/weave-git-merge/SKILL.md` and
`skills/weave-git-merge/references/behaviour.md`. Where a modelled invariant is
implicit, add concise wording that states it plainly. Do not restructure the
documents.
- Add new `in skill` / `in behaviour` contract assertions to
`tests/test_weave_git_merge_skill.py` for any new wording. Keep every existing
contract assertion unchanged.

Research

The weave-git-merge skill documents Weave as a per-file Git merge driver. skills/weave-git-merge/SKILL.md and skills/weave-git-merge/references/behaviour.md define the rules: sequential multi-commit rebase replays where an early corrupt result becomes a later ours stage, three attribute scopes (tracked .gitattributes, clone-local .git/info/attributes, global core.attributesFile) with per-scope bypass rules, and stage semantics (:1: base, :2: ours, :3: theirs) plus the resolved working file.

Two test files exist. tests/test_weave_git_merge_skill.py asserts fixed documentation strings. tests/test_weave_git_merge_procedures.py drives real Git in tmp_path repositories with a cmd_mox-stubbed driver, using helpers such as diverged, _select_scope, _wire_driver, _bypass_prefix, _start_operation, _writing_handler, and _conflict_handler.

Hypothesis is an unpinned dev dependency. Existing property tests live in dedicated _properties.py modules, use plain @given with module-level strategies, and apply @settings(deadline=None, max_examples=50) for subprocess-heavy cases. No RuleBasedStateMachine exists in the repository.

---

🚀 Next Steps

🤖 All AI agent prompts combined

Task: 1

Build the pure-Python behavioural model that encodes the documented
`weave-git-merge` invariants. This model is the system under test for the
property tests in Phase 2, so match each documented rule precisely.

- Create `tests/weave_git_merge_model.py`, following the
`tests/typos_rollout_test_support.py` support-module convention. Do not call Git
from this module; model documented behaviour only.
- Define enumerations for operation type (`rebase`, `merge`) and attribute scope
(`tracked`, `clone-local`, `global`).
- Define a lightweight replay-state type that records, per replayed commit: the
base/ours/theirs inputs, the driver exit code, and whether the produced output
is structurally valid.
- Add a function for attribute-scope fallback that returns the effective `merge`
attribute (`weave` or `unspecified`) for a given scope and applied bypass. The
global scope becomes `unspecified` only under the
`core.attributesFile=/dev/null` override. The tracked and clone-local scopes
become `unspecified` only under a later path-specific `!merge` rule, and stay
`weave` under the `/dev/null` override. Encode the `core.attributesFile`
pitfall: an absent setting means the default global path applies, not the
absence of a global rule.
- Add a function for stage validity that reports the valid stage set (`:1:`,
`:2:`, `:3:`) for a given operation and case, including cases without a base.
Only existing stages may be parsed. During a multi-commit rebase, stage `:2:` is
not a trusted baseline, because it can hold an earlier corrupt replay.
- Add a function for multi-commit replay transitions that folds a sequence of
replay outcomes into per-commit states, where commit N's `ours` input derives
from commit N-1's produced result. A clean-exit but structurally invalid early
result must propagate into the later `ours` stage. Apply the andon rule: flag a
structurally invalid replay as unsafe, and never accept it as a safe later
`ours` stage.
===============================================================================

Task: 2

Add a property-test module that exercises the Phase 1 model with generated
sequences, covering every operation type, every scope, valid and invalid stage
combinations, and at least two replay transitions.

- Create `tests/test_weave_git_merge_properties.py`, following the
`_properties.py` naming and strategy conventions.
- Import Hypothesis as `from hypothesis import given, settings` and `from
hypothesis import strategies as st`.
- Define module-level, `SCREAMING_SNAKE_CASE` strategies for operation types,
scopes, replay-outcome sequences, and stage-combination cases. Apply `@settings`
per test only where needed; the model is pure Python, so a `deadline` override
is not required.
- Add attribute-scope fallback properties: for every scope, the documented
bypass yields `unspecified`; the wrong bypass for a scope does not yield
`unspecified` (for example, `/dev/null` against a tracked or clone-local rule);
the `core.attributesFile` absent-versus-unset property holds for the global
scope.
- Add stage-validity properties: generated cases only ever parse stages that
exist; a parsing stage `:3:` never marks a non-parsing stage `:2:` as safe
during a multi-commit rebase; base-absent cases never expose a `:1:` stage.
- Add multi-commit replay safety properties over generated sequences of length
two or more: a structurally invalid early result is never accepted as a safe
later `ours` stage; a corrupt early replay marks the sequence unsafe even when
later replays parse cleanly; reordering the transition sequence changes the
accepted outcome, so incorrect ordering fails the property.
===============================================================================

Task: 3

Ground the model in real Git behaviour and reconcile the skill documentation,
without touching existing documentation tests.

- Update `tests/test_weave_git_merge_procedures.py`: extend the `_diverge`
helper path to build a two-commit topic branch where both commits touch the
conflicting file. Reuse a single cmd_mox spy across both invocations with a
closure-held counter, returning corrupt content on the first replay and valid
content on the second. Assert `spy.call_count == 2`, inspect
`spy.invocations[0]` and `spy.invocations[1]`, and confirm the corrupt early
result propagates into the second replay's `ours` stage.
- Review `skills/weave-git-merge/SKILL.md` and
`skills/weave-git-merge/references/behaviour.md`. Where a modelled invariant is
implicit, add concise wording that states it plainly. Do not restructure the
documents.
- Add new `in skill` / `in behaviour` contract assertions to
`tests/test_weave_git_merge_skill.py` for any new wording. Keep every existing
contract assertion unchanged.

💡 Iterate on the plan with: `@coderabbitai` <feedback>

Example Feedback
- `@coderabbitai` You can skip phase 3. Add a simple unit test case for phase 2.
- `@coderabbitai` For design choice 1 go ahead with option 3 and replan.

---