# SPEC 11 and 12: checking proofs. Each case checks a proof document against
# a program and expects the exact report. Failure details are free text.

=== a valid proof is checked
spec: 11, 12
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
implies(q(X), r(X))
--- proof.py
q('a')
r('a')

clause(1, fact(p('a')))
clause(2, implies(p(X), q(X)))
clause(3, implies(q(X), r(X)))

step(q('a'), clause(2), {'X': 'a'}, [p('a')])
step(p('a'), clause(1), {}, [])
step(r('a'), clause(3), {'X': 'a'}, [q('a')])
--- stdout
condition('C1', 'resolution', 'ok', 3)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', 'ok', 3)
condition('C4', 'coverage', 'ok', 4)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 5)
steps(3)
verified(3)
recomputed(0)
composed(0)
trusted(0)
claims(2)
verdict('checked')

=== the proof can come from standard input
spec: 14
args: --check-proof - program.py
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
--- stdin
q('a')

step(q('a'), clause(2), {'X': 'a'}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== C1: a clause display that differs from the program fails
spec: 11.1, 11.2
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
--- proof.py
q('a')

clause(1, fact(p('b')))

step(q('a'), clause(2), {'X': 'a'}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', failed(1), 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
failure('C1', clause(1, fact(p('b'))), …)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C1: the program, not the display, is the authority
spec: 11.2
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('b'))
implies(p(X), q(X))
--- proof.py
q('a')

clause(1, fact(p('a')))

step(q('a'), clause(2), {'X': 'a'}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', failed(2), 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
failure('C1', clause(1, fact(p('a'))), …)
failure('C1', p('a'), …)
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(2))

=== C1: a binding that disagrees with the goal fails
spec: 11.2
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
--- proof.py
q('a')

step(q('a'), clause(2), {'X': 'b'}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', failed(1), 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
failure('C1', q('a'), …)
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C1: a use that is not the rule's body fails
spec: 11.2
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'), p('b'))
implies(p(X), q(X))
--- proof.py
q('a')

step(q('a'), clause(3), {'X': 'a'}, [p('b')])
step(p('b'), clause(2), {}, [])
--- stdout
condition('C1', 'resolution', failed(1), 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
failure('C1', q('a'), …)
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C1: an unknown clause number fails
spec: 11.2
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
--- proof.py
q('a')

step(q('a'), clause(999), {'X': 'a'}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', failed(1), 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
failure('C1', q('a'), …)
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C1: variable sharing in a source clause cannot be forged
spec: 11.2
args: --check-proof proof.py --goal "same(A, B)" program.py
exit: 2
--- program.py
from peye import *
fact(same(X, X))
--- proof.py
same('a', 'b')

step(same('a', 'b'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', failed(1), 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C1', same('a', 'b'), …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C2: a step that depends on itself fails
spec: 11.3
args: --check-proof proof.py --goal "p()" program.py
exit: 2
--- program.py
from peye import *
implied_by(p, p)
--- proof.py
p()

step(p(), clause(1), {}, [p()])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', failed(1), 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C2', 'p', …)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C3: an unknown justification fails
spec: 11.4
args: --check-proof proof.py --goal "p(X)" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), 'magic', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', failed(1), 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C3', p('a'), …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C3: two steps for one goal fail
spec: 11.1
args: --check-proof proof.py --goal "p(X)" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), clause(1), {}, [])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', failed(1), 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C3', p('a'), …)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C3: bindings that are not a dictionary fail
spec: 11.1
args: --check-proof proof.py --goal "p(X)" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), clause(1), 'broken', [])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 0)
condition('C3', 'justification', failed(1), 0)
condition('C4', 'coverage', failed(1), 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 1)
failure('C3', p('a'), …)
failure('C4', p('a'), …)
steps(0)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(2))

=== C3: a builtin step has no uses
spec: 11.4
args: --check-proof proof.py --goal "1 < 2" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
1 < 2

