Skip to content

[2/7] Invariant order, locality, trivial spaces, precision, sums - #3

Open
zilberstein wants to merge 10 commits into
mainfrom
claude/happy-noether-41vna7-part2
Open

[2/7] Invariant order, locality, trivial spaces, precision, sums#3
zilberstein wants to merge 10 commits into
mainfrom
claude/happy-noether-41vna7-part2

Conversation

@zilberstein

@zilberstein zilberstein commented Oct 1, 2026

Copy link
Copy Markdown
Owner

Part 2 of the stack splitting #1 (based on part 1).

Contents

  • Invariants ordered by factorization (Inv.LE_Inv); proof of invariant monotonicity.
  • Locality: memory bookkeeping in the frame lemmas.
  • Script listing declarations that use sorry.
  • Laws: oplus_distrib, introduction half of sure_sep.
  • Probability spaces without probabilistic information (TrivialSpace.lean).
  • Precision: the paper's definition, with proofs for ⌈P⌉ and ∗, and for outcome conjunctions.
  • Outcome conjunctions range over countable index types.
  • Sums: shifting spaces to disjoint outcomes, monotonicity of sums (Lemma B.5).
  • DESIGN.md updates (invariant order, precision).

🤖 Generated with Claude Code

https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug

Generated by Claude Code

@zilberstein
zilberstein added this pull request to stack #8 October 1, 2026 12:22
Base automatically changed from claude/happy-noether-41vna7-part1 to main October 8, 2026 16:56
claude added 10 commits October 8, 2026 12:56
@claude
Invariants: factorization order, proving invariant monotonicity
22cd010 
The order on invariants was projection: `𝓘 ≤ 𝓙` when `𝓙` is the
restriction of `𝓘` to fewer variables.  Invariant-sensitive execution is
not monotone along that order, so the `sorry` in `Inv.replace_monotone`
(which every `wp` depended on, through the `MonoSem` instance) could not
be filled.  Counterexample: `𝓘` constrains `a` and `b` to be equal, `𝓙`
only says `a ∈ {0, 1}`; replacing the invariant part of `{a=0, b=0}`
under `𝓙` can produce `{a=1, b=0}`, which it cannot under `𝓘`.

The order is now factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is
`𝓙 ∗ 𝓚` for some invariant `𝓚` on the other variables, which is the
situation of Lemma 5.3 of the paper (`I ∗ J`).  With it:

* `Inv.replace_le` / `Inv.checkReplace_monotone`: checking and then
  replacing the invariant is monotone (replacing alone is not, which is
  why the old lemma is gone);
* the `MonoSem` instance is proved;
* the DCPO structure is simplified: a directed set of invariants has a
  greatest element (the one with the fewest variables, preferring
  nonempty ones), which is its supremum;
* `Cmd.withInv_monotone` is proved, including the `while` and action
  cases (`pom_singleton_mono`), and `Inv.le_emp` gives the step needed
  in `wp_share`.

`Semantics/Invariant.lean` no longer contains any `sorry`, and `wp_seq`
is now proved without axioms beyond Lean's standard ones.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Locality: fill the memory bookkeeping in the frame lemmas
e83132d 
The remaining `sorry`s in `sem_withInv_frame` and `sem_withInv_indep`
were pointwise identities about overwriting the invariant part of a
memory.  They follow from a new general lemma,
`Mem.union_restrict_of_subset`: restricting commutes with overwriting by
a memory that lives inside the restriction.

With this, `Pom.par_comp` (Lemma C.5) is proved without `sorry`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Add a script listing the declarations that use sorry
db0c09a 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Laws: prove oplus_distrib and the introduction half of sure_sep
e234635 
* `sumProd_le_sum_product` / `sum_product_le_sumProd` restate the
  distributive law of products over sums (`sum_prod_distribute`) as
  inequalities for the new order.
