Constraint violation under epistemic reduction names the wrong authored constraint
Audited revision
4ea98a5a0833470256dc416a659c2845810d0418 (origin/main), binary xlog-cli 0.12.0, sha256 783b84b99b10f81d7ad56df95064e7e23935b4f73a2bdc59ce4358fe5b8edc9d, clean tracked tree.
Summary
When a program in epistemic_mode = faeel contains an epistemic-bodied constraint textually before an ordinary constraint, and the ordinary constraint is violated, the error message names the epistemic constraint — one that cannot have fired. The violation index is raised in the reduced constraint space (epistemic-bodied constraints dropped), but the presentation resolves it against the authored constraint list.
This is a follow-up to #213. The UnsupportedEpistemicConstruct { "epistemic GPU transfer budget" } false cause is fixed and verified — an ordinary expectation break in an epistemic scenario now reports a constraint violation. But the constraint it names is only correct when no epistemic-bodied constraint precedes the violated one.
Reproduction
xlog run /dev/stdin <<'EOF'
#pragma epistemic_mode = faeel
pred p(u32).
pred q(u32).
pred kp(u32).
p(1).
kp(X) :- p(X), know p(X).
:- q(X), know p(X).
:- p(X).
?- kp(X).
EOF
q has no facts, so authored constraint 0 (:- q(X), know p(X).) cannot fire. p(1) exists, so authored constraint 1 (:- p(X).) is violated.
Observed:
Error: Execution("Constraint 0 violated: :- q(X), know p(X).")
rc=1. The message names the unviolated epistemic constraint.
Control — identical program with the two constraints swapped (violated ordinary constraint is authored 0 = reduced 0):
Error: Execution("Constraint 0 violated: :- p(X).")
Correct. The defect is ordering-dependent, which is exactly the signature of an index-space mismatch, not a text-formatting bug.
Root cause pointer
crates/xlog-gpu/src/logic.rs:
constraint_violation_error resolves authored_constraints.get(constraint_index) (falling back to source_program.constraints.get(constraint_index)), where constraint_index arrives from the epistemic execution path in reduced space.present_epistemic_constraint_violation guards constraint_index < self.program.constraints.len() — a range check on the normalized program, not a translation between the reduced and authored index spaces.
The fix needs a reduced→authored index map built when the reduction drops epistemic-bodied constraints, applied before presentation.
Impact
The current mistaber corpus contains zero epistemic-bodied constraints (grep -rn '^\s*:-.*\(know\|possible\)' programs/ scenarios/ → 0), so the 1,348 live scenarios cannot trigger the misnaming today; their epistemic scenarios now report honestly. The defect gates BrainyBlaze/mistaber-xlog#18, whose closure criterion requires the mixed witness to name the authored violated constraint.
Constraint violation under epistemic reduction names the wrong authored constraint
Audited revision
4ea98a5a0833470256dc416a659c2845810d0418(origin/main), binaryxlog-cli 0.12.0, sha256783b84b99b10f81d7ad56df95064e7e23935b4f73a2bdc59ce4358fe5b8edc9d, clean tracked tree.Summary
When a program in
epistemic_mode = faeelcontains an epistemic-bodied constraint textually before an ordinary constraint, and the ordinary constraint is violated, the error message names the epistemic constraint — one that cannot have fired. The violation index is raised in the reduced constraint space (epistemic-bodied constraints dropped), but the presentation resolves it against the authored constraint list.This is a follow-up to #213. The
UnsupportedEpistemicConstruct { "epistemic GPU transfer budget" }false cause is fixed and verified — an ordinary expectation break in an epistemic scenario now reports a constraint violation. But the constraint it names is only correct when no epistemic-bodied constraint precedes the violated one.Reproduction
qhas no facts, so authored constraint 0 (:- q(X), know p(X).) cannot fire.p(1)exists, so authored constraint 1 (:- p(X).) is violated.Observed:
rc=1. The message names the unviolated epistemic constraint.
Control — identical program with the two constraints swapped (violated ordinary constraint is authored 0 = reduced 0):
Correct. The defect is ordering-dependent, which is exactly the signature of an index-space mismatch, not a text-formatting bug.
Root cause pointer
crates/xlog-gpu/src/logic.rs:constraint_violation_errorresolvesauthored_constraints.get(constraint_index)(falling back tosource_program.constraints.get(constraint_index)), whereconstraint_indexarrives from the epistemic execution path in reduced space.present_epistemic_constraint_violationguardsconstraint_index < self.program.constraints.len()— a range check on the normalized program, not a translation between the reduced and authored index spaces.The fix needs a reduced→authored index map built when the reduction drops epistemic-bodied constraints, applied before presentation.
Impact
The current mistaber corpus contains zero epistemic-bodied constraints (
grep -rn '^\s*:-.*\(know\|possible\)' programs/ scenarios/→ 0), so the 1,348 live scenarios cannot trigger the misnaming today; their epistemic scenarios now report honestly. The defect gates BrainyBlaze/mistaber-xlog#18, whose closure criterion requires the mixed witness to name the authored violated constraint.