Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic

• p. 29 Section 4.4, second bullet

  the camera version of a frame-preserving update implies the RA version.

• p. 9 Figure 3, frame-preserving update definition

  a ⇝B

• p. 30 Figure 9, frame-preserving update definition

  a ⇝B

• p. 29 §4.4, second bullet, last sentence

  the camera version of a frame-preserving update implies the RA version

Only the authors can say what is right here.

Judge's note: I checked Fig. 3 (p. 9): RA a ⇝ B ≜ ∀c?. V̄(a·c?) ⇒ ∃b∈B. V̄(b·c?). Fig. 9 (p. 30): camera a ⇝ B ≜ ∀n,c?. n∈V(a·c?) ⇒ ∃b∈B. n∈V(b·c?). In the camera version b may depend on n, so getting the RA version means swapping ∀n and ∃b, which is not valid in general. I checked reviewer 2's counterexample myself. Carrier {ε, a, ↯, b_k}, discrete OFE. ε is the identity and every other product is ↯. V(ε)=V(a)=ℕ, V(b_k)={0..k}, V(↯)=∅, and the core is always ε. ASSOC and COMM hold because ↯ absorbs. CORE-ID, CORE-IDEM and CORE-MONO hold trivially. VALID-OP holds: a product is either ↯ (validity ∅) or equal to one of its factors. EXTEND is trivial because the OFE is discrete. Camera update a ⇝ {b_k}: the only frames that keep a valid are ⊥ and ε, and b_n works at index n, so the update holds. RA update: V̄(a) holds, but V̄(b_k) fails for every k, so the update fails. The printed general claim is therefore false as stated. It is a side remark that holds for deterministic B (a ⇝ b) and for cameras built from RAs, and nothing later appears to depend on it. Hence minor, S3.

Second check: another model agreed

• p. 49 Section 6.3.3, paragraph following the authoritative camera definition

  validity of • a · ◦b implies b ≼a.

• p. 30 Figure 9, CAMERA-INCL

  a ≼b ≜∃c. b = a · c

Only the authors can say what is right here.

Judge's note: I checked p. 49. •a·◦b = (ex(a), b), whose validity is {n | n∈V(a) ∧ b ≼ⁿ a}. Even validity at every n only gives ∀n. b ≼ⁿ a, with a witness that may depend on n. I checked the reviewer's counterexample. M is the zero sequence plus all nonnegative rational sequences with infinite support. Composition is pointwise addition, unit and core are zero, everything is valid at every index, and x =ⁿ y means coordinates 0..n agree. M is closed under addition, because nonnegative sequences cannot cancel. EXTEND holds: copy b1 and b2 on the prefix and put a/2 on each tail, which keeps infinite support; a=0 is handled with zeros. Take a=(2,1,1,…) and b=(1,1,1,…). For each n, c_n=(1,0,…,0,1,1,…) with zeros at coordinates 1..n is in M, and b+c_n agrees with a on coordinates 0..n. The only exact remainder, a−b=(1,0,0,…), is not in M, so b ≼ a fails while •a·◦b is valid at every index. The paper elsewhere allows incomplete OFEs and cameras, so the claim is false for general M. It does hold for discrete M, such as the heap instance used right afterwards, so this is a side remark of limited impact.

Second check: another model agreed

• p. 35 Fig. 10, line for the guarded fixed-point

  μx. t : iPropρ ≜fixτ(λu. t : iPropρ[x ←u])

• p. 34 §5, grammar of terms

  μx : τ. t

Only the authors can say what is right here.

Judge's note: p35 image shows the line as quoted: iProp on both sides, subscript ⟦τ⟧ on fix, and no type annotation on the binder. The p34 grammar has μx : τ. t. The line mixes the general and the iProp-specialised form; either the type should be τ throughout or the subscript should be ⟦iProp⟧. Authors to say which.

Second check: another model agreed

• p. 52 Fig. 14, definition of W

  W ≜∃I : N fin −⇀iProp.

• p. 52 §7.1.1, displayed definition of W

  W ≜∃I : N →iProp.

• p. 53 §7.1.1, first line

  Here, I : N →iProp is a registry of all existing invariants.

• p. 52 Fig. 14

  W ≜ ∃I : ℕ ⇀fin iProp.

Judge's note: Checked pages 52–53. Fig. 14's definition of W carries a 'fin' decoration on the arrow. The §7.1.1 display and the first sentence on p53 use a plain →. The camera AUTH(ℕ ⇀fin AG(▶iProp)) and the side condition ι ∉ dom(I) both need a finite partial map. The inconsistency is in the notation; the intended meaning is clear from context.

