From 49df4671cf8ca518c81c2b0437d33da29171a6dc Mon Sep 17 00:00:00 2001 From: Graham Date: Wed, 23 Aug 2023 10:33:19 -0400 Subject: [PATCH] Switch to autorender Previously we were abusing in a way that chrome detested. --- index.html | 124 +++++++++++++++++++++++++-------------------------- src/deck.mjs | 11 ++--- 2 files changed, 65 insertions(+), 70 deletions(-) diff --git a/index.html b/index.html index 472ed8b..729cd75 100644 --- a/index.html +++ b/index.html @@ -22,17 +22,17 @@

Outcome Logic

Motivating example: non-determinism

-

If Σ are some states, ⟦C⟧:Σ→ 𝒫(Σ) is the action of the non-deterministic program C on those states, and σ,τ : Σ and P,Q⊆Σ then: +

If \(Σ\) are some states, \(⟦C⟧:Σ→ 𝒫(Σ)\) is the action of the non-deterministic program \(C\) on those states, and \(σ,τ : Σ\) and \(P,Q⊆Σ\) then:

Hoare Logic:
-
⊨ \{P\}C\{Q\} +
\(⊨ \{P\}C\{Q\}\) iff - ∀σ∈P, ∀τ∈ ⟦C⟧(σ), τ ∈ Q + \(∀σ∈P, ∀τ∈ ⟦C⟧(σ), τ ∈ Q\)
Incorrectness Logic:
-
⊨ [P]C[Q] +
\(⊨ [P]C[Q]\) iff - ∀τ∈Q, ∃σ ∈ P, τ ∈ ⟦C⟧(σ) + \(∀τ∈Q, ∃σ ∈ P, τ ∈ ⟦C⟧(σ)\)
@@ -40,29 +40,29 @@

Motivating example: non-determinism

Hoare Logic:

- P + \(P\) - Q + \(Q\) - ⟦C⟧^\dagger(P) + \(⟦C⟧^\dagger(P)\) -

Postcondition Q “over-approximates” ⟦C⟧^\dagger(P), it's allowed to include some unreachable outcomes.

+

Postcondition \(Q\) “over-approximates” \(⟦C⟧^\dagger(P)\), it's allowed to include some unreachable outcomes.

Incorrectness Logic:

- P + \(P\) - Q + \(Q\) - ⟦C⟧^\dagger(P) + \(⟦C⟧^\dagger(P)\) -

Postcondition “under-approximates” ⟦C⟧^\dagger(P), it's allowed to leave out some reachable outcomes

+

Postcondition “under-approximates” \(⟦C⟧^\dagger(P)\), it's allowed to leave out some reachable outcomes

Both HL and IL combine two difference sources of outcome multiplicity:

@@ -75,47 +75,47 @@

Incorrectness Logic:

Heisenbugs: “Every state in the precondition can (sometimes, nondeterministically) produce an error”

Correct Shuffles: “Each of several postconditions is (sometimes, nondeterministically) reachable from every state in the precondition”

-

Manifest Errors (Le et al.): “Executing C on any state terminates erroniously in some state satisfying…”

+

Manifest Errors (Le et al.): “Executing \(C\) on any state terminates erroniously in some state satisfying…”

Idea for a solution:

-

look at properties of the sets ⟦C⟧(x) for x∈ P, or actually more generally, ⟦C⟧^\dagger(X) for X \subseteq P.

-

A Heisenbug means that ⟦C⟧^\dagger(X) overlaps error, for any choice of X\subseteq P.

-

A fair shuffle means that ⟦C⟧^\dagger(X) covers your shuffle outcomes, for any choice of X\subseteq P.

+

look at properties of the sets \(⟦C⟧(x)\) for \(x∈ P\), or actually more generally, \(⟦C⟧^\dagger(X)\) for \(X \subseteq P\).

+

A Heisenbug means that \(⟦C⟧^\dagger(X)\) overlaps error, for any choice of \(X\subseteq P\).

+

A fair shuffle means that \(⟦C⟧^\dagger(X)\) covers your shuffle outcomes, for any choice of \(X\subseteq P\).
Generic Outcome Logic:
-
⊨ ⟨φ⟩C⟨ψ⟩ +
\(⊨ ⟨φ⟩C⟨ψ⟩\) iff - ∀S⊨φ,\qquad ⟦C⟧^\dagger(S) ⊨ ψ + \(∀S⊨φ,\qquad ⟦C⟧^\dagger(S) ⊨ ψ\)

Because we're interested in properties of - ⟦C⟧^\dagger(X), we need to promote ⊨ + \(⟦C⟧^\dagger(X)\), we need to promote \(⊨\) from a relation between states and assertions to a relation between sets of states and assertions.

