A Formally Verified Compiler Back-End

Xavier Leroy

Journal of Automated Reasoning, 2009 · paper · Computer science

Describes the development and machine-checked verification, in the Coq proof assistant, of a compiler back-end from the Cminor intermediate language to PowerPC assembly. The verification guarantees that safety properties proved on source code also hold for the compiled code.

Checked: PDF from xavierleroy.org, fetched 4 Oct 2026. Page numbers are those of that PDF.

14 findings

Substance The hypothesis 'Initial states: if initial(P1, S1) and initial(P2, S2), then S1 ∼ S2' does not say that P2 has an initial state, so Theorems 3 and 4 ('P1 ⇓ B and B ∉ Wrong imply P2 ⇓ B') do not follow as stated.

p. 16 Section 3.7, hypotheses and Theorem 3
Initial states: if initial(P1, S1) and initial(P2, S2), then S1 ∼ S2.
p. 15 Definition of P ⇓ B
initial(P, S)

Only the authors can say what is right here.

Judge's note: Checked p. 16 (hypotheses, Theorem 3 and its proof), p. 17 (Theorem 4), p. 15 (every ⇓ rule needs initial(P,S)) and Fig. 8 (initial requires symbol(globalenv(P), P.main) = ⌊b⌋, so initial states can fail to exist). My own reworking: let P2 have no initial state and let ∼ be empty. Then the initial-states, final-states and lock-step/star hypotheses all hold vacuously. P1 ⇓ converges(ε,0) can hold while P2 has no behavior at all. Both proofs implicitly start from a related initial S2. The repair is an existential hypothesis (for every initial S1 there is an initial S2 with S1 ∼ S2). The per-pass results are unaffected.

Second check: another model agreed

Report a problem with this finding

Substance The Fig. 8 Cminor tailcall rule ends in 'C(Fd, v⃗, callcont(k), M)' with M unchanged. The text says 'the tail call deallocates the current stack data block', and the RTL tailcall rule (Fig. 10) gives free(M, σ).

p. 24 Fig. 8, tailcall rule
ϵ→C(Fd,⃗v, callcont(k), M)
p. 20 Section 4.1, top of page
current stack data block before invoking the function. This enables tail recursion to
p. 19 Section 4.1
except that the tail call deallocates the
p. 31 Fig. 10, RTL tailcall rule
ϵ→C(Σ, Fd, R(⃗r), free(M, σ))

Judge's note: Checked p. 24 (Fig. 8: the tailcall conclusion keeps M, while the return rules use free(M,σ)), pp. 19-20 (text on deallocation and constant stack space) and p. 31 (the RTL tailcall uses free(M,σ)). The rule as printed contradicts the prose. The evident fix is free(M, σ).

Second check: another model agreed

Report a problem with this finding

Substance The smart-constructor rule 'rolm_{n1,m1}(rolm_{n2,m2}(a)) = rolm_{n1+n2,m}(a) with m = rol(m1, n2) ∧ m2' (p. 28) has its indices swapped. With rolm_{n,m}(x) = rol(x,n) ∧ m, the mask should be rol(m2,n1) ∧ m1. The p. 29 identity is correct, but only for the opposite nesting.

p. 28 Section 5.2, smart-constructor equations
with m = rol(m1, n2) ∧ m2
p. 29 Section 5.3, identity used in the proof
rol((rol(x, n1) ∧ m1), n2) ∧ m2 = rol(x, n1 + n2) ∧ (rol(m1, n2) ∧ m2)

Only the authors can say what is right here.

Judge's note: Definition from p. 26: rolm_{n,m} is a left rotation by n followed by 'and' with m. My own reworking: the inner y = rol(a,n2) ∧ m2, and the outer rol(y,n1) ∧ m1 = rol(a,n1+n2) ∧ rol(m2,n1) ∧ m1. The p. 29 identity rol((rol(x,n1) ∧ m1),n2) ∧ m2 = rol(x,n1+n2) ∧ (rol(m1,n2) ∧ m2) has (n1,m1) inside, so it does not match the p. 28 left-hand side. Counterexample I checked: n1=0, m1=0xFF, n2=8, m2=0xFFFFFFFF, a=0x01000000. The left side gives 1; the printed right side gives rol(a,8) ∧ 0xFF00 = 0. Lemma 2 survives once the indices are swapped.

