Module worktree_dirty_restore 

The restore of a snapshot of a main checkout with uncommitted changes, and its proof. What: The restore of a snapshot of a main checkout that had uncommitted changes: make the copy’s index and files equal the tree of the new worktree’s HEAD with git read-tree --reset -u and git clean -f -d, then prove it in the stage. Why: git worktree add from a checkout with changes makes a worktree that holds the committed files and nothing of the changes. The snapshot carries the changes, so the copy is reset the way Git’s own reset --hard would reset it, from the index the snapshot carries: that index still records the files as they were before they were edited, so the reset rewrites exactly the edited, deleted and staged paths and leaves the rest. Untracked files that no ignore rule covers go, ignored files stay. Both Git runs are the ladder’s own steps on the new worktree (its Git directory and its stage), started as real Git children by the lifecycle’s runner, so no policy of the wrapper that guards a person’s reset or clean applies to them. The proof runs before the stage is swapped in; a proof that fails ends the rung and Git’s own checkout makes the worktree. The main checkout is read only to be snapshotted and listed, and is never written.

In TS you’d write (pseudocode):

await restoreDirtySnapshot({ source, target, stage, runGit, context }); // throws the reason it cannot be proven

Functions

left_out_note

What: The line that tells the person a snapshot of a checkout with changes left the changes out. Why: The new worktree matches a clean git worktree add, which the person may not expect from a copy of a dirty checkout.

prove_restored

What: Prove that the stage equals what Git’s checkout of the target commit makes: the index equals the commit’s tree, Git shows no untracked file, and no tracked file differs from the index. Why: The restore trusts Git’s reset and clean; the proof asks Git again from the other side, so a state either of them left (a path the reset skipped, a directory the clean could not remove) ends the rung instead of reaching the person.

record_left_out

What: Record in the journal, at the ordinary level, that a snapshot left the uncommitted changes of the main checkout out of the new worktree, with the destination and the number of paths as fields. Why: The line on standard error is gone when the command ends; the journal keeps what the add did with a dirty checkout.

restore_dirty

What: Restore the stage, which is a snapshot of source made with its own index, to the tree of the target commit, and prove it. Why: See the module description. The stage is never the source’s own directory, and the Git directory is the new worktree’s, so neither run can reach the main checkout.