To do this (and get the nondeterministic outcome logic from the paper) we supply:

    -
  1. An execution model: basically 𝒫,∪,\varnothing (details postponed).
    2. -
  2. Atomic commands Σ→𝒫(Σ).
    3. -
  3. Atomic assertions \mathsf{Prop}, and an +
  4. An execution model: basically \(𝒫,∪,\varnothing\) (details postponed).
    5. +
  5. Atomic commands \(Σ→𝒫(Σ)\).
    6. +
  6. Atomic assertions \(\mathsf{Prop}\), and an atomic satisfaction relation, in this case:
    - S ⊨ p iff S ≠ \varnothing and ∀σ∈S, σ ∈ v(p). + \(S ⊨ p\) iff \(S ≠ \varnothing\) and \(∀σ∈S, σ ∈ v(p)\).
Given our atomic assertions, we build an assertion language as follows:

- φ::= ⊤ \mid ⊥ \mid φ∧ψ \mid φ⇒ψ \mid φ\oplus ψ \mid ⊤^\oplus\mid p -

and we extend satisfaction (skipping classical connectives ⊤,⊥,∧, ⇒):

+ \(φ::= ⊤ \mid ⊥ \mid φ∧ψ \mid φ⇒ψ \mid φ\oplus ψ \mid ⊤^\oplus\mid p\) +

and we extend satisfaction (skipping classical connectives \(⊤,⊥,∧, ⇒\)):

- + - +
S ⊨ φ\oplusψ iff S=T∪R where T ⊨ φ, R ⊨ ψ\(S ⊨ φ\oplusψ\) iff \( S=T∪R\) where \(T ⊨ φ, R ⊨ ψ\)
S ⊨ ⊤^\oplus iff S=\varnothing\(S ⊨ ⊤^\oplus\) iff \( S=\varnothing\)
@@ -124,39 +124,39 @@

Idea for a solution:

Observe:

 - S ⊨ φ\oplus ⊤^\oplus just in case S ⊨ φ. + \(S ⊨ φ\oplus ⊤^\oplus\) just in case \(S ⊨ φ\). - ⟨Q⟩C⟨⊤^\oplus⟩ just in case ⟦C⟧^\dagger(Q) = \varnothing + \(⟨Q⟩C⟨⊤^\oplus⟩\) just in case \(⟦C⟧^\dagger(Q) = \varnothing\) - ⟨φ⟩C⟨⊥⟩ just in case ∀S, S\nvDash φ + \(⟨φ⟩C⟨⊥⟩\) just in case \(∀S, S\nvDash φ \) -

⟨φ⟩C⟨ψ∨⊤^\oplus⟩ expresses partial +

\(⟨φ⟩C⟨ψ∨⊤^\oplus⟩\) expresses partial correctness.

Holds just in case given a set of states - satisfying φ, ⟦C⟧^\dagger produces - either a set of states satisfying ψ, or the empty + satisfying \(φ\), \(⟦C⟧^\dagger\) produces + either a set of states satisfying \(ψ\), or the empty set.

-

⟨φ⟩C⟨p\oplus - ⊤⟩ expresses under-approximation.

holds just in - case every set of states satisfying φ - contains some member that ⟦C⟧ sends to - a state contained in v(p).

+

\(⟨φ⟩C⟨p\oplus + ⊤⟩\) expresses under-approximation.

holds just in + case every set of states satisfying \(φ\) + contains some member that \(⟦C⟧\) sends to + a state contained in \(v(p)\).

 We also build a command language, but we'll skip that

We get a lot of expressive power.

    -
  1. Hoare Triples: \{p\}C\{q\} iff ⟨p⟩C⟨q∨⊤^\oplus⟩
    2. -
  2. Heisenbugs: ⟨φ⟩C⟨\mathsf{err}\oplus ⊤⟩
    3. -
  3. Fair Shuffle: ⟨φ⟩C⟨p\oplus q\oplus r …⟩
    4. +
  4. Hoare Triples: \(\{p\}C\{q\}\) iff \(⟨p⟩C⟨q∨⊤^\oplus⟩\)
    5. +
  5. Heisenbugs: \(⟨φ⟩C⟨\mathsf{err}\oplus ⊤⟩\)
    6. +
  6. Fair Shuffle: \(⟨φ⟩C⟨p\oplus q\oplus r …⟩\)
-

Given a concrete Σ, concrete command language generating - C, and concrete atoms p, you can +

Given a concrete \(Σ\), concrete command language generating + \(C\), and concrete atoms \(p\), you can equip OL with a sound proof system to reason about the above.

@@ -167,31 +167,31 @@

Idea for a solution:

Corollary to big theorem:

Nondeterministic OL can falsify HL triples

-

we have \nvDash\{p\}C\{q\} just in case for some φ⇒p where φ is satisfiable, ⟨φ⟩C⟨\bar{q}\oplus ⊤⟩

-

Or anyway, this holds if C is guaranteed to terminate.