Second check: another model agreed

Report a problem with this finding

Substance Sec. 8.3 characterization for calls reads "Φ(r′) ≠ rm for all r′ ∈ A(l) \ {rd} and all callee-save registers rm"; by the paper's own construction this should be caller-save registers.

p. 45 Section 8.3, third bullet
for all r′ ∈ A(l) \ {rd} and all callee-save registers rm.
p. 45 Section 8.3, characterization of Φ for call instructions
for all r′ ∈ A(l) \ {rd} and all callee-save registers rm
p. 43 Section 8.2.3
the registers live across the call and the caller-save machine registers
p. 42 Section 8.1, postcall
undef if ℓ is a temporary or caller-save register

Judge's note: On p.42, postcall(L) sets temporary and caller-save registers to undef, and the text says no value live across a call may be stored in a caller-save register. On p.43 (8.2.3), interference edges are added between registers live across the call and the caller-save machine registers. The p.45 characterization says callee-save. My own check: if r′ is live across the call and Φ(r′) is a caller-save register c, the printed condition holds. After the call L(c) = undef while R(r′) keeps its value, so R(r) = L(Φ(r)) fails. As printed, the property contradicts the construction and the semantics.

Second check: another model agreed

Report a problem with this finding

Substance Footnote 5 says "We reserve 2 integer and 3 float machine registers as temporaries to be used later for spilling and reloading", while section 11.2 says "We reserve 3 integer registers and 3 float registers to hold reloaded values and results of instructions before spilling".

p. 44 Footnote 5
We reserve 2 integer and 3 ﬂoat machine registers as temporaries
p. 51 Section 11.2
We reserve 3 in-teger registers and 3 ﬂoat registers to hold reloaded values
p. 51
We reserve 3 in-

Only the authors can say what is right here.

Judge's note: Page 44 footnote 5 and page 51 section 11.2 both describe the temporaries reserved for spilling and reloading, but give different integer counts (2 vs 3); both give 3 float registers. I searched the text for an explanation and found none. The ARM remark in the text layer (line 4180) concerns a reduced count for the ARM port, not PowerPC, so it does not reconcile the two. Only the authors can say which count is right.

Second check: another model agreed

Report a problem with this finding

Substance loadimm's general case "addis(r, R0, high(n)); ori(r, r, low(n))" does not rebuild n when low(n) < 0 under the stated signed decomposition "n = high(n) × 2^16 + low(n)".

p. 62 Section 14.1, definition of loadimm
addis(r, R0, high(n)); ori(r, r, low(n))
p. 62 Section 14.1
compute the signed 16-bit integers such that n = high(n) × 2^16 + low(n)

Only the authors can say what is right here.

Judge's note: Rests on outside knowledge: that PowerPC ori is a bitwise OR with a 16-bit (zero-extended) immediate. The p.62 image defines low/high as signed 16-bit integers with n = high×2^16 + low, and addimm uses addi for the low part. Take n = 0x18000 = 98304: high = 2 and low = −32768. addis gives 0x20000. OR-ing 0x8000 into that gives 0x28000 = 163840. With a sign-extended immediate the result is 0xFFFF8000. Neither equals n. With the signed parts the printed formula is wrong; it would need unsigned halves or addi. The authors should say which is intended.

Second check: another model agreed

Report a problem with this finding

Reference or label Section 6.4 opens "We now return to the question left open at the beginning of section 6.3", but the question (how to implement the translation in Coq without imperative updates) is raised at the beginning of section 6.2.

p. 35 Section 6.4, first sentence
We now return to the question left open at the beginning of section 6.3
p. 31 Section 6.2 (continued)
Section 6.4 describes a solution, based (unsurprisingly) on the use of a monad.

