residuation: open membership returns residual constraints

1 files changed, 15 insertions, 7 deletions

diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org
index 90cc6c0..f70f459 100644
--- a/docs/virtual-machine-specification.org
+++ b/docs/virtual-machine-specification.org
@@ -53,14 +53,21 @@ runs any goal decidable under the current substitution:
 - a universal runs once its quantifier is decidable, checking the
   body against every quantifier solution.
 
-Goals that are not yet decidable wait. If none can ever run, the plan
-is rejected with the stuck goals named. This is the whole of the
-distinction the specification demands: membership checks, constraints
+Goals that are not yet decidable wait. When only waiting goals
+remain, membership residuates and search rejects: if every remaining
+goal is builtin membership, the answer carries them as residual
+constraints; if any is a stalled search, the plan is rejected with
+the stuck goals named. This is the whole of the distinction the
+specification demands: membership checks or residuates, constraints
 wait, generation only under bounds, and non total plans do not
 execute.
 
-Answers are the query's free variables resolved to canonical values.
-Variables that live only under a universal are not answer variables.
+Answers are the query's free variables resolved to canonical values,
+plus the residual constraints the answer is conditioned on; the
+common case is ground and residue free. Variables that live only
+under a universal are not answer variables. Integrity criteria
+accept only residue free proof: a conditioned answer admits no
+fact.
 
 * Totality accounting
 
@@ -122,8 +129,9 @@ whole or not at all.
 Specified, not yet implemented; each grows admission or planning
 without changing admitted semantics:
 
-- residuation: a constraint store that returns residual constraints
-  for satisfiable but underdetermined queries instead of rejecting;
+- constraint propagation: residuated constraints today wait and
+  return; a store that actively narrows domains and detects
+  unsatisfiable residue early is the next strength;
 - symbolic discharge: algebraic evidence for universals over
   infinite domains, and arithmetic decrease measures for recursion
   that structural containment cannot see;