residuation: open membership returns residual constraints

2 files changed, 23 insertions, 10 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;
diff --git a/docs/vm.org b/docs/vm.org
index 4253231..8d1215a 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -56,9 +56,14 @@ decidable wait. So conjunction stays commutative in fact, not just in
 doctrine: the page order of =:and= operands never matters, and the
 tests assert it.
 
-If no remaining goal can ever run, the plan is rejected as non
-total. =[Integer value: X]= alone is not an enumeration, it is an
-error telling you to bind or bound =X=. Membership is not generation.
+When goals remain that cannot run, two things can happen. If every
+one of them is pure membership, decidable the moment its variables
+ground, the answer comes back with those goals as residual
+constraints: =[Integer value: X]= alone answers =X= conditioned on
+=[Integer value: X]=, which is exactly what the expression means.
+Constraining is not searching. If any remaining goal is a stalled
+search, an unbounded recursion or an infinite universal, the plan is
+rejected as non total. Membership is never generation either way.
 
 Recursive rules unfold only when their witness argument is ground, so
 the admission proof becomes a runtime termination measure: the