Polish a bit

compcertoe/popl25/popl2025-response-239.mdwn

@@ -1,131 +1,116 @@
-We are grateful for the reviewers' hard work and valuable feedback.
+We are grateful for the reviewers' valuable feedback.
 Since cross-cutting concerns include the motivation and framing of our contributions,
 the relationship of our work to other relevant research, and the status of our
-implementation, we will discuss these issues first. We then include a proposed
-revision plan for the paper and provide responses to reviewers' individual concerns.
+implementation, we will discuss these points first. We then include a proposed
+revision plan for the paper and provide point-by-point responses
+to some of the reviewers' individual concerns.
 
 ## I. Motivation and Novelty
 
-Our long-term goal is to facilitate
+Our goal is to facilitate
 the construction of large-scale certified systems.
-In the same way a present-day system administrator
-would set up an infrastructure by
-selecting a combination of existing hardware and software components
-and configuring them to work together,
-we envision a situation where
+Present-day system administrators
+set up infrastructures by
+selecting combinations of hardware and software components,
+and configuring them to work together.
+We envision a situation where
 future certified systems architects
-would build complex systems
+would similarly build complex systems
 by assembling off-the-shelf certified components,
-and would be able to obtain end-to-end proofs of correctness
+and obtain end-to-end proofs of correctness
 for very large systems
 with little additional effort.
 
-Figuring out whether and how this vision can be realized
-will require research in several directions,
-including (i) improving the range of proof automation techniques
+Among other things, realizing this vision
+will require (i) improving the range of proof automation techniques
 and streamlining the experience of verification engineers