step(1 < 2, 'builtin', {}, [p('a')])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', failed(1), 1)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C3', 1 < 2, …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C3: a builtin step must name a primitive
spec: 11.4
args: --check-proof proof.py --goal "p(X)" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), 'builtin', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', failed(1), 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C3', p('a'), …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C3: a document that does not read fails
spec: 9, 11.1
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
x = 1
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 0)
condition('C3', 'justification', failed(1), 0)
condition('C4', 'coverage', 'ok', 0)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 0)
failure('C3', 'proof_document', …)
steps(0)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(0)
verdict(failed(1))

=== C3: a document is never executed
spec: 9, 11.1, 15
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
__import__('os').system('echo executed')
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 0)
condition('C3', 'justification', failed(1), 0)
condition('C4', 'coverage', 'ok', 0)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 0)
failure('C3', 'proof_document', …)
steps(0)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(0)
verdict(failed(1))

=== C4: an empty document claims nothing, and so checks
spec: 11.5
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(p('a'))
--- proof.py
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 0)
condition('C3', 'justification', 'ok', 0)
condition('C4', 'coverage', 'ok', 0)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 0)
steps(0)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(0)
verdict('checked')

=== C4: a claim and a use without a step fail
spec: 11.5
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
implies(q(X), r(X))
--- proof.py
q('a')
r('a')

step(p('a'), clause(1), {}, [])
step(r('a'), clause(3), {'X': 'a'}, [q('a')])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', failed(2), 3)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', failed(1), 4)
failure('C4', q('a'), …)
failure('C4', r('a'), …)
failure('C7', p('a'), …)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(2)
verdict(failed(3))

=== C4: a use may be a fact of the program without a step
spec: 11.5
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
--- proof.py
q('a')

step(q('a'), clause(2), {'X': 'a'}, [p('a')])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== C4: a use may be an instance of a fact with variables
spec: 11.5
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(same(X, X), item(1))
implies(item(Y) & same(Y, Y), twin(Y))
--- proof.py
twin(1)

step(twin(1), clause(3), {'Y': 1}, [item(1), same(1, 1)])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 3)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== C4 and C7: an unrelated claim fails
spec: 11.5, 11.8
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X))
--- proof.py
q('a')
unrelated('x')

step(q('a'), clause(2), {'X': 'a'}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', failed(1), 3)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', failed(1), 4)
failure('C4', unrelated('x'), …)
failure('C7', unrelated('x'), …)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(2)
verdict(failed(2))

=== C5: a primitive is recomputed
spec: 11.6
args: --check-proof proof.py --goal "is_(5, 2 + 3)" program.py
--- program.py
from peye import *
--- proof.py
is_(5, 2 + 3)

step(is_(5, 2 + 3), 'builtin', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 1)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
steps(1)
verified(0)
recomputed(1)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== C5: a primitive that does not hold fails
spec: 11.6
args: --check-proof proof.py --goal "is_(7, 2 + 3)" program.py
exit: 2
--- program.py
from peye import *
--- proof.py
is_(7, 2 + 3)

