more spelling

docs/user-guide/glossary.md

@@ -15,24 +15,35 @@ control flow graph
   control flow graph.
   A CVL rule can be seen as a program with some extra "assert" commands, thus 
   a rule has a CFG like regular programs.
-  Certora Prover's [TAC reports](tac-reports) contain a control flow graph of 
-  the {term}`TAC` intermediate representation of each given CVL rule.
-  Further reading: [wikipedia](https://en.wikipedia.org/wiki/Control-flow_graph)
+  The Certora Prover's [TAC reports](tac-reports) contain a control flow graph 
+  of the {term}`TAC` intermediate representation of each given CVL rule.
+  Further reading: [Wikipedia](https://en.wikipedia.org/wiki/Control-flow_graph)
   % TODO: ok to mention TAC here?
 
-
 environment
   The environment of a method call refers to the global variables that solidity
   provides, including `msg`, `block`, and `tx`.  CVL represents these variables
   in a structure of type {ref}`env <env>`.  The environment does *not* include
   the contract state or the state of other contracts --- these are referred to
   as the {ref}`storage <storage-type>`.
 
+EVM
+Ethereum Virtual Machine
+EVM bytecode
+  EVM is short for Ethereum Virtual Machine.
+  EVM bytecode is one of the source languages that the Certora Prover internally
+  can take as input for verification. It is produced by the Solidity and Vyper 
+  compilers, among others.
+  For details on what the EVM is and how it works, the following links provide
+  good entry points.
+  [Official documentation](https://ethereum.org/en/developers/docs/evm/)
+  [Wikipedia](https://en.wikipedia.org/wiki/Ethereum#Virtual_machine)
+
 havoc
-  In some cases, the Prover should assume that some variables can change in an
-  unknown way.  For example, an external function on an unknown contract may
-  have an arbitrary effect on the state of a third contract.  In this case, we
-  say that the variable was "havoced".  See {ref}`havoc-summary` and
+  In some cases, the Certora Prover should assume that some variables can change 
+  in an unknown way.  For example, an external function on an unknown contract 
+  may have an arbitrary effect on the state of a third contract.  In this case, 
+  we say that the variable was "havoced".  See {ref}`havoc-summary` and
   {ref}`havoc-stmt` for more details.
 
 hyperproperty
@@ -50,8 +61,13 @@ model
 example
 counterexample
   The terms "model", "example", and "counterexample" are used interchangeably.
-  They all refer to an assignment of values to all of the CVL variables and
-  contract storage.  See {ref}`rule-overview`.
+  In the context of a CVL rule, they refer to an assignment of values to all of 
+  the CVL variables and contract storage that either violates an `assert` statement 
+  or fulfills a `satisfy` statement. See {ref}`rule-overview`.
+  In the context of {term}`SMT solver`s, a model is a valuation of the logical 
+  constants and uninterpreted functions in the input formula that makes the formula
+  evaluate to `true`.
+
 
 linear arithmetic
 nonlinear arithmetic
@@ -69,9 +85,11 @@ underapproximation
   simpler that is easier to reason about.  If the approximation includes all of
   the possible behaviors of the original code (and possibly others), it is
   called an "overapproximation"; if it does not then it is called an
-  "underapproximation".  For example, a {ref}`NONDET <view-summary>` summary is
+  "underapproximation".  
+  
+  Example: A {ref}`NONDET <view-summary>` summary is
   an overapproximation because every possible value that the original
-  implementation could return is considered by the Prover, while an
+  implementation could return is considered by the Certora Prover, while an
   {ref}`ALWAYS <view-summary>` summary is an underapproximation if the
   summarized method could return more than one value.
 
@@ -83,8 +101,8 @@ underapproximation
 
 parametric rule
   A parametric rule is a rule that calls an ambiguous method, either using a
-  method variable, or using an overloaded function name.  The Prover will
-  generate a separate report for each possible instantiation of the method.
+  method variable, or using an overloaded function name. The Certora Prover 
+  will generate a separate report for each possible instantiation of the method.
   See {ref}`parametric-rules` for more information.
 
 quantifier
@@ -99,9 +117,20 @@ sanity
   This section is incomplete.  See {ref}`--rule_sanity` and {ref}`built-in-sanity` for partial information.
   ```
 
+SAT result
+UNSAT result
+  *SAT* and *UNSAT* are the results that an {term}`SMT solver` returns on a 
+  successful run (i.e. not a timeout). SAT means that the input formula is 
+  satisfiable and a {term}`model` has been found. UNSAT means that the input 
+  formula is unsatisfiable (and thus there is no model for it).
+  Within the Certora Prover, what SAT means depends on the type of rule 
+  being checked: For an `assert` rule, SAT means a violation, while for a 
+  `satisfy` rule, SAT means non-violation of the rule, and vice versa for UNSAT. 
+  (See also {ref}`rule-overview`.)
+
 scene
-  The *scene* refers to the set of contract instances that the Prover knows
-  about.
+  The *scene* refers to the set of contract instances that the Certora Prover 
+  knows about.
 
 SMT
 SMT solver
@@ -117,30 +146,30 @@ SMT solver
   formula evaluate to "true". For instance, on the formula "x > 5 /\ x = y * y", 
   a solver will return SAT, and produce any valuation where x is the square of
   an integer and larger than 5, and y is the root of x.
-  Further reading: [wikipedia](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
+  Further reading: [Wikipedia](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
 
 sound
 unsound
   Soundness means that any rule violations in the code being verified are
-  guaranteed to be reported by the Prover.  Unsound approximations such as
-  loop unrolling or certain kinds of harnessing may cause real bugs to be
-  missed by the Prover, and should therefore be used with caution.  See
+  guaranteed to be reported by the Certora Prover.  Unsound approximations 
+  such as loop unrolling or certain kinds of harnessing may cause real bugs 
+  to be missed by the Prover, and should therefore be used with caution. See
   {doc}`/docs/prover/approx/index` for more details.
 
 summary
 summarize
   A method summary is a user-provided approximation of the behavior of a
   contract method.  Summaries are useful if the implementation of a method is
-  not available or if the implementation is too complex for the Prover to
-  analyze without timing out.  See {doc}`/docs/cvl/methods` for
+  not available or if the implementation is too complex for the Certora 
+  Prover to analyze without timing out.  See {doc}`/docs/cvl/methods` for
   complete information on different types of method summaries.
 
 TAC
   TAC (originally short for "three address code") is an intermediate 
   representation
-  ([wikipedia](https://en.wikipedia.org/wiki/Intermediate_representation))
+  ([Wikipedia](https://en.wikipedia.org/wiki/Intermediate_representation))
   used by the Certora Prover. TAC code is kept invisible to the 
-  user most of the time, so it's details are not in the scope of this 
+  user most of the time, so its details are not in the scope of this 
   documentation. We provide a working understanding, which is helpful for some 
   advanced proving tasks, in the {ref}`tac-reports` section.