Repository navigation
[3/7] Skip and Frame rules; wp side conditions - #4
Open
zilberstein wants to merge 7 commits into
Open
zilberstein wants to merge 7 commits into
zilberstein wants to merge 7 commits into
Conversation
`wp_skip` claimed `φ ⊣⊢ wp skip φ`. The reverse entailment is stronger than the paper's Skip rule, is unused, and does not hold in this model (`wp` holds vacuously of preconditions that no distribution realizes). It is now the paper's rule `φ ⊢ wp skip φ`, proved: running `skip` from `μ` produces the distributions above `μ`, and `μ` has no mass on `⊥`, so it is maximal. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
* `ProbSpace.product_trivialOn_le`: a space without probabilistic information is independent of every other space: if `X ≤ Z` and the memories of `T` are restrictions of those of `Z`, then `X ⊗ T ≤ Z`. * `ProbSpace.forget Z U`: the part of `Z` over the variables `U`, keeping only which memories are possible. * `OProp.sure_sep_elim`: `⌈P ∗ Q⌉ ⊢ ⌈P⌉ ∗ ⌈Q⌉` when `P` and `Q` have footprints; the two factors are the forgotten parts of the space over the two footprints. `sure_sep` (both directions) now takes the footprints, and `MProp.Footprint.sep` gives the footprint of `P ∗ Q`. * `Mem.union_le`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
`oplus_distrib'`: `⨁ (φ v ∗ ψ) ⊢ (⨁ φ) ∗ ψ` for precise `ψ` (the paper's law for factoring precise assertions out of outcome conjunctions). The frame is satisfied by the least model `𝓠` of `ψ` in every branch. The rest of branch `v` is completed by the variables it does not constrain (`forget`, which is independent of everything) so that all branches own the same variables, and the branches are shifted to disjoint outcomes; the product with `𝓠` is then below the original sum by distributivity and monotonicity of sums. This also proves `oplus_collapse`, `nondet_distrib'` and `nondet_collapse`, which were stated in terms of it. `ProbSpace.product_swap_right` rearranges nested products. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
`ProbSpace.sum_pure_le`: a sum over a point mass is below its summand (the other summands are irrelevant, and the rest of the space is null). With it, `nondet_intro` (`φ i ⊢ & φ`), which the example had to assume, is proved: a space is a one-point mixture of a shifted copy of itself. The obstruction described in the example (memories compared at null outcomes, no relabeling) was removed by the new order. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
`wp_frame`: `φ ∗ wp c ψ ⊢ wp c (φ ∗ ψ)`. The program is run with its frame extended by the space of `φ` (`Framed.right`), and the result is regrouped with the new `Framed.unright`, which moves the left factor of the frame back into the program's space. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Programs do not acquire variables, matching the paper's fixed memory footprint. With this, the postconditions of the two threads in wp_par own disjoint variables, which closes the disjointness sorry there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Add Distr.Keeps μ ν (every variable allocated in all memories of μ is allocated in all memories of ν) to wp_base and to Lemma C.6. The paper gets this for free from its fixed memory domain. It is needed for the Split rule: the postconditions of the branches may own fewer variables than the preconditions, and must be padded back to a common domain from the final memories. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
zilberstein
force-pushed
the
claude/happy-noether-41vna7-part3
branch
from
October 8, 2026 16:56
67b185e to
f78b4d8
Compare
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.
Part 3 of the stack splitting #1 (based on part 2).
Contents
Skiprule.⌈P ∗ Q⌉(with footprints).nondet_introin the von Neumann example.Framerule.wpguarantees that the postcondition owns no more variables than the precondition, and that programs do not deallocate variables (Distr.Keeps).🤖 Generated with Claude Code
https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Generated by Claude Code