step(is_(7, 2 + 3), 'builtin', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', failed(1), 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C5', is_(7, 2 + 3), …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C5: a primitive that would need to bind something fails
spec: 11.6
args: --check-proof proof.py --goal "is_(X, 2 + 3)" program.py
exit: 2
--- program.py
from peye import *
--- proof.py
is_(X, 2 + 3)

step(is_(X, 2 + 3), 'builtin', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', failed(1), 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C5', is_(A, 2 + 3), …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C5: a control step is composed of its uses
spec: 11.6
args: --check-proof proof.py --goal "call(p(X))" program.py
--- program.py
from peye import *
fact(p('a'))
--- proof.py
call(p('a'))

step(call(p('a')), 'control', {}, [p('a')])
step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 1)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
steps(2)
verified(1)
recomputed(0)
composed(1)
trusted(0)
claims(1)
verdict('checked')

=== C5: a control step must follow from its uses
spec: 11.6
args: --check-proof proof.py --goal "call(p(X))" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
call(p('b'))

step(call(p('b')), 'control', {}, [p('a')])
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', failed(1), 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
failure('C5', call(p('b')), …)
steps(1)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C5: either side of a disjunction composes it
spec: 11.6
args: --check-proof proof.py --goal "p(X) | q(X)" program.py
--- program.py
from peye import *
fact(q('a'))
--- proof.py
p('a') | q('a')

step(p('a') | q('a'), 'control', {}, [q('a')])
step(q('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 1)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
steps(2)
verified(1)
recomputed(0)
composed(1)
trusted(0)
claims(1)
verdict('checked')

=== obligations are listed and make the verdict conditional
spec: 11.7, 12
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(p(1), p(2))
implies(p(X) & ~blocked(X), ok(X))
implies(findall(X, p(X), L), all_of(L))
--- proof.py
ok(1)
ok(2)
all_of([1, 2])

step(ok(1), clause(3), {'X': 1}, [p(1), ~blocked(1)])
step(p(1), clause(1), {}, [])
step(~blocked(1), 'absent', {}, [])
step(ok(2), clause(3), {'X': 2}, [p(2), ~blocked(2)])
step(p(2), clause(2), {}, [])
step(~blocked(2), 'absent', {}, [])
step(all_of([1, 2]), clause(4), {'L': [1, 2]}, [findall(X, p(X), [1, 2])])
step(findall(X, p(X), [1, 2]), 'collected', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 5)
condition('C2', 'well_founded', 'ok', 8)
condition('C3', 'justification', 'ok', 8)
condition('C4', 'coverage', 'ok', 8)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 3)
condition('C7', 'relevance', 'ok', 11)
obligation('absent', 'theory_scoped', ~blocked(1))
obligation('absent', 'theory_scoped', ~blocked(2))
obligation('collected', 'theory_scoped', findall(A, p(A), [1, 2]))
steps(8)
verified(5)
recomputed(0)
composed(0)
trusted(3)
claims(3)
verdict('checked_with_obligations')

=== strict checking forbids trusted boundaries
spec: 11.6, 14
args: --strict-proof --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p(1))
implies(p(X) & ~blocked(X), ok(X))
--- proof.py
ok(1)

step(ok(1), clause(2), {'X': 1}, [p(1), ~blocked(1)])
step(p(1), clause(1), {}, [])
step(~blocked(1), 'absent', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', 'ok', 3)
condition('C4', 'coverage', 'ok', 3)
condition('C5', 're_decision', failed(1), 0)
condition('C6', 'boundary_consistency', 'ok', 1)
condition('C7', 'relevance', 'ok', 4)
failure('C5', ~blocked(1), …)
obligation('absent', 'theory_scoped', ~blocked(1))
steps(3)
verified(2)
recomputed(0)
composed(0)
trusted(1)
claims(1)
verdict(failed(1))

=== C3: a trusted boundary has no bindings or uses
spec: 11.4
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p(1))
implies(p(X) & ~blocked(X), ok(X))
--- proof.py
ok(1)

step(ok(1), clause(2), {'X': 1}, [p(1), ~blocked(1)])
step(p(1), clause(1), {}, [])
step(~blocked(1), 'absent', {'X': 1}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', failed(1), 3)
condition('C4', 'coverage', 'ok', 3)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 1)
condition('C7', 'relevance', 'ok', 4)
failure('C3', ~blocked(1), …)
obligation('absent', 'theory_scoped', ~blocked(1))
steps(3)
verified(2)
recomputed(0)
composed(0)
trusted(1)
claims(1)
verdict(failed(1))

=== C6: an absence contradicted by a program fact fails
spec: 11.7
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
implies(~p('a'), q)
--- proof.py
'q'

step('q', clause(2), {}, [~p('a')])
step(~p('a'), 'absent', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', failed(1), 1)
condition('C7', 'relevance', 'ok', 3)
failure('C6', ~p('a'), …)
obligation('absent', 'theory_scoped', ~p('a'))
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(1)
claims(1)
verdict(failed(1))

=== C6: an absence contradicted by a primitive fails
spec: 11.7
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
implies(~(struct('<', 1, 2)), q)
--- proof.py
'q'

step('q', clause(1), {}, [~(1 < 2)])
step(~(1 < 2), 'absent', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', failed(1), 1)
condition('C7', 'relevance', 'ok', 3)
failure('C6', ~(1 < 2), …)
obligation('absent', 'theory_scoped', ~(1 < 2))
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(1)
claims(1)
verdict(failed(1))

=== C6: an absence contradicted by a step of the proof fails
spec: 11.7
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(s(1))
implies(s(X), p(X))
implies(s(X) & ~p(X), q(X))
--- proof.py
p(1)
q(1)

step(p(1), clause(2), {'X': 1}, [s(1)])
step(s(1), clause(1), {}, [])
step(q(1), clause(3), {'X': 1}, [s(1), ~p(1)])
step(~p(1), 'absent', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 3)
condition('C2', 'well_founded', 'ok', 4)
condition('C3', 'justification', 'ok', 4)
condition('C4', 'coverage', 'ok', 5)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', failed(1), 1)
condition('C7', 'relevance', 'ok', 6)
failure('C6', ~p(1), …)
obligation('absent', 'theory_scoped', ~p(1))
steps(4)
verified(3)
recomputed(0)
composed(0)
trusted(1)
claims(2)
verdict(failed(1))

=== C6: a collection missing a solution fails
spec: 11.7
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p(1), p(2))
implies(findall(X, p(X), L), all_of(L))
--- proof.py
all_of([1])

step(all_of([1]), clause(3), {'L': [1]}, [findall(X, p(X), [1])])
step(findall(X, p(X), [1]), 'collected', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 2)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', failed(1), 1)
condition('C7', 'relevance', 'ok', 3)
failure('C6', findall(A, p(A), [1]), …)
obligation('collected', 'theory_scoped', findall(A, p(A), [1]))
steps(2)
verified(1)
recomputed(0)
composed(0)
trusted(1)
claims(1)
verdict(failed(1))

=== C6: an absence over a conjunction with shared variables stays undecided
spec: 11.7
args: --check-proof proof.py --goal "ok(X)" program.py
--- program.py
from peye import *
fact(p(1), q(2))
implied_by(ok(X), p(X) & ~(p(Y) & q(Y)))
--- proof.py
ok(1)

step(ok(1), clause(3), {'X': 1}, [p(1), ~(p(Y) & q(Y))])
step(p(1), clause(1), {}, [])
step(~(p(Y) & q(Y)), 'absent', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', 'ok', 3)
condition('C4', 'coverage', 'ok', 3)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 4)
obligation('absent', 'theory_scoped', ~(p(A) & q(A)))
steps(3)
verified(2)
recomputed(0)
composed(0)
trusted(1)
claims(1)
verdict('checked_with_obligations')

=== C7: a claim must answer the question asked
spec: 11.8
args: --check-proof proof.py program.py
exit: 2
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', failed(1), 2)
failure('C7', p('a'), …)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C7: goals asked from outside are the questions
spec: 11.8
args: --check-proof proof.py --goal "p(X)" program.py
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), clause(1), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 2)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== C7: a claim must be an instance of the question, not more general
spec: 11.8
args: --check-proof proof.py --goal "p('a')" program.py
exit: 2
--- program.py
from peye import *
fact(p(X))
--- proof.py
p(Z)