+

we have \(\nvDash\{p\}C\{q\}\) just in case for some \(φ⇒p\) where \(φ\) is satisfiable, \(⟨φ⟩C⟨\bar{q}\oplus ⊤⟩\)

+

Or anyway, this holds if \(C\) is guaranteed to terminate.

Generalizing

-

What is ⟦C⟧^\dagger?

-

Intuitively, ⟦C⟧ : Σ → 𝒫(Σ)

-

But, ⟦C⟧^\dagger : 𝒫(Σ) → 𝒫(Σ)

+

What is \(⟦C⟧^\dagger\)?

+

Intuitively, \(⟦C⟧ : Σ → 𝒫(Σ)\)

+

But, \(⟦C⟧^\dagger : 𝒫(Σ) → 𝒫(Σ)\)

So you do the obvious thing:

-

⟦C⟧^\dagger(X) := \bigcup\{⟦C⟧(x) | x ∈ X\}

+

\(⟦C⟧^\dagger(X) := \bigcup\{⟦C⟧(x) | x ∈ X\}\)

which is really a completely general construction:

-

\mathsf{bind}:𝒫(A)→(A→𝒫(B))→𝒫(B)

+

\(\mathsf{bind}:𝒫(A)→(A→𝒫(B))→𝒫(B)\)

 -

It turns out that this \mathsf{bind}, along with the singleton constructor for \mathsf{unit}:A→𝒫(A), make 𝒫 a monad.

-

It also has a little bit of extra structure: ∪ and \varnothing make 𝒫(X) a commutative monoid, for any X.

+

It turns out that this \(\mathsf{bind}\), along with the singleton constructor for \(\mathsf{unit}:A→𝒫(A)\), make \(𝒫\) a monad.

+

It also has a little bit of extra structure: \(∪\) and \(\varnothing\) make \(𝒫(X)\) a commutative monoid, for any \(X\).

So, callback to earlier:

-

An execution model is a triple ⟨M,⬦,\mathbf{1}⟩, where M is a Monad, and ⬦,\mathbf{1} are the multiplication and unit providing a (partial, commutative) monoid structure on every M(X) +

An execution model is a triple \(⟨M,⬦,\mathbf{1}⟩\), where \(M\) is a Monad, and \(⬦,\mathbf{1}\) are the multiplication and unit providing a (partial, commutative) monoid structure on every \(M(X)\)

-

Outcome logic can be made parametric on a choice of monad, M, monoid structure on each M(X), and clause for ⊨p

+

Outcome logic can be made parametric on a choice of monad, \(M\), monoid structure on each \(M(X)\), and clause for \(⊨p\)

The cash value of that fact is that:

  1. You get a principled way of generalizing the semantics @@ -207,18 +207,18 @@

    Generalizing

 -

For example, given error states E, the error - monad is given by \mathsf{Er}_E(X) = E+X, with - \mathsf{bind}_E propagating error states, and \mathsf{unit}_E just the right-hand inclusion. +

For example, given error states \(E\), the error + monad is given by \(\mathsf{Er}_E(X) = E+X\), with + \(\mathsf{bind}_E\) propagating error states, and \(\mathsf{unit}_E\) just the right-hand inclusion.

-

\mathsf{Er}_E has the following nice property: there's a uniform way to - give M \circ \mathsf{Er}_E a monad structure, for - any monad M. +

\(\mathsf{Er}_E\) has the following nice property: there's a uniform way to + give \(M \circ \mathsf{Er}_E\) a monad structure, for + any monad \(M\).

- So, if ⟨M,⬦,\mathbf{1}⟩ is an execution model, so is ⟨M\circ \mathsf{Er}_E,⬦,\mathbf{1}⟩. + So, if \(⟨M,⬦,\mathbf{1}⟩\) is an execution model, so is \(⟨M\circ \mathsf{Er}_E,⬦,\mathbf{1}⟩\).

In particular, we get an execution model for non-determinism with errors, which the authors use for non-deterministic separation logic.

diff --git a/src/deck.mjs b/src/deck.mjs index b3caab0..d4d5b74 100644 --- a/src/deck.mjs +++ b/src/deck.mjs @@ -1,4 +1,5 @@ -import Katex from "https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/katex.mjs" +import Katex from "https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/katex.mjs"; +import renderMathInElement from "https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/contrib/auto-render.mjs"; const registry = window.customElements @@ -110,13 +111,7 @@ class RazzleDeck extends HTMLElement { shadow.appendChild(kclone); shadow.appendChild(svgDefs); [...children].map(child => { - const mathElements = child.querySelectorAll("math") - for (let element of mathElements) { - Katex.render(element.textContent, element, { - throwOnError: false, - displayMode: [...element.classList].includes("d") - }); - }; + renderMathInElement(child) shadow.appendChild(child) })