Judge's note: The text layer places the heading "6.2 Relational specification of the translation" on page 30. The paragraph continuing on page 31 ends with "implementing this translation in Coq is delicate ... Section 6.4 describes a solution". Section 6.3 (page 34) begins with the semantic-preservation outline and raises no such question. The pointer should read 6.2.

Second check: another model agreed

Report a problem with this finding

Reference or label The third rule of the constant-propagation invariant reads "C(Σ, v, M) ∼ C(Σ′, v, M)". It relates three-component return states but uses the call-state constructor C. It should be R(Σ, v, M) ∼ R(Σ′, v, M).

p. 39 Section 7.2.3, third invariant rule
C(Σ, v, M) ∼C(Σ′, v, M)

Judge's note: Page 39 image: the rule is printed with calligraphic C on both sides. Call states are C(Σ, Fd, v⃗, M) with four components (p. 30), and return states are R(Σ, v, M). The rule above it on the same page already covers call states with C(Σ, Fd, v⃗, M). Page 34 uses R(v, k, M) ∼ R(Σ, v, M) for the analogous case. As printed, the constructor is wrong and the fix is evident.

Second check: another model agreed

Report a problem with this finding

Wording CSE rewrites the instruction "as a move op(move, r, r′, l′) from r′ to r". Under the paper's convention op(move, rs, rd, l′), with source first, this term moves from r to r′, contradicting the prose. It should be op(move, r′, r, l′).

p. 41 Section 7.3.2
move op(move, r, r′, l′) from r′ to r

Judge's note: The convention is used consistently elsewhere. On page 40 (7.3.1), op(move, rs, rd, l′) records rd = rs. On page 44 (8.2.5) it is op(move, rs, rd, l′). On page 32, with γ(id)=r, op(move, r, rd, l2) puts the value into rd. The Coq excerpt on page 36 has Iop Omove (rd::nil) rv, argument list then destination. Here the result register is r and the reused value is in r′, so the arguments are swapped. The prose states the intended direction.

Second check: another model agreed

Report a problem with this finding

Wording Sec. 9.2 tunneling invariant concludes "S(Σ, F, σ, l, L, M) ∼ S(Σ, F′, σ, DF(l), L, M)" with unprimed Σ on the right, although the premise is Σ ∼ Σ′.

p. 46 Section 9.2, invariant rule
S(Σ, F, σ, l, L, M) ∼S(Σ, F ′, σ, DF (l), L, M)

Judge's note: The crop shows unprimed Σ in the tunneled state, so the premise Σ ∼ Σ′ goes unused. The other invariants (pp.39, 45, 49) put Σ′ on the right. This is a typographical slip in the rule.

Second check: another model agreed

Report a problem with this finding

Wording Fig. 13 LTLin goto rule has premise "findlabel(F, ltrue) = ⌊c′⌋" for conclusion goto(l).c → c′; the label should be l.

p. 48 Fig. 13, goto rule
findlabel(F, ltrue) = ⌊c′⌋

Judge's note: The p.48 image shows l_true in the premise of the goto(l) rule. l_true is not bound in that rule and is evidently copied from the cond rule below it.

Second check: another model agreed

Report a problem with this finding

Wording Fig. 14 Linear function-entry rule concludes "S(Σ, F.code, σ, F.code, L′, M′)"; the second component of a Linear state is the function F.

p. 51 Fig. 14, internal function entry rule
S(Σ, F.code, σ, F.code, L′, M′)

Judge's note: Linear regular states are S(Σ, F, σ, c, L, M) (p.50), and the other rules in Fig. 14 use F in that position. F.code in the function slot looks like a carry-over from the RTL rule.

Second check: another model agreed

Report a problem with this finding

Wording Fig. 14 Linear tailcall rule concludes "→ C(Σ, Fd, L′, M)" without free(M, σ), unlike the Linear return rule and the RTL tailcall rule.

p. 51 Fig. 14, tailcall rule
ϵ→C(Σ, Fd, L′, M)

Judge's note: The p.51 image shows M unchanged in the tailcall rule, while the return rule just below has free(M, σ). The RTL tailcall rule (text line ~1816) has C(Σ, Fd, R(r), free(M, σ)). The Mach tailcall rule in Fig. 15 also leaves M unchanged, but Mach has its own conventions. The Linear rule is inconsistent with its own return rule and with RTL.

