Scribble-ify (emina#184)

- More linkify - Fix minor typos - Fix quote style
sorawee · Mar 18, 2021 · a64e2bc · a64e2bc
1 parent ac96664
commit a64e2bc
Show file tree

Hide file tree

Showing 10 changed files with 41 additions and 39 deletions.
diff --git a/rosette/guide/scribble/datatypes/bitvectors.scrbl b/rosette/guide/scribble/datatypes/bitvectors.scrbl
@@ -140,7 +140,7 @@ equality (@racket[bveq]) and signed / unsigned versions of
            [(bvor  [x (bitvector n)] ...+) (bitvector n)]
            [(bvxor [x (bitvector n)] ...+) (bitvector n)])]{
 
-Returns the bitwise "and", "or", "xor" of one or more bitvector values of the same type.
+Returns the bitwise ``and'', ``or'', ``xor'' of one or more bitvector values of the same type.
 
  @examples[#:eval rosette-eval
  (bvand (bv -1 4) (bv 2 4))

diff --git a/rosette/guide/scribble/datatypes/vectors.scrbl b/rosette/guide/scribble/datatypes/vectors.scrbl
@@ -2,7 +2,8 @@
 
 @(require (for-label 
            rosette/base/form/define rosette/query/query 
-           rosette/base/core/term  
+           rosette/base/core/term
+           rosette/solver/solution
            (only-in rosette/base/base assert define-symbolic union?
                     vc clear-vc! bitvector bitvector? bv?
                     bitvector->natural integer->bitvector

diff --git a/rosette/guide/scribble/essentials/essentials.scrbl b/rosette/guide/scribble/essentials/essentials.scrbl
@@ -1,19 +1,21 @@
 #lang scribble/manual
 
-@(require (for-label racket (only-in racket/sandbox with-deep-time-limit))
-          (for-label  
+@(require (for-label
+           racket
+           (only-in racket/sandbox with-deep-time-limit)
            rosette/base/form/define
-           (only-in rosette/base/base assert assume vc vc-asserts vc-assumes clear-vc!)
-           rosette/query/query 
-           (only-in rosette/base/base bv? bitvector
+           rosette/query/query
+           rosette/solver/solution
+           (only-in rosette/base/base
+                    assert assume vc vc-asserts vc-assumes clear-vc!
+                    bv? bitvector
                     bvsdiv bvadd bvsle bvsub bvand
                     bvor bvxor bvshl bvlshr bvashr
                     bvnot bvneg)
            rosette/lib/synthax))
 
-@(require racket/sandbox  racket/runtime-path  scribble/core scribble/racket
-          scribble/example scribble/html-properties scriblib/footnote 
-          (only-in racket [unsyntax racket/unsyntax]))
+@(require racket/sandbox racket/runtime-path scribble/core scribble/racket
+          scribble/example scribble/html-properties scriblib/footnote)
 
 @(require (only-in "../refs.scrbl" ~cite rosette:onward13 rosette:pldi14)
           "../util/lifted.rkt")
@@ -140,7 +142,7 @@ Assumptions behave analogously to assertions on both concrete and symbolic value
 
 @section[#:tag "sec:queries"]{Solver-Aided Queries}
 
-The solver reasons about assumed and asserted properties only when we ask a question about them---for example, "Does my program have an execution that violates an assertion while satisfying all the assumptions?"  We pose such @emph{solver-aided queries} with the help of constructs explained in the remainder of this chapter.
+The solver reasons about assumed and asserted properties only when we ask a question about them---for example, ``Does my program have an execution that violates an assertion while satisfying all the assumptions?''  We pose such @emph{solver-aided queries} with the help of constructs explained in the remainder of this chapter.
 
 We will illustrate the queries on the following toy example. Suppose that we want to implement a
 procedure @racket[bvmid] that takes as input two non-negative 32-bit integers, @racket[lo] ≤ @racket[hi],
@@ -321,7 +323,7 @@ The synthesis query takes the form @racket[(synthesize #:forall #, @var[input] #
 
 Rosette supports one more solver-aided query, which we call angelic execution. This query is the dual of verification.  Given a program with symbolic values, it instructs the solver to find a binding for them that will cause the program to execute normally---that is, without any assumption or assertion failures. 
 
-Angelic execution can be used to solve puzzles, to run incomplete code, or to "invert" a program, by searching for inputs that produce a desired output.  For example, we can ask the solver to search for two distinct legal inputs, @racket[l] and @racket[h], whose midpoint is the bitwise-and of their bits: 
+Angelic execution can be used to solve puzzles, to run incomplete code, or to ``invert'' a program, by searching for inputs that produce a desired output.  For example, we can ask the solver to search for two distinct legal inputs, @racket[l] and @racket[h], whose midpoint is the bitwise-and of their bits:
 @examples[#:eval rosette-eval #:label #f 
 (define (bvmid-fast lo hi)
   (bvlshr (bvadd hi lo) (bv #x00000001 32)))
@@ -480,7 +482,7 @@ n2
 n3]
 In general, recursion terminates under symbolic evaluation only when the stopping condition is reached with concrete values.
 
-We can force termination by placing a concrete bound @var{k} on the number of times @racket[bvsqrt] can call itself recursively. This approach is called @deftech{finitization}, and it is the standard way to handle unbounded loops and recursion under symbolic evaluation. The following code shows how to implement a @emph{sound} finitization policy. If a @racket[verify] query returns @racket[(unsat)] under a sound policy, we know that (1) the unrolling bound @var{k} is sufficient to execute all possible inputs to  @racket[bvsqrt], and (2) all of these executions satisfy the query. If we pick a bound that is too small, the query will generate a counterexample input that needs a larger bound to compute the result. In our example, the bound of 16 is sufficient to verify the correctness of @racket[sqrt] on all inputs: 
+We can force termination by placing a concrete bound @var{k} on the number of times @racket[bvsqrt] can call itself recursively. This approach is called @deftech{finitization}, and it is the standard way to handle unbounded loops and recursion under symbolic evaluation. The following code shows how to implement a @emph{sound} finitization policy. If a @racket[verify] query returns @racket[(unsat)] under a sound policy, we know that (1) the unrolling bound @var{k} is sufficient to execute all possible inputs to  @racket[bvsqrt], and (2) all of these executions satisfy the query. If we pick a bound that is too small, the query will generate a counterexample input that needs a larger bound to compute the result. In our example, the bound of 16 is sufficient to verify the correctness of @racket[bvsqrt] on all inputs:
 @(rosette-eval '(clear-vc!))
 @(rosette-eval '(require (only-in racket make-parameter parameterize)))
 @examples[#:eval rosette-eval #:label #f #:no-prompt

diff --git a/rosette/guide/scribble/forms/forms.scrbl b/rosette/guide/scribble/forms/forms.scrbl
@@ -5,7 +5,7 @@
 
 @title[#:tag "ch:syntactic-forms" #:style 'toc]{Syntactic Forms}
 
-The core of the Rosette language (@racket[rosette/safe]) consists of two kinds of syntax forms: a set of basic  forms @deftech[#:key "lifted constructs"]{lifted} from Racket, and a set of forms for @seclink["ch:essentials"]{solver-aided programming}.  We use the term "lifted" to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.
+The core of the Rosette language (@racketmodname[rosette/safe]) consists of two kinds of syntax forms: a set of basic  forms @deftech[#:key "lifted constructs"]{lifted} from Racket, and a set of forms for @seclink["ch:essentials"]{solver-aided programming}.  We use the term ``lifted'' to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.
 
 @[table-of-contents]
 @include-section["racket-forms.scrbl"]

diff --git a/rosette/guide/scribble/libs/libraries.scrbl b/rosette/guide/scribble/libs/libraries.scrbl
@@ -4,7 +4,7 @@
 
 @title[#:tag "ch:libraries" #:style 'toc]{Libraries}
 
-Chapters @seclink["ch:getting-started"]{1}-@seclink["ch:programmer-defined-datatypes"]{5} introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by @racket[rosette/safe], as well as Rosette libraries that provide additional facilities for solver-aided development.
+Chapters @seclink["ch:getting-started"]{1}-@seclink["ch:programmer-defined-datatypes"]{5} introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by @racketmodname[rosette/safe], as well as Rosette libraries that provide additional facilities for solver-aided development.
 
 @[table-of-contents]
 

diff --git a/rosette/guide/scribble/libs/racket-libs.scrbl b/rosette/guide/scribble/libs/racket-libs.scrbl
@@ -17,5 +17,4 @@ Rosette exports the following facilities from the core Racket libraries:
 
 These facilities are safe to use in Rosette programs, even in the presence of symbolic values, assertions, and solver-aided queries. They are not, however, @tech[#:key "lifted constructs"]{lifted}:  if their Racket implementation expects a concrete value of a given type, they will fail when given a symbolic value.  These constructs are safe to use in the sense that they will fail in a predictable fashion, according to their concrete Racket specification, instead of causing the enclosing Rosette program to exhibit unexpected behavior.
 
-The @racket[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism.  This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}.  Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files).  In other words, arbitrary Racket code is, by default, unsafe to use.
-
+The @racketmodname[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism.  This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}.  Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files).  In other words, arbitrary Racket code is, by default, unsafe to use.
diff --git a/rosette/guide/scribble/libs/rosette-libs.scrbl b/rosette/guide/scribble/libs/rosette-libs.scrbl
@@ -367,7 +367,7 @@ sol
   generated for programs that have been saved to disk.
 
   This procedure cooperates with the constructs in the
-  @racket[rosette/lib/synthax] library to turn solutions into
+  @racketmodname[rosette/lib/synthax] library to turn solutions into
   code. It works by scanning program files for
   @racketlink[??]{constant}, @racketlink[choose]{choice}, and
   @racketlink[define-grammar]{grammar} holes, and replacing
@@ -471,4 +471,4 @@ sol
 }
 
 
-@(kill-evaluator rosette-eval)
+@(kill-evaluator rosette-eval)
diff --git a/rosette/guide/scribble/performance/performance.scrbl b/rosette/guide/scribble/performance/performance.scrbl
@@ -55,7 +55,7 @@ integers and reals (while being correct under the
 finite-precision semantics). For example, this program
 incorrectly says that no integer greater than 15 exists,
 because the setting of @racket[current-bitwidth] causes it
-to consider only values of @racket{x} that can be
+to consider only values of @racket[x] that can be
 represented as a 5-bit bitvector.
 
 @examples[#:eval rosette-eval #:label #f
@@ -387,15 +387,15 @@ the performance of @tt{verify-xform} to degrade, from a
 couple of seconds when @tt{N} = 5 to over a minute when @tt{N}
 = 20. To identify the source of this performance issue, we
 can invoke the @tech{symbolic profiler} on the verifier,
-producing the output below (after selecting the "Collapse
-solver time" checkbox):
+producing the output below (after selecting the ``Collapse
+solver time'' checkbox):
 
 @(image profile-xform.png #:scale 0.425)
 
 The symbolic profiler identifies @tt{list-set} as the
 bottleneck in this program. The output shows that @tt{list-set}
 creates many symbolic terms, and performs many symbolic
-operations (the "Union Size" and "Merge Cases" columns).
+operations (the ``Union Size'' and ``Merge Cases'' columns).
 
 The core issue here is an @tech{algorithmic mismatch}: @tt{list-set}
 makes a recursive call guarded by a short-circuiting
@@ -431,4 +431,4 @@ and so the verification conditions no longer grow quadratically.
 (list-set* '(1 2 3) idx 4)]
 
 The performance of @tt{verify-xform} after this change
-improves by 3× for @tt{N} = 20.
+improves by 3× for @tt{N} = 20.
diff --git a/rosette/guide/scribble/unsafe/unsafe.scrbl b/rosette/guide/scribble/unsafe/unsafe.scrbl
@@ -13,20 +13,20 @@
 @title[#:tag "ch:unsafe"]{Unsafe Operations}
 
 Throughout this guide, we have assumed that Rosette programs are 
-written in the @racket[rosette/safe] dialect of the full language.  
+written in the @racketmodname[rosette/safe] dialect of the full language.
 This dialect extends a core subset of Racket with @seclink["ch:essentials"]{solver-aided 
-functionality}.  In this chapter, we briefly discuss the @racket[rosette] 
+functionality}.  In this chapter, we briefly discuss the @racketmodname[rosette]
 dialect of the language, which exports all of Racket.  
 
-Safe use of the full @racket[rosette] language requires a basic understanding 
+Safe use of the full @racketmodname[rosette] language requires a basic understanding
 of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14].  
 Briefly, the SVM hijacks the normal Racket execution for all procedures and 
-constructs that are exported by @racket[rosette/safe].  Any programs that are 
-implemented exclusively in the @racket[rosette/safe] language are therefore 
+constructs that are exported by @racketmodname[rosette/safe].  Any programs that are
+implemented exclusively in the @racketmodname[rosette/safe] language are therefore
 fully under the SVM's control.  This means that the SVM can correctly interpret 
 the application of a procedure or a macro to a symbolic value, and it 
 can correctly handle any side-effects (in particular, writes to memory) performed 
-by @racket[rosette/safe] code.
+by @racketmodname[rosette/safe] code.
 
 The following snippet demonstrates the non-standard execution that the SVM needs to 
 perform in order to assign the expected meaning to Rosette code:
@@ -53,17 +53,17 @@ y
 (define sol2 (solve (assert (not b))))
 (evaluate y sol2)]
 
-Because the SVM controls only the execution of @racket[rosette/safe] code, 
-it cannot, in general, guarantee the safety or correctness of arbitrary @racket[rosette] programs. 
-As soon as a @racket[rosette] program calls an @tech[#:key "lifted construct"]{unlifted} Racket construct  
-(that is, a procedure or a macro not implemented in or provided by the @racket[rosette/safe] language), 
+Because the SVM controls only the execution of @racketmodname[rosette/safe] code,
+it cannot, in general, guarantee the safety or correctness of arbitrary @racketmodname[rosette] programs.
+As soon as a @racketmodname[rosette] program calls an @tech[#:key "lifted construct"]{unlifted} Racket construct
+(that is, a procedure or a macro not implemented in or provided by the @racketmodname[rosette/safe] language),
 the execution escapes back to the Racket interpreter.  The SVM has no control over the side-effects 
 performed by the Racket interpreter, or the meaning that it (perhaps incorrectly) assigns to programs 
 in the presence of symbolic values.  As a result, the programmer is responsible for ensuring that 
-a @racket[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
+a @racketmodname[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
 
-As an example of incorrect behavior, consider the following @racket[rosette] snippet.  
-The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racket[rosette/safe].
+As an example of incorrect behavior, consider the following @racketmodname[rosette] snippet.
+The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racketmodname[rosette/safe].
 Whenever they are invoked, the execution escapes to the Racket interpreter.
 
 @(rosette-eval '(require (only-in racket make-hash hash-clear! hash-ref)))
@@ -105,4 +105,4 @@ as long as they iterate over concrete sequences, and all guard expressions produ
 each iteration.  In practice, Rosette programs can safely use many common Racket constructs, and with a 
 bit of experience, it becomes easy to see when it is okay to break the effectively-concrete rule.
 
-@(kill-evaluator rosette-eval)
+@(kill-evaluator rosette-eval)
diff --git a/rosette/guide/scribble/welcome/welcome.scrbl b/rosette/guide/scribble/welcome/welcome.scrbl
@@ -16,7 +16,7 @@ Rosette is a @emph{solver-aided} programming system with two components:
                 compiles them to logical constraints.  The SVM enables Rosette 
                 to use the solver to automatically reason about program behaviors.}]
 
-The name "Rosette" refers both to the language and the whole system.
+The name ``Rosette'' refers both to the language and the whole system.
 
 @section[#:tag "sec:get"]{Installing Rosette}
Original file line number	Diff line number	Diff line change
Expand Up		@@ -17,5 +17,4 @@ Rosette exports the following facilities from the core Racket libraries:

		These facilities are safe to use in Rosette programs, even in the presence of symbolic values, assertions, and solver-aided queries. They are not, however, @tech[#:key "lifted constructs"]{lifted}: if their Racket implementation expects a concrete value of a given type, they will fail when given a symbolic value. These constructs are safe to use in the sense that they will fail in a predictable fashion, according to their concrete Racket specification, instead of causing the enclosing Rosette program to exhibit unexpected behavior.

		The @racket[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism. This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}. Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files). In other words, arbitrary Racket code is, by default, unsafe to use.

		The @racketmodname[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism. This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}. Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files). In other words, arbitrary Racket code is, by default, unsafe to use.