Repository navigation
[5/7] Assign, Bern, If, Share and Atom rules - #6
Open
zilberstein wants to merge 12 commits into
Open
zilberstein wants to merge 12 commits into
zilberstein wants to merge 12 commits into
Conversation
zilberstein
added this pull request to stack #8
October 1, 2026 12:22
Refines.bind: if a space is refined by μ, and a kernel only produces memories extending prescribed ones (one per outcome of the space), then running the kernel refines the space with those memories. This is the semantic core of the assignment rules. Also Refines.exists_le, Refines.sure, the memories of the padding space, and lemmas about Mem.extend. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Fixes the build broken by the previous commit, which moved this lemma. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Actions.lean describes the possible outcomes of an action run under an invariant (SupportedIn is preserved by the monad operations). With Refines.bind and Refines.pad, wp_assign follows: the program's part of the space is updated in place, and the invariant's part is rebuilt from the final memories. The expression must be local (Expr.Local: monotone, and defined after an assignment), so that its value survives interference and own e survives the assignment; the examples pass this for literals, variables and xor. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Factor the analysis of a run of an assignment out of wp_assign (assign_run), and use it for wp_assign_pres: after the assignment, the parts of the space over x and over the other variables carry the values of x and of e. wp_assign_pres now also asks for e to be monotone. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
ofPMF_product_le computes the product of two discrete spaces, and Refines.prod lifts it to refinement: independent draws from distributions refining two spaces refine their product. This is what makes freshly sampled values independent of the rest of the state. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Det describes actions whose outcome is a fixed distribution; with it, sem_samp_withInv gives the outcome of x :≈ Bern e under an invariant exactly: interference on the invariant's variables, then an independent sample. sampleSpace x ξ is the space of a fresh sample: it satisfies x ~ ξ and is refined by the distribution of the sample. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
bern_run analyses a run of x :≈ Bern e: the interference on the invariant's variables refines the program's part of the space without x (Refines.bind), and the fresh sample is independent of it (Refines.prod with sampleSpace). wp_bern follows; like the assignment rules, it asks for the expression to be local. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
wp_bern_pres was assumed in the von Neumann example; it is a general rule, so it moves to WeakestPre and is proved from bern_run: after the sampling, the rest of the program's space still knows the value of e, and the fresh sample is independent of it. Like wp_assign_pres, it asks for e to be monotone. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
The guard must be monotone, so that the value it has in the precondition is its value in the initial memories; the test then selects the first branch in every run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Running a program without interference is one of the behaviours of running it under the invariant. The shared resource is added to the invariant's space for the run, and recovered from the final invariant space. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
mem_bind_of_mixture averages nondeterministic choices made from different initial memories into one kernel on the averaged distribution (using posterior probabilities and convexity of the semantics). Also: an action under the empty invariant runs as itself, and the decomposition of a run under an invariant into interference, the action and the final check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
A run of an atomic action under an invariant is interference on the invariant's variables, the action, and a check. After the interference, the precondition and frame are unchanged and a space without probabilistic information satisfies the invariant, so the premise (the action run without interference re-establishes the invariant) applies. It shows first that every run re-establishes the invariant, so the final check always passes; the per-memory choices of the action are then averaged into one run. 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-part5
branch
from
October 8, 2026 16:56
dbe1bbc to
0785c53
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 5 of the stack splitting #1 (based on part 4).
Contents
Mem.extendalgebra.Actions.lean: runs of assignments and samples.Assignand value-preservingAssignrules (expressions must beExpr.Local).Bernand value-preservingBernrules.Ifrule for a guard that holds (Expr.Monoguards).Sharerule.Atomrule.Note: commit 65e3c52 in this slice does not build on its own (fixed by the next commit, 80e24d6); the slice head builds.
🤖 Generated with Claude Code
https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Generated by Claude Code