Second check: another model agreed

Report a problem with this finding

Wording Section 14.2 says PPC generation "is proved using a simulation diagram of the “option” type" (p. 62), but the next page says "The simulation diagram is of the “star” kind" (p. 63).

p. 62 Section 14.2, first sentence
is proved using a simulation diagram of the “option” type.
p. 63 Section 14.2
The simulation diagram is of the “star” kind because Mach transitions
p. 62 Section 14.2, first sentence
using a simulation diagram of the “option” type
p. 63 Section 14.2
The simulation diagram is of the “star” kind

Judge's note: I read both pages and Definition 14 on p. 18. In the 'option' diagram, a source step is matched by exactly one target step, or by a stuttering step (none). Section 14.1 expands Mach instructions into sequences of PPC instructions (loadimm/addimm can emit two instructions; cond emits a compare, possibly cror, then bt/bf). Section 14.2 itself reasons with the derived →+ rule. So these cases cannot be matched by a single target step, and the 'option' diagram as defined does not apply. The p. 63 'star' description, with measure 1 for return states and 0 for other states, fits the proof sketch. Both 'plus' and 'option' imply 'star', so the theorem still holds. The p. 62 label is a misdescription of the proof method.

Second check: another model agreed

Report a problem with this finding

30 minor (typos and the like; most checked by the judge only)

Substance Fig. 19 gives "43.8%" as the Compcert geometric mean, but the 17 Compcert percentages printed above it give about 43.6%. The gcc -O1 (40.8%) and -O2 (38.9%) means do reproduce from their columns.

p. 67 Fig. 19, Geometric mean row, Compcert column
43.8%
p. 68 Section 16.2
only 7% slower than gcc -O1 and 12% slower than gcc -O2
p. 68 §16.2, second paragraph
On average, Compcert code is only 7% slower than gcc -O1 and 12% slower than gcc -O2

Only the authors can say what is right here.

Judge's note: I read all cells from the p. 67 image. My sum of ln values for the Compcert column is 64.158; divided by 17 that is 3.7740, and exp gives 43.56%. The same method on the -O1 column gives exp(63.059/17) = 40.83%, which matches the printed 40.8%. Rounding each cell to 0.1% cannot move the geometric mean by 0.25 points. With 43.8 against 38.9 the ratio is 1.126, about 13%, while the text on p. 68 says 12%; the recomputed 43.56/38.88 gives 1.120. Only the authors can say whether the mean or one of the cells is mistyped.

Second check: another model agreed

Report a problem with this finding

Wording Equation label (i) is used for both 'Comp(S) = OK(C) ⟹ S ≈ C' (Def. 8, p. 6) and '∀S,C,B ∉ Wrong, Comp(S) = OK(C) ∧ S ⇓ B ⟹ C ⇓ B' (Sec. 2.4, p. 9). The later 'provided the proof of (i)' (p. 10) can therefore point to either.

p. 6 Definition 8
Comp(S) = OK(C) =⇒S ≈C
p. 9 Section 2.4, item 1
Comp(S) = OK(C) ∧S ⇓B =⇒C ⇓B
p. 10 Section 2.4, item 4
provided the proof of (i) is carried out
p. 9 Sec. 2.4 item 1
Comp(S) = OK(C) ∧S ⇓B =⇒C ⇓B (i)

Judge's note: Seen on pp. 6, 9 and 10. The labels go (i) on p. 6, (ii) for Def. 9, then (i) again on p. 9. The 2.4 formula is an instance of Def. 8, so the ambiguity is mild.

Second check: another model agreed

Report a problem with this finding

Wording RTL call-stack grammar gives frames as "Σ ::= (F(r, F, σ, l, R))∗" (function F), but Fig. 10 builds and pops frames "F(r, g, σ, l′, R)" holding the CFG g; Lemma 5 likewise writes regular states S(Σ, F, σ, l1, R, M) where the grammar has g.