Second check: another model agreed

• p. 62 §8.1, View shifts versus fancy updates

  encoded in terms of the fancy update modality as P −∗ |⇛ E1 E2 Q

• p. 56 §7.2, definition of view shifts

  Q ≜□(P −∗ |⇛ E1 E2 Q)

• p. 62 §8.1, 'View shifts versus fancy updates'

  As demonstrated in §7.2, view shifts P E1⇛E2 Q can be encoded in terms of the fancy update modality as P −∗ E1|⇛E2 Q

• p. 56 §7.2 definition of view shifts

  P E1⇛E2 Q ≜□(P −∗ E1|⇛E2 Q)

Judge's note: The page 62 image shows the encoding without □. Fig. 14 on p52 (repeated in §7.2) defines the view shift as □(P −∗ |⇛ Q). The □ makes view shifts persistent, so the restated form differs from the definition it cites. This is probably informal shorthand in the discussion.

Second check: another model agreed

• p. 17 §2.4, proof of check, list item 2

  Case 2 (P “on the right”, I “on the left”)

• p. 17 §2.4, proof of check, list item 3

  Case 2 (P “on the right”, I “on the right”)

• p. 17 Proof of check, list item 3

  3. Case 2 (P “on the right”, I “on the right”):

• p. 17 Proof of check, list item 3

  3. Case 2 (P “on the right”, I “on the right”)

Judge's note: Page 17 image shows list items 2 and 3 both with the bold label 'Case 2'; item 1 on the previous page is 'Case 1'. The three cases are distinct combinations, not sub-cases. Mislabelled case heading, cosmetic.

Second check: none (judge only)

• p. 28 §4.3, first display

  ag(P) · ag(Q) =

• p. 18 §3.1, Agreement

  AG0(X) ≜ag0(x : X) |

Judge's note: p28 crop shows 'ag' with no subscript in the display and in the sentence after it, while the passage is about AG0(T) (p27) and p18 defines AG0 with constructor ag0. The subscript is missing; the meaning is clear from context, so this is a minor notation slip.

Second check: none (judge only)

• p. 19 §3.2, first paragraph

  propositions of the form l →v

• p. 19 §3.2, first paragraph

  propositions of the form l ↦ v

Judge's note: Crop of p19 shows an italic Latin 'l' before ↦; pages 3, 8 and 53 show the script ℓ in the same points-to notation. Typographic inconsistency only.

Second check: none (judge only)

• p. 56 §7.2, paragraph after the list of roles

  strip laters of timeless propositions

Judge's note: Crop of p56 shows 'strip laters of timeless propositions (⋄-TIMELESS)'. p42 uses 'strip laters off of'. A small wording slip that is still readable as written.

Second check: none (judge only)

• p. 58 §7.2, proof of INV-OPEN, first bullet

  E \ ι γEN

Judge's note: p58 crop: first bullet shows the boxed token E \ ι without braces; the second bullet and the INV-OPEN rule show E \ {ι}. Missing braces, meaning unaffected.

Second check: none (judge only)

• p. 60 §7.3, derivation of WP-INV, line labelled INV-ACCESS

  x. |⇛ E\N E Φ(v)

Judge's note: Viewed the crop of the derivation on PDF page 60. The four lines above bind 'v.' and use Φ(v); the INV-ACCESS conclusion line binds 'x.' while still using Φ(v), which leaves v unbound. Clear slip with an evident fix; cosmetic, since the intended meaning is obvious.

Second check: none (judge only)

• p. 60 Derivation of WP-INV, line obtained by INV-ACCESS

  wpE\N e {x. E\N|⇛E Φ(v)}

Judge's note: The page 60 image shows 'x.' in the line above WP-ATOMIC. Every other line uses the binder v. This is a typo in the binder.

Second check: none (judge only)

• p. 73 References, O'Hearn (2007)

  TCS, 375(1), 271–307

• p. 71 References, Brookes (2007)

  TCS, 375(1–3), 227–270

• p. 71 References, Brookes (2007)

  TCS, 375(1–3), 227–270.

• p. 73 References, O’Hearn (2007)

  TCS, 375(1), 271–307.

Judge's note: Rests on outside knowledge: that the two papers appeared in the same issue of Theoretical Computer Science vol. 375 and what that issue's number is (1–3 or 1). Viewed the page 71 and page 73 crops: the entries read as quoted. Contiguous pages (270 then 271) in the same volume and year make a single issue likely, so the issue field is inconsistent between the two entries, but the files cannot say which form is right. Cosmetic either way; both entries remain findable.

Second check: none (judge only)