-(as suggested in Review #239C)
+(per Review #239C)
 as well as (ii)
-conducting more integration verification case studies
-(like those referenced by Review #239A).
-Simultaneously,
+conducting more integration verification case studies (#239A).
+In addition,
 we must (iii) draw from these experiences
-to develop a systematic understanding
+to deepen our understanding
 of the principles underlying these successes,
-and distill them into new mathematical tools
+and distill them into new mathematical tools,
 which can then serve as a foundation for
 the next round of ground-breaking challenges and research.
-Although our **§6 Applications** section illustrates
-concrete verification tasks carried out using our framework,
+Although §6 outlines verification tasks carried out using our framework,
 we would consider that our work and claim to novelty
-falls squarely under (iii).
+largely falls under (iii).
 
 **Illustration with integration verification.**
 The Bedrock2 case studies mentioned by Review #239A
 can be used to illustrate this point.
 Erbsen et al. [PLDI '24] presents the end-to-end verification of
 a minimalistic but sophisticated embedded system,
 which mediates access to an external actuator
-(in their demonstration, the opening mechanism for
-a miniature replica of a garage door)
-through cryptographically authenticated network commands.
+(the opening mechanism for
+a miniature garage door replica)
+through cryptographically-authenticated network commands.
 The top-level correctness statement takes the form:
-$$
-\mathtt{always\:\:run1\:\:(eventually\:\:run1\:\:}
+$$\mathtt{always\:\:run1\:\:(eventually\:\:run1\:\:}
 (q \mapsto \mathtt{io\_spec}\:\:q.\mathtt{getLog}))
-\:\:q_0\,,\quad(1)
-$$
+\:\:q_0\,,\quad(1)$$
 where
-`run1` models one execution step of the low-level RISC-V system being verified,
-$q_0$ is the initial state of the system,
-`getLog` extracts from the state
+`run1` models one execution step of the system being verified,
+$q_0$ is its initial state,
+`getLog` extracts from states
 the accumulated record of external interactions,
 which must satisfy the predicate `io_spec`.
-An equivalent formulation within our framework may look something like:
-$$
-\mathtt{io\_spec}\:\le_{R \twoheadrightarrow S}\:
-[q_0\rangle \odot (\cdots \mathtt{run1} \cdots)\,,
-\quad(2)
-$$
+An equivalent formulation within our framework may look like:
+$$\mathtt{io\_spec}\:\le_{R \twoheadrightarrow S}\:
+[q_0\rangle \odot (\cdots \mathtt{run1} \cdots)\,,\quad(2)$$
 where $\mathtt{io\_spec}:\mathcal{A}\twoheadrightarrow\mathcal{N}$
 specifies which actuator commands ($\mathcal{A}$)
-should result from given network interactions ($\mathcal{N}$),
-where the right-hand side of $\le$ models the implemented system,
-and where $R$ and $S$ can be used to spell out any abstraction relationships
-between this implementation and the high-level `io_spec`.
+should result from given network interactions ($\mathcal{N}$);
+where the right-hand side of $\le$ models the implemented system;
+and where $R$ and $S$ spell out any abstraction relationships
+between this implementation and the high-level $\mathtt{io\_spec}$.
 
 Logically,
-the formulations (1) and (2) are quite close.
-Both use external interaction traces
-to specify the system's observable behavior,
-and it may in fact be relatively straightforward
-to establish something like (2)
+the formulations (1) and (2) are quite close,
+and it should be straightforward
+to establish (2)
 from the property (1) proven in the existing development.
 At the same time,
-reformulating the correctness property in this ``standard refinement'' form
+the "standard refinement" reformulation
 presents some advantages:
 
   * First, our composition principles would be immediately available
-    to someone who were trying to *prove* the property again, and they may
-    lessen the need to use other kinds of compositional techniques.
-    As we understand it, the Bedrock proof relies on forms of separating
+    to someone who were trying to *prove* the property again.
+    The Bedrock proof relies on forms of separating
     conjunction and data abstraction, which in a different version
     could conceivably fall under our spatial and vertical composition infrastructure.
     This approach may also make it easier to reuse the CompCertO correctness
     theorem, CAL methodology, ... as needed.
-  * More to the point (since the proof already exists),
+  * More interestingly,
     consider a *user* of this certified network actuator, seeking
-    to use it as a component within (say) a larger certified industrial control
-    network.
-    At first, they will want to reason about the correctness of their overall
-    network in terms of `io_spec` alone, and they should not be forced to deal with
-    the implementation details spelled out in `run1` and $q_0$.
+    to use it as a component within a larger certified industrial control network.
+    They will want to reason about the correctness of their
+    network in terms of $\mathtt{io\_spec}$ alone, and should not be forced to deal with
+    the implementation details in $\mathtt{run1}$ and $q_0$.
     At a later stage, they may choose
-    among several competing vendors for certified `io_spec` implementations,
+    among several competing vendors for certified $\mathtt{io\_spec}$ implementations,
     and would simply be able to "plug" the refinement (2) provided by the
-    selected vendor within their own proof, replacing `io_spec` by their chosen
+    vendor within their own proof, replacing $\mathtt{io\_spec}$ by their chosen
     implementation in a correctness-preserving manner.
 
-This mirrors what happens in our paper with Fig 1 / Example 1.1 / §6.3,
+This mirrors our paper's Example 1.1,
 where correctness results obtained for individual programs
-can be reused and made part of a "next-scale" system of interacting processes,
-where the details of their internal semantics and execution can be encapsulated
-and abstracted away when we reason about their coarse-grained interaction patterns.
+can be reused and made part of a "next-scale" system of interacting processes.
+The details of their internal semantics and execution are encapsulated
+and abstracted away as we reason about their coarse-grained interaction patterns.
 
-In summary,
+**In summary,**
 our goal is not to supplant or out-do
 any prior verification effort or technique.
 As noted in Reviews #239A and #239C, and alluded to on ll. 93--117,
 our main example could be tackled using existing techniques,
 and we intend it primarily for illustration purposes.
-It is also true that extending the framework to support concurrency
-would significantly increase its power and
-will be necessary to tackle many complex systems.
-However,
-by consolidating a broad range of existing
+But by consolidating a broad range of existing
 verification techniques, tools and results
-under the scope of a single semantic model
-where they can be made open-ended and interoperable,
+under the scope of a single semantic model,
+where they can be made interoperable,
 we claim our work represents strong contribution towards
 a state-of-the-art where
 the verification of even larger-scale
@@ -138,17 +123,17 @@ and several existing approaches, we briefly discuss below some
 of work mentioned by the reviews.
 
 **Interaction Trees.**
-As a "semantic tool" of sorts,
+As a "semantics toolbox" of sorts,
 interaction trees share some goals and techniques with our model.
 In fact, an interaction tree `t : itree E X` can be intepreted
 into our framework as
 a strategy $\langle t \rangle : E \twoheadrightarrow \{* : X\}$.
 However, strategies generalize ITrees in several ways:
 
   * Strategies are two-sided and encode incoming as well as outgoing
-    interactions, forming the base for horizontal composition
-  * By design, ITrees must be executable programs, whereas strategies can be
-    described logically using more declarative and arbitrary Coq specifications.
+    interactions, forming the basis for horizontal composition
+  * By design, ITrees must be executable programs, whereas strategies
+    can be described logically using arbitrary Coq specifications.
   * Strategies which exhibit the same external behavior are formally *equal*.
     By contrast, ITrees are compared using *bisimlation equivalences*.
     Equational reasoning requires Coq's setoid support, which can be slower and
@@ -166,23 +151,18 @@ for which to our knowledge there exists no precedent in the game semantics liter
 In particular,
 refinement conventions involve alternations of angelic and demonic choices;
 we were surprised to find they can be modeled using a fairly standard approach,
-though a rather unconventional ordering of plays must be used accordingly.
+though a rather unconventional ordering of plays must be used.
 An interesting question for further research would be to investigate
 how far this can be pushed and whether games more complex than effect signatures
 could admit their own forms of refinement conventions.
 
 **Refinement Calculus.**
 Review #239B further mentions the refinement calculus as another point of comparison,
-and indeed it was a major source of inspiration for our framework.
+and indeed it was a source of inspiration for our framework.
 One defining feature of the refinement calculus is dual nondeterminism,
 which provides very powerful abstraction mechanisms.
-At the same time, models like predicate transformers cannot deal with
-external interactions or state encapsulation in the way we want,
-and while there have been attempts to incorporate dual nondeterminism into game semantics,
-we have found that arbitrary alternations of angelic and demonic choices
-introduce a high degree of complexity that is difficult to deal with in our context.
-This complexity can be avoided by performing data abstraction in a more controlled way
-in the form of refinement conventions.
+At the same time, models like predicate transformers do not deal with
+external interactions or state encapsulation.
 
 **CompCertO.**
 Finally it is worth pointing out the ways in which our framework
@@ -232,7 +212,7 @@ in the embedding $\bigvee_w [R]_w$ of a simulation convention $R$.
 We can then use proof principles such as:
 $$(\forall w\cdot\sigma\le_{R \twoheadrightarrow S_w}\tau)\Rightarrow
 \sigma\le_{R \twoheadrightarrow\bigvee_w S_w}\tau$$
-to help us reduce our proof obligations to consider
+to allow our proof to consider
 only a single world at a time.
 
 ## IV. Proposed edits and plan
@@ -241,19 +221,15 @@ We would be happy to incorporate these clarifications
 and revise our paper based on the reviewers' feedback.
 In particular, we will
 
-  * In the introduction,
-    clarify our contributions and the novel aspects of our work
-    following the discussion under §I above.
-    We will also strive to give a more comprehensive account of
-    existing verification work combining multiple languages,
-    compilation and external interactions, including Bedrock2
-    integration verification projects.
-  * More generally, we will strive to cover a broader range of
+  * In the Introduction section,
+    better frame our contributions and the novel aspects of our work
+    along the lines discussed under §I above.
+  * We will cover a broader range of
     Related Work, including but not limited to the comparisons
     we have outlined outlined under §II.
   * We will augment §6 with a qualitative and quantitative discussion and
-    evalulation of our implementation (§III)
-  * We will use the reviewers' excellent suggestions to improve the
+    evalulation of our Coq implementation (§III)
+  * We will use the reviewers' suggestions to improve the
     presentation, and generally strive to make the paper easier to follow.
 
 In the remainder of this response,