* `oplus_distrib`: a frame can be pushed into the branches of an outcome
  conjunction.
* `sure_sep_intro`: `⌈P⌉ ∗ ⌈Q⌉ ⊢ ⌈P ∗ Q⌉`.  The other direction of
  `sure_sep` needs the two assertions to have fixed footprints (it has to
  split the probability space along the variables), and stays `sorry`
  for now.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Probability spaces without probabilistic information
ab3f01d 
`ProbSpace.trivialOn V f` has the trivial σ-algebra `{∅, ℕ}` and memories
`f`: it records which memories over `V` are possible, but no
probabilities.  Every outcome is in its support (`support_trivialOn`),
and it is below any space that owns `V` and whose memories almost surely
extend memories of `f` (`trivialOn_le`).  These spaces are the least
models of almost sure assertions.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Precision: the paper's definition, and proofs for ⌈P⌉ and ∗
9179114 
`Precise` now follows Definition 4.1: if `φ` is satisfiable, then it has
a least model.  Previously it also required satisfiability, which made
e.g. the invariant of the von Neumann example imprecise for an empty set
of biases.

* `Precise.sure` was false as stated (`⌈x = 1 ∨ y = 1⌉` has no least
  model).  As in the paper, where `⌈P⌉` is interpreted over the
  variables of `P`, it now requires `P` to have a finite footprint
  (`MProp.Footprint`); the least model is the space without
  probabilistic information whose memories are those satisfying `P`.
  Footprint lemmas are provided for `emp`, `x == v`, `own x`,
  conjunctions, equations `e == c`, and invariants.
* `Precise.sep` is proved: the least model is the product of the least
  models.
* `wp_par` obtains the satisfiability of the postconditions by running
  each thread alone, using the new `Framed.left` / `Framed.right`, which
  split a framed product between the two threads.

The examples supply the footprints of their precise assertions.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
DESIGN: record the invariant order and the treatment of precision
63dde87 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Outcome conjunctions range over countable index types
6f4b9c5 
`ProbSpace.sum` requires its summands to have pairwise disjoint (and
nonempty) sets of outcomes in `ℕ`.  Over an uncountable index type no
such family exists, so `⨁[ξ] φ` and `& φ` were unsatisfiable there.
They now require `[Countable ι]`, which holds for all index types used in
practice (values, booleans, finite sets of biases, ranks), and which
allows summands to be moved to disjoint parts of `ℕ` by an injection.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Sums: shifting spaces to disjoint outcomes, and monotonicity (Lemma B.5)
5ae36b7 
* `ProbSpace.shift p c` renames the outcome `n` of `p` to the pair
  `(c, n)`.  It carries the same information as `p` (`shift_le`,
  `le_shift`), and shifts by different `c` have disjoint supports
  (`disjoint_support_shift`), so the summands of an outcome conjunction
  can always be made disjoint.
* `ProbSpace.sum_mono` (Lemma B.5): a sum grows when each summand of
  positive weight grows.  The relabeling of the sum is assembled from the
  relabelings of the summands, which is possible because the summands
  have disjoint supports.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@claude
Precision of outcome conjunctions
624f94e 
The summands of a sum own the same variables, so the precision rule for
`⨁` needs the least models of the branches to own the same variables.
`PreciseDom φ V` is precision where the least model owns exactly `V`;
`⌈P⌉` with footprint `V` has it (`Precise.sureDom`), and so does
`⨁[ξ] φ` when every branch does (`Precise.oplusDom`).  The least model of
the outcome conjunction is the sum of the least models of the branches,
shifted to disjoint outcomes; minimality follows from monotonicity of
sums.  As explained in DESIGN.md, the indexed model makes the
partitioning side condition of the paper's rule unnecessary.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
@zilberstein
zilberstein force-pushed the claude/happy-noether-41vna7-part2 branch from 45edd2f to 624f94e Compare October 8, 2026 16:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@zilberstein @claude