Proof-Carrying Code

• p. 5 Figure 5, lines 1, 13 and 14

  MOV r_1, 0

• p. 6 Figure 6

  if Π_i = INV I

Only the authors can say what is right here.

Judge's note: Checked on the page images. Figure 5 (p.5) uses MOV at lines 1 and 14 and BR at line 13. Figure 6 (p.6) and Figure 8 (p.12) have no cases for MOV or BR. Page 12 says the machine halts 'when ... invalid instructions are encountered'. The text never says that MOV and BR are pseudo-instructions that expand to supported forms. The figures also name the same instructions differently (ADD/LD in Fig. 6, ADDQ/LDQ in Fig. 8). This is a gap in the presentation only the authors can resolve, not an evident typo.

Second check: another model agreed

• p. 8 Quantitative Results, first paragraph

  less the precondition, which is supplied by the code producer

• p. 5 Computing the Verification Condition

  the code consumer prepends the instruction INV Pre to each untrusted program

• p. 8

  which is supplied by the code producer

Only the authors can say what is right here.

Judge's note: Page 2 image: the safety policy, including the interface (the invariants holding when the consumer invokes the foreign code), 'is defined and made public by the code consumer'. Page 5 image: 'the code consumer prepends the instruction INV Pre to each untrusted program'. Page 8 image says the precondition is 'supplied by the code producer'. It is also unclear why the precondition would be left out of the proof if the producer supplied it. 'Consumer' was probably meant; only the authors can confirm.

Second check: another model agreed

• p. 6 Definition of VC(Π, Inv, Post)

  VC(Π, Inv, Post) = ∀r_i. ⋀_{i∈Inv} Inv_i ⊃ VC_{i+1}

Judge's note: Confirmed in the page 6 image. The intended meaning (quantify over all registers) can be inferred, but as printed the same letter serves as two bound indices. This is a notational ambiguity, not an error in the result.

Second check: another model agreed

• p. 12 Appendix A, proof of Lemma A.1, Case ADD

  From hypothesis ▷ ρ([r_s + n/r_d] VC_{pc+1})

• p. 6 Figure 6, ADD case

  [r_s + op/r_d] VC_{i+1}

• p. 12 Proof of Lemma A.1, Case ADD

  ▷ ρ([r_s + n/r_d] VC_{pc+1})

• p. 12 Lemma A.1 proof, ADD case

  ADD r_s, op, r_d. From hypothesis ▷ ρ([r_s + n/r_d] VC_{pc+1})

Only the authors can say what is right here.

Judge's note: The p12 image shows the case header with op and the body with n. Figure 6 (p6) and Figure 8 (p12) both use r_s + op. n is not bound in this case (it is the LD/BEQ offset). The argument goes through once n is read as op, so this is a symbol slip and the result stands.

Second check: another model agreed

• p. 8 Section 3, paragraph after Corollary 3.3

  normalization is only involved in checking instances of the universal quantification elimination rule schema

• p. 7 Signature constant all_i

  (Πv:exp.pf (p v)) → pf (all p)

Only the authors can say what is right here.

Judge's note: My own working from the page 7 and page 14 images. all_i : Πp:exp→pred.(Πv:exp.pf (p v)) → pf (all p). Applying all_i to N = λx:exp.⌜P_x⌝ uses at_app, whose premise [N/p]B ⇓ B′ must normalize pf ((λx:exp.⌜P_x⌝) v). That is a β-redex, so nm_beta is needed. By contrast, and_i and impl_i instantiate p:pred with non-lambda terms, so they create no redex. The literal 'only elimination' claim therefore does not match the signature as printed. The soundness and adequacy results are unaffected.

Second check: another model agreed

• p. 8 Corollary 3.3

  M :_LF pf ⌜P⌝

• p. 14 Corollary B.5

  M :_c pf ⌜P⌝

• p. 8 Corollary 3.3

  · ⊢_L M :_LF pf ⌜P⌝

• p. 14 Corollary B.5

  · ⊢_L M :_c pf ⌜P⌝

Only the authors can say what is right here.

Judge's note: Page 8 image: Corollary 3.3 has ':_LF'. Page 14 image: Corollary B.5 has ':_c'. Both are introduced as the corollary of the adequacy theorem, and Theorems 3.2 and B.4 are stated with ':_c'. To get the :_LF version from those theorems, a reader would need a completeness result (canonical and LF-typable implies LF0 :_c-typable), and the paper does not state one. The intended statement is probably the :_c form, but only the authors can confirm.

Second check: another model agreed

• p. 5 Section 3, Computing the Verification Condition, right column top

  the foreign code is accompanied contains a valid proof of it

• p. 5 right column, first paragraph

  the code consumer to ensure that the foreign code is accompanied contains a valid proof of it.

Judge's note: Visible in the page 5 image, right column, first paragraph. The sentence combines 'is accompanied by' and 'contains'.

Second check: none (judge only)

• p. 6 Section 3, paragraph after first conjunct

  says both that the the loop invariant is pre-

• p. 6

  both that the the loop invariant is preserved

Judge's note: Visible in the page 6 image, left column, in the paragraph after the displayed conjunct. Both copies of 'the' are on the same line.

Second check: none (judge only)

• p. 12 Figure 8

  if Π_pc = ADDQ r_s, op, r_d

• p. 6 Figure 6

  if Π_i = ADD r_s, op, r_d

• p. 12 Figure 8, abstract machine rules

  ADDQ r_s, op, r_d

• p. 6 Figure 6, VC generator

  ADD r_s, op, r_d

Judge's note: Checked on the images: Fig. 8 (p12) uses ADDQ/LDQ, while Fig. 6 (p6) and the proof cases (p12) use ADD/LD. These are the real Alpha mnemonics and the meaning is clear, so this is a minor naming inconsistency.

Second check: none (judge only)

• p. 8 Corollary 3.3

  there exists a derivation of D :: ▷ P

• p. 14 Corollary B.5 (same statement)

  there exists a derivation D :: ▷ P

Judge's note: Confirmed on the page 8 and page 14 images. D is the derivation itself, so 'of' is a stray word.

Second check: none (judge only)

• p. 10 Section 7 Conclusion, first paragraph

  or proof in an PCC binary

• p. 10 Section 7 Conclusion, first paragraph

  either the native code or proof in an PCC binary

• p. 10

  in an PCC binary

Judge's note: The p10 image, right column, Conclusion paragraph 1, clearly prints 'in an PCC binary'. Elsewhere the paper uses 'a PCC binary'.

Second check: none (judge only)

• p. 10 Section 7 Conclusion, third paragraph

  be done only once independently how many times the

Judge's note: The p10 image, right column, Conclusion paragraph 3, shows the text as quoted, without 'of'.

Second check: none (judge only)

• p. 12 Appendix A, paragraph before Lemma A.1

  in a state the satisfies the postcondition

Judge's note: The p12 image, right column, paragraph 'The central result...', prints 'a state the satisfies'.

Second check: none (judge only)