step(p(Z), clause(1), {'X': Z}, [])
--- stdout
condition('C1', 'resolution', 'ok', 1)
condition('C2', 'well_founded', 'ok', 1)
condition('C3', 'justification', 'ok', 1)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', failed(1), 2)
failure('C7', p(A), …)
steps(1)
verified(1)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C7: a step that serves no claim fails
spec: 11.8
args: --check-proof proof.py --goal "p(X)" program.py
exit: 2
--- program.py
from peye import *
fact(p('a'), s('z'))
--- proof.py
p('a')

step(p('a'), clause(1), {}, [])
step(s('z'), clause(2), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', failed(1), 3)
failure('C7', s('z'), …)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== C7: a query's body is a question
spec: 11.8
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(p(1), q(1))
query(p(X), q(X))
--- proof.py
p(1) & q(1)

step(p(1), clause(1), {}, [])
step(q(1), clause(2), {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 2)
condition('C3', 'justification', 'ok', 2)
condition('C4', 'coverage', 'ok', 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 3)
steps(2)
verified(2)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== a halted proof is checked against the forward heads
spec: 11.8
args: --check-proof proof.py --goal "p(X)" program.py
--- program.py
from peye import *
fact(account('bob', -5))
contradiction(account(O, B), B < 0)
--- proof.py
'false'

step('false', clause(2), {'O': 'bob', 'B': -5}, [account('bob', -5), -5 < 0])
step(account('bob', -5), clause(1), {}, [])
step(-5 < 0, 'builtin', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', 'ok', 3)
condition('C4', 'coverage', 'ok', 3)
condition('C5', 're_decision', 'ok', 1)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 4)
steps(3)
verified(2)
recomputed(1)
composed(0)
trusted(0)
claims(1)
verdict('checked')

=== a report's variables are lettered in order of appearance
spec: 12
args: --check-proof proof.py --goal "p(X, Y)" program.py
exit: 2
--- program.py
from peye import *
--- proof.py
p(Zebra, Aardvark)
--- stdout
condition('C1', 'resolution', 'ok', 0)
condition('C2', 'well_founded', 'ok', 0)
condition('C3', 'justification', 'ok', 0)
condition('C4', 'coverage', failed(1), 1)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 1)
failure('C4', p(A, B), …)
steps(0)
verified(0)
recomputed(0)
composed(0)
trusted(0)
claims(1)
verdict(failed(1))

=== a report as JSON
spec: 12, 14
args: --json --check-proof proof.py --goal "p(X)" program.py
--- program.py
from peye import *
fact(p('a'))
--- proof.py
p('a')

step(p('a'), clause(1), {}, [])
--- stdout json
{"valid": true, "steps": 1, "claims": 1, "verified": 1, "redecided": 0, "composed": 0, "uses": 0,
 "trusted": [], "failures": [],
 "conditions": [{"id": "C1", "name": "resolution", "covered": 1, "failed": 0},
                {"id": "C2", "name": "well_founded", "covered": 1, "failed": 0},
                {"id": "C3", "name": "justification", "covered": 1, "failed": 0},
                {"id": "C4", "name": "coverage", "covered": 1, "failed": 0},
                {"id": "C5", "name": "re_decision", "covered": 0, "failed": 0},
                {"id": "C6", "name": "boundary_consistency", "covered": 0, "failed": 0},
                {"id": "C7", "name": "relevance", "covered": 2, "failed": 0}]}

=== a failing report as JSON
spec: 12, 14
args: --json --check-proof proof.py --goal "is_(7, 2 + 3)" program.py
exit: 2
--- program.py
from peye import *
--- proof.py
is_(7, 2 + 3)

step(is_(7, 2 + 3), 'builtin', {}, [])
--- stdout json
{"valid": false, "steps": 1, "claims": 1, "verified": 0, "redecided": 0, "composed": 0, "uses": 0,
 "trusted": [],
 "failures": [{"condition": "C5", "detail": "primitive disagrees: is_(7, 2 + 3)", "conclusion": "is_(7, 2 + 3)"}],
 "conditions": [{"id": "C1", "name": "resolution", "covered": 0, "failed": 0},
                {"id": "C2", "name": "well_founded", "covered": 1, "failed": 0},
                {"id": "C3", "name": "justification", "covered": 1, "failed": 0},
                {"id": "C4", "name": "coverage", "covered": 1, "failed": 0},
                {"id": "C5", "name": "re_decision", "covered": 0, "failed": 1},
                {"id": "C6", "name": "boundary_consistency", "covered": 0, "failed": 0},
                {"id": "C7", "name": "relevance", "covered": 2, "failed": 0}]}

=== a generated proof checks
spec: 7.7, 11
args: --check-proof proof.py program.py
--- program.py
from peye import *
fact(n(1), n(3))
implies(n(X) & (X > 2), big(X))
--- proof.py
big(3)

clause(2, fact(n(3)))
clause(3, implies(n(X) & (X > 2), big(X)))

step(big(3), clause(3), {'X': 3}, [n(3), 3 > 2])
step(n(3), clause(2), {}, [])
step(3 > 2, 'builtin', {}, [])
--- stdout
condition('C1', 'resolution', 'ok', 2)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', 'ok', 3)
condition('C4', 'coverage', 'ok', 3)
condition('C5', 're_decision', 'ok', 1)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 4)
steps(3)
verified(2)
recomputed(1)
composed(0)
trusted(0)
claims(1)
verdict('checked')