p. 30 Section 6.1, call stack grammar
Σ ::= (F(r, F, σ, l, R))∗
p. 31 Fig. 10, call rule
C(F(r, g, σ, l′, R).Σ, Fd, R(⃗r), M)

Judge's note: Page 30: the grammar has F in the second slot of frames, and the prose says frames contain the "per-function state F, σ, l, R". Page 31, Fig. 10: the call and return rules use F(r, g, σ, l′, R) and F(r, g, σ, l, R). Page 34: Lemma 5 writes S(Σ, F, σ, l1, R, M) although the grammar defines S(Σ, g, σ, l, R, M). The notation is inconsistent, but g is derivable from F (F.code), so the meaning can be recovered.

Second check: another model agreed

Report a problem with this finding

Wording Section 8.2 says "register allocation is performed in four steps, which we now outline", but five numbered subsections follow: 8.2.1 type reconstruction, 8.2.2 liveness analysis, 8.2.3 interference graph, 8.2.4 coloring, 8.2.5 LTL generation.

p. 42 Section 8.2 opening sentence
register allocation is performed in four steps
p. 44 Section 8.2.5
8.2.5 LTL generation

Judge's note: Page 42 shows 'four steps'. Pages 42–44 show five subsections, and 8.2.5 opens 'Finally, the actual code transformation...', which presents it as a further step. Nothing says two of them count as one. It is a count mismatch, though one could argue type reconstruction or LTL generation is not an 'allocation' step.

Second check: another model agreed

Report a problem with this finding

Wording Sec. 11.1: "exitfun(L, L′) determines the locations in the callee when the call returns"; the result is the caller's location state after return.

p. 50 Section 11.1
exitfun(L, L′) determines the locations in the callee when the call returns

Judge's note: The table on p.50 builds exitfun from the caller's L (callee-save registers, local and incoming slots) and the callee's L′. In Fig. 14 (p.51) the resulting L′ is carried by the R state into the caller's frame. 'in the callee' misdescribes this and should read 'in the caller'. It is a wording issue only.

Second check: another model agreed

Report a problem with this finding

Wording Frame-offset conventions do not cohere as printed: Δ offsets "are negative" (p.55), the Mach stack pointer is "σ = ptr(b, F.stack low)" with loadstack reading at δ′+δ (Fig. 15), and the frame invariant indexes Φ by absolute block offset n with L(M′,b) = F.stack_low (p.58).

p. 55 Fig. 15, loadstack and function-entry rule
σ = ptr(b, F.stack low)
p. 55 Section 12.2
(Note that these offsets are negative
p. 58 Section 12.3, frame invariant
load(κ(τ), M′, b, n) = ⌊Φ(τ, n)⌋

Only the authors can say what is right here.

Judge's note: I reworked this from the printed definitions. Loadstack reads at stack_low + Δ. If Δ is negative as p.55 states, that address lies below the block's low bound L(M′,b) = stack_low. Example: stack_low = −16, Δ = −8 gives address −24 < −16. The invariant on p.58 only describes offsets from stack_low to 0. The text does not say how the alternate semantics indexes Φ for getstack, so I cannot tell which convention is meant. The printed definitions are mutually inconsistent and only the authors can say which convention the Coq development uses. Lemma 10 is presumably unaffected there.

Second check: another model agreed

Report a problem with this finding

Wording "The remaining 86% comprise 10% of specifications ..., 21% of statements ..., 44% of proof scripts and 8% of directives". These parts sum to 83%; the 3% Code (in Caml) column of Fig. 18 is left out.

p. 65 Section 15.3
The remaining 86% comprise 10% of speciﬁcations
p. 65 Fig. 18, Total row percentages
14% 3% 10% 21% 44% 8%

Judge's note: I checked the Total row of Fig. 18 on p. 65: 14% 3% 10% 21% 44% 8%. 100-14 = 86 includes the 3% Caml code, but the listed parts add up to only 83. The sentence is about the Coq verification, so leaving out Caml may be intentional, but then the stated 86% does not match.

Second check: another model agreed

Report a problem with this finding

Wording "Among the 37500 lines of the initial development, 28000 (76%) were found to be processor-independent and 8900 (24%) ended up in PowerPC-specific modules". 28000+8900 = 36900, not 37500, and the percentages use 36900 as the base.

p. 70 Section 17.2, end
Among the 37500 lines of the initial development, 28000 (76%) were found to be processor-independent and 8900 (24%)
p. 70 Section 17.2, last paragraph
Among the 37500 lines of the initial development, 28000 (76%) were found to be processor-independent and 8900 (24%) ended up in PowerPC-specific modules
p. 70 Section 17.2 On retargeting, first paragraph
28000 (76%) were found to be processor-independent and 8900 (24%)

Only the authors can say what is right here.

Judge's note: I checked p. 70. The two parts sum to 36900, which leaves 600 lines unaccounted for. 28000/36900 = 75.9%, which matches the printed 76%, whereas 28000/37500 = 74.7%. Lines removed during the restructuring could explain the gap, but the text does not say so. Only the authors can say which figure is intended.

Second check: another model agreed

Report a problem with this finding

Typo 'return update memory state M′' should read 'return the updated memory state M′'.

p. 11 Section 3.2, store operation
return update memory state M′

Judge's note: Seen in the crop on p. 11. The parallel alloc and free bullets both say 'the updated memory state'.

Second check: none (judge only)

Report a problem with this finding

Typo In the remark after Definition 12, 'or |S′1| < |S1| and t = ϵ and S2 ∼ S′1' reverses the arguments of ∼. It should read S′1 ∼ S2.

p. 17 Below Definition 12
and S2 ∼S′1”

Judge's note: Seen on p. 17. Everywhere else ∼ relates an L1 state on the left to an L2 state on the right, and Definition 12 itself writes S′1 ∼ S′2.

Second check: none (judge only)

Report a problem with this finding

Typo 'CompCert compilation chain' (p. 18) is the only place the name is written CompCert. Everywhere else it is 'Compcert'.

p. 18 Section 4
CompCert compilation chain

Judge's note: Seen in the crop on p. 18. The text layer has 1 'CompCert' against 64 'Compcert'.

Second check: none (judge only)

Report a problem with this finding

Typo The text says 'Note the explicit address computation int32[tbl + i*4]', but the Fig. 5 Cminor code has int32[arr + i*4]; no variable tbl exists in the example.

p. 20 Section 4.1, paragraph on Figure 5
int32[tbl + i*4] to access element i of the array
p. 20 Fig. 5, Cminor code
floatofint(int32[arr + i*4])
p. 20 paragraph on Figure 5
int32[tbl + i*4]
p. 20 Fig. 5 Cminor code
int32[arr + i*4]

Judge's note: Checked on p. 20. The array parameter is arr in both the C and the Cminor code. tbl is the switch-table metavariable.

Second check: none (judge only)

Report a problem with this finding

Typo Fig. 8 has 'alloc(M, 0, F.stackspace)', but the Cminor field is named stacksize ('A fresh memory block of size F.stacksize').

p. 24 Fig. 8, internal function call rule
alloc(M, 0, F.stackspace) = (σ, M′)
p. 24 Fig. 8, function entry rule
alloc(M, 0, F.stackspace)
p. 20 Sec. 4.1 syntax and text
A fresh memory block of size F.stacksize

Judge's note: Seen on p. 24 and p. 20. The text layer shows stackspace only in Fig. 8. The RTL and later rules use F.stacksize.

Second check: none (judge only)

Report a problem with this finding

Typo The Fig. 6 empty-list rule 'G, σ, E, M ⊢ ϵ : ϵ' uses ':' where the list judgment uses '⇒' (it should be ⊢ ϵ ⇒ ϵ).

p. 21 Fig. 6, empty list rule
G, σ, E, M ⊢ϵ : ϵ

Judge's note: Seen on p. 21. The companion cons rule uses G, σ, E, M ⊢ a⃗ ⇒ v⃗.

Second check: none (judge only)

Report a problem with this finding

Typo The Fig. 7 store rule writes '(κ[a1] = [a2])', with stray brackets around a2. The syntax is κ[a1] = a2.

p. 23 Fig. 7, store rule
(κ[a1] = [a2])

Judge's note: Seen in the crop of p. 23. The p. 19 syntax reads κ[a1] = a2.

Second check: none (judge only)

Report a problem with this finding

Typo In Lemma 2 item 5, 'mode(a) = (mode, a⃗). then there exists' has a full stop where a comma belongs.

p. 28 Lemma 2, item 5
mode(a) = (mode,⃗a). then there exists

Judge's note: Seen on p. 28.

Second check: none (judge only)

Report a problem with this finding

Typo 'algebraic properties of rotate-and-left and bitwise “and”' should read 'rotate-left'.

p. 29 Section 5.3
algebraic properties of rotate-and-left and bitwise “and”

Judge's note: Seen on p. 29. The operation is rol (rotate left).

Second check: none (judge only)

Report a problem with this finding

Typo The expression sub-graph is said to have "a start node l1 and an end node le", but the predicate defined next uses "l1, l2 the start and end nodes in the CFG", and le later denotes the list of exit nodes for statements.

p. 32 Section 6.2 paragraph
an end node le
p. 32 same section, predicate definition
l1, l2 the start and end nodes in the CFG

Judge's note: Page 32: the paragraph uses l_e for the end node of an expression sub-graph. The next paragraph and all expression rules use l2. On page 33, l_e is 'a list of nodes' for statement exits. This is a notation clash, and the meaning is clear from context.

Second check: none (judge only)

Report a problem with this finding

Typo The monad operation is listed as "newreg : mon(reg)" in the prose (p. 35) but appears as "do rd <- new_reg;" in the Coq excerpt (p. 36). The other operations (add_instr, reserve_instr, update_instr) keep the same spelling in both places.

p. 35 Section 6.4, list of monad operations
newreg : mon(reg) generates a fresh temporary register
p. 36 Coq excerpt
do rd <- new_reg;

Judge's note: Both images confirm the two spellings. This is a cosmetic naming inconsistency.

Second check: none (judge only)

Report a problem with this finding

p. 39 Section 7.2.3
Agreement between a concrete and an abstract value is written |= a : v

Judge's note: Page 39 image confirms that the prose order is the reverse of the order in the rules directly below it and in all later uses. The meaning is recoverable from the rules.

Second check: none (judge only)

Report a problem with this finding

Typo The statement of Lemma 7 ends "S′1 ∼ S′2," with a trailing comma instead of a full stop.

p. 40 Lemma 7
S′1 ∼S′2,

Judge's note: Page 40 image: the lemma text ends with a comma, followed by the section break.

Second check: none (judge only)

Report a problem with this finding

Typo CSE satisfaction condition 3 writes "eval_addressing(mode, V(x⃗)) = ⌊ptr(b, δ)⌋ and load(κ, M, b, δ) = ⌊V(x)⌋". The function is called eval_mode(G, σ, mode, …) elsewhere (Figs. 9–10), and load is defined as load(M, κ, b, δ) in section 3.2.

p. 41 Section 7.3.1, item 3
eval addressing(mode, V (⃗x)) = ⌊ptr(b, δ)⌋and load(κ, M, b, δ)

Judge's note: Page 41 image confirms eval_addressing and load(κ, M, …). The text layer shows load(M, κ, b, δ) in section 3.2 and Fig. 10, but load(κ, M, …) also recurs in later sections (lines 2974, 3241 of the text), so the paper switches argument order in several places. eval_addressing is introduced nowhere else. This is a naming and ordering inconsistency only.

Second check: none (judge only)

Report a problem with this finding

Typo Sec. 8.2.4 item 1 prints "Φ(r) ≠ rm for all interference edges (r, m)"; the machine-register edges are written (r, rm) in 8.2.3.

p. 44 Section 8.2.4, item 1
Φ(r)̸ = rm for all interference edges (r, m).

Judge's note: I checked the crop: the edge reads (r, m), but 8.2.3 (p.43) writes the ordered pairs as (r, r_m). This is a notational slip and the meaning is clear.

Second check: none (judge only)

Report a problem with this finding

Typo Measure definition "|S(Σ, F, sp, l, L, M)| = #nopF(l)" writes the stack pointer as sp instead of σ.

p. 46 Section 9.2
|S(Σ, F, sp, l, L, M)| = #nopF (l)

Judge's note: The crop confirms 'sp'. This is the only occurrence of sp in the text layer; every other state uses σ. Cosmetic.

Second check: none (judge only)

Report a problem with this finding

Typo Sec. 12.2 says "getslot and setslot Linear instructions are rewritten as follows", but the Linear syntax (Sec. 11.1, p.50) names them getstack(s, r) / setstack(r, s).

p. 49 Section 11.1
Two instructions getstack and setstack are provided to move data between machine registers and stack slots s.
p. 56 Section 12.2
getslot and setslot Linear in-structions are rewritten as follows
p. 56 Section 12.2 translation equations
getslot and setslot Linear in-
p. 50 Section 11.1 Linear syntax
getstack(s, r) | setstack(r, s)

Judge's note: The Linear grammar on p.50 and the text on pp.49 and 51 use getstack/setstack. The rewrite rules on p.56 use getslot/setslot on the Linear side and getstack/setstack (with different arguments) on the Mach side. This is a naming inconsistency and the intent is clear.

Second check: none (judge only)

Report a problem with this finding

Typo Stack invariant on p.53 writes the Linear frame as "F([[F]], σ, L′, c′)", whereas Linear frames are defined as F(F, σ, c, L).

p. 53 Section 11.3, stack invariant
F([[F]], σ, L′, c′).Σ′ : sig

Judge's note: p.50 defines Σ ::= (F(F, σ, c, L))*, and Fig. 14 uses F(F, σ, c, L). On p.53 the components are swapped (L′, c′). The LTLin frame on the left is also written F(ℓ, F, σ, postcall(L), c). Notational only.

Second check: none (judge only)

Report a problem with this finding

Typo p.57: "Leroy and Blazy [59, section 5.2] study the properties of this relation between memory states and shows that it commutes"; 'shows' should be 'show'.

p. 57 Section 12.3, end
study the properties of this relation between memory states and shows
p. 57 end of Section 12.3
Leroy and Blazy [59, section 5.2] study the properties of this relation between memory states and shows that it commutes

Judge's note: The p.57 image confirms the plural subject with 'study ... and shows'. This is a subject–verb agreement slip.

Second check: none (judge only)

Report a problem with this finding

Typo Section 14.1 lists "cmplw, cmplwi, cmpw, cmpwi or fcmp", but the PowerPC subset in Fig. 17 contains only "fcmpu" as a float compare.

p. 62 Section 14.1
cmplw, cmplwi, cmpw, cmpwi or fcmp
p. 59 Fig. 17
fcmpu

Judge's note: I checked Fig. 17 on p. 59. Its instruction list includes fcmpu and no fcmp. The other compare mnemonics named on p. 62 are spelled exactly as in Fig. 17, so 'fcmp' appears to be a slip for 'fcmpu'.

Second check: none (judge only)

Report a problem with this finding

Typo Memory sizes are given as "4 Gb of RAM" (p. 66) and "6 Gb of RAM" (p. 68). The unit symbol Gb means gigabits; gigabytes (GB) are meant.

p. 66 §15.3, last paragraph
equipped with 4 Gb of RAM
p. 68 §16.2, first paragraph
6 Gb of RAM

Judge's note: I checked both page images and the text reads 'Gb' in both places. The meaning is clear from context and this is common informal usage, so it is cosmetic.

Second check: none (judge only)

Report a problem with this finding

Typo "weakly typed in a int-or-float type system": the article should be "an".

p. 72 §17.5, fourth paragraph
weakly typed in a int-or-float type system

Judge's note: The p. 72 image shows 'a int-or-float'. 'int' begins with a vowel sound, so the article should be 'an'.

Second check: none (judge only)

Report a problem with this finding

Something wrong with this page, or a finding we missed?