feat(protocol): let a proof end a program that writes, evaluated on the snapshot its writes committed against - #272

auth: authenticated default

=== setup kg
>>> .kg create pinned_live
>>> 
<<< {
 "type": "result",
 "rows": [
  [
   "Knowledge graph 'pinned_live' created."
  ],
  [
   "Switched to knowledge graph: pinned_live"
  ]
 ],
 "errors": []
}

=== use kg
>>> .kg use pinned_live
<<< {
 "type": "result",
 "rows": [
  [
   "Switched to knowledge graph: pinned_live"
  ]
 ],
 "errors": []
}

=== pack
>>> +il_txn(t: string)
>>> +il_ghost(n: int)
>>> +attempt(s: string, t: string, id: string)
>>> +decision(id: string, s: string, t: string)
>>> +il_ghost[(0)]
>>> +need[("s1", "carrier_check"), ("s1", "say_eta")]
>>> +tool_ready[("carrier_check"), ("say_eta")]
>>> +eligible(S, T) <- need(S, T), tool_ready(T), !attempt(S, T, _)
<<< {
 "type": "result",
 "rows": [
  [
   "Schema for 'il_txn' registered with 1 columns (persistent)"
  ],
  [
   "Schema for 'il_ghost' registered with 1 columns (persistent)"
  ],
  [
   "Schema for 'attempt' registered with 3 columns (persistent)"
  ],
  [
   "Schema for 'decision' registered with 3 columns (persistent)"
  ],
  [
   "Inserted 1 fact(s) into 'il_ghost'."
  ],
  [
   "Inserted 2 fact(s) into 'need'."
  ],
  [
   "Inserted 2 fact(s) into 'tool_ready'."
  ],
  [
   "Rule 'eligible' registered."
  ]
 ],
 "errors": [],
 "statements": [
  {
   "index": 4,
   "kind": "insert",
   "inserted": 1,
   "deleted": 0
  },
  {
   "index": 5,
   "kind": "insert",
   "inserted": 2,
   "deleted": 0
  },
  {
   "index": 6,
   "kind": "insert",
   "inserted": 2,
   "deleted": 0
  }
 ]
}

=== S1 token-form claim wins, proof of the guard state
>>> -il_txn(""), +il_txn("t-1") <- eligible(S, T), S = "s1", T = "carrier_check"
>>> -il_ghost(0), +attempt("s1", "carrier_check", "t-1") <- il_txn("t-1")
>>> -il_ghost(0), +decision("t-1", "s1", "carrier_check") <- il_txn("t-1")
>>> -il_txn(T) <- il_txn(T), T = "t-1"
>>> .why ?eligible("s1", "carrier_check")
<<< {
 "type": "result",
 "rows": [
  [
   "Update: 0 deleted, 1 inserted."
  ],
  [
   "Update: 1 deleted, 1 inserted."
  ],
  [
   "Update: 0 deleted, 1 inserted."
  ],
  [
   "Conditional delete: 1 fact(s) deleted from 'il_txn'."
  ]
 ],
 "errors": [],
 "statements": [
  {
   "index": 0,
   "kind": "update",
   "inserted": 1,
   "deleted": 0
  },
  {
   "index": 1,
   "kind": "update",
   "inserted": 1,
   "deleted": 1
  },
  {
   "index": 2,
   "kind": "update",
   "inserted": 1,
   "deleted": 0
  },
  {
   "index": 3,
   "kind": "delete",
   "inserted": 0,
   "deleted": 1
  }
 ],
 "proof_trees": [
  {
   "query": "__query__(_c0, _c1) <- eligible(_c0, _c1), _c0 = \"s1\", _c1 = \"carrier_check\"",
   "revision": 6,
   "roots": [
    "eligible([\"s1\",\"carrier_check\"])"
   ],
   "leaves": [
    "fact:need",
    "fact:tool_ready",
    "negation:attempt"
   ]
  }
 ]
}

=== S1b state after claim
>>> ?attempt(S, T, Id)
>>> 
<<< {
 "type": "result",
 "rows": [
  [
   "s1",
   "carrier_check",
   "t-1"
  ]
 ],
 "errors": []
}

=== S2 same claim again is refused, empty proof
>>> -il_txn(""), +il_txn("t-2") <- eligible(S, T), S = "s1", T = "carrier_check"
>>> -il_ghost(0), +attempt("s1", "carrier_check", "t-2") <- il_txn("t-2")
>>> -il_ghost(0), +decision("t-2", "s1", "carrier_check") <- il_txn("t-2")
>>> -il_txn(T) <- il_txn(T), T = "t-2"
>>> .why ?eligible("s1", "carrier_check")
<<< {
 "type": "result",
 "rows": [
  [
   "Update: 0 deleted, 0 inserted."
  ],
  [
   "Update: 0 deleted, 0 inserted."
  ],
  [
   "Update: 0 deleted, 0 inserted."
  ],
  [
   "Conditional delete: 0 fact(s) deleted from 'il_txn'."
  ]
 ],
 "errors": [],
 "statements": [
  {
   "index": 0,
   "kind": "update",
   "inserted": 0,
   "deleted": 0
  },
  {
   "index": 1,
   "kind": "update",
   "inserted": 0,
   "deleted": 0
  },
  {
   "index": 2,
   "kind": "update",
   "inserted": 0,
   "deleted": 0
  },
  {
   "index": 3,
   "kind": "delete",
   "inserted": 0,
   "deleted": 0
  }
 ],
 "proof_trees": []
}

=== S2b only one attempt/decision
>>> ?decision(Id, S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "t-1",
   "s1",
   "carrier_check"
  ]
 ],
 "errors": []
}

=== S3 standalone .why after the claim (the old shim problem)
>>> .why ?eligible("s1", "carrier_check")
<<< {
 "type": "result",
 "rows": [],
 "errors": []
}

=== S4a proof not last -> unsupported
>>> .why ?eligible(S, T)
>>> +need("s9", "x")
<<< {
 "type": "result",
 "rows": [
  [
   "'.why ?eligible(S, T)' must be the last statement of a program that changes facts, rules or schemas: a proof there explains the state the program's writes committed against. Nothing was applied."
  ]
 ],
 "errors": [
  {
   "index": 0,
   "code": "unsupported",
   "message": "'.why ?eligible(S, T)' must be the last statement of a program that changes facts, rules or schemas: a proof there explains the state the program's writes committed against. Nothing was applied."
  }
 ]
}

=== S4b query + proof -> unsupported
>>> +need("s9", "x")
>>> ?need(S, T)
>>> .why ?eligible(S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "'?need(S, T)' cannot run in a program that changes facts, rules or schemas and ends with a proof: the program replies with its statements' messages and the proof. Nothing was applied; send the query in a separate request."
  ]
 ],
 "errors": [
  {
   "index": 1,
   "code": "unsupported",
   "message": "'?need(S, T)' cannot run in a program that changes facts, rules or schemas and ends with a proof: the program replies with its statements' messages and the proof. Nothing was applied; send the query in a separate request."
  }
 ]
}

=== S4c .rule query + proof -> unsupported (review fix)
>>> +need("s9", "x")
>>> .rule eligible
>>> .why ?eligible(S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "'.rule eligible' cannot run in a program that changes facts, rules or schemas and ends with a proof: the program replies with its statements' messages and the proof. Nothing was applied; send the query in a separate request."
  ]
 ],
 "errors": [
  {
   "index": 1,
   "code": "unsupported",
   "message": "'.rule eligible' cannot run in a program that changes facts, rules or schemas and ends with a proof: the program replies with its statements' messages and the proof. Nothing was applied; send the query in a separate request."
  }
 ]
}

=== S4d outside command + proof -> unsupported
>>> +need("s9", "x")
>>> .rel
>>> .why ?eligible(S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "'.rel' cannot run in a program that changes facts, rules or schemas: those changes commit together as one transaction, and this command cannot join it. Nothing was applied; send the command in a separate request."
  ]
 ],
 "errors": [
  {
   "index": 1,
   "code": "unsupported",
   "message": "'.rel' cannot run in a program that changes facts, rules or schemas: those changes commit together as one transaction, and this command cannot join it. Nothing was applied; send the command in a separate request."
  }
 ]
}

=== S4e nothing applied by rejected programs
>>> ?need("s9", T)
<<< {
 "type": "result",
 "rows": [],
 "errors": []
}

=== S5 failed proof keeps writes
>>> +need("s1", "escalate")
>>> .why ?need(S, T), X > 1
<<< {
 "type": "result",
 "rows": [
  [
   "Inserted 1 fact(s) into 'need'."
  ],
  [
   "Why error: Query execution failed: Unsafe rule: Atom { relation: \"__query__\", args: [Variable(\"S\"), Variable(\"T\"), Variable(\"X\")] }. Variables [\"X\"] in head do not appear in positive body atoms."
  ]
 ],
 "errors": [
  {
   "index": 1,
   "code": "validation",
   "message": "Why error: Query execution failed: Unsafe rule: Atom { relation: \"__query__\", args: [Variable(\"S\"), Variable(\"T\"), Variable(\"X\")] }. Variables [\"X\"] in head do not appear in positive body atoms."
  }
 ],
 "statements": [
  {
   "index": 0,
   "kind": "insert",
   "inserted": 1,
   "deleted": 0
  }
 ]
}

=== S5b write committed
>>> ?need("s1", "escalate")
<<< {
 "type": "result",
 "rows": [
  [
   "s1",
   "escalate"
  ]
 ],
 "errors": []
}

=== S6 .why full ends a write
>>> +tool_ready("escalate")
>>> .why full ?eligible(S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "Inserted 1 fact(s) into 'tool_ready'."
  ]
 ],
 "errors": [],
 "statements": [
  {
   "index": 0,
   "kind": "insert",
   "inserted": 1,
   "deleted": 0
  }
 ],
 "proof_trees": [
  {
   "query": "__query__(S, T) <- eligible(S, T)",
   "revision": 8,
   "roots": [
    "eligible([\"s1\",\"say_eta\"])"
   ],
   "leaves": [
    "fact:need",
    "fact:tool_ready",
    "negation:attempt"
   ]
  }
 ]
}

=== S6b .why_not ends a write, sees pre-write state
>>> +need("s2", "say_eta")
>>> .why_not eligible("s2", "say_eta")
<<< {
 "type": "result",
 "rows": [
  [
   "Inserted 1 fact(s) into 'need'."
  ]
 ],
 "errors": [],
 "statements": [
  {
   "index": 0,
   "kind": "insert",
   "inserted": 1,
   "deleted": 0
  }
 ],
 "proof_trees": [
  {
   "query": ".why_not eligible(\"s2\", \"say_eta\")",
   "revision": 9,
   "roots": [
    "eligible([\"s2\",\"say_eta\"])"
   ],
   "leaves": [
    "why_not:eligible",
    "why_not:eligible",
    "why_not:need"
   ]
  }
 ]
}

=== S6c .why_not afterwards
>>> .why_not eligible("s2", "say_eta")
<<< {
 "type": "result",
 "rows": [
  [
   "eligible(\"s2\", \"say_eta\") was NOT derived:"
  ],
  [
   ""
  ],
  [
   "  Rule: eligible (clause 0)"
  ],
  [
   "    eligible(S, T) <- need(S, T), tool_ready(T), !attempt(S, T, _)"
  ]
 ],
 "errors": [],
 "proof_trees": [
  {
   "query": ".why_not eligible(\"s2\", \"say_eta\")",
   "revision": 10,
   "roots": [
    "eligible([\"s2\",\"say_eta\"])"
   ],
   "leaves": [
    "fact:need",
    "fact:tool_ready",
    "why_not:eligible",
    "why_not:eligible"
   ]
  }
 ]
}

=== S7 failed program returns no proof and rolls back
>>> +need("s3", "say_eta")
>>> +attempt(1, 2)
>>> .why ?eligible(S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "Insert rejected for 'attempt': Insert rejected for 'attempt': batch of 1 tuples had type/arity errors (rolled back: none of the program's 2 write statements 0-1 was applied)"
  ]
 ],
 "errors": [
  {
   "index": 1,
   "code": "validation",
   "message": "Insert rejected for 'attempt': Insert rejected for 'attempt': batch of 1 tuples had type/arity errors (rolled back: none of the program's 2 write statements 0-1 was applied)"
  }
 ]
}

=== S7b rolled back
>>> ?need("s3", T)
<<< {
 "type": "result",
 "rows": [],
 "errors": []
}

=== S8 no-write program: .why still standalone
>>> ?eligible(S, T)
>>> .why ?eligible(S, T)
<<< {
 "type": "result",
 "rows": [
  [
   "s1",
   "escalate"
  ],
  [
   "s1",
   "say_eta"
  ],
  [
   "s2",
   "say_eta"
  ]
 ],
 "errors": [],
 "proof_trees": [
  {
   "query": "__query__(S, T) <- eligible(S, T)",
   "revision": 10,
   "roots": [
    "eligible([\"s1\",\"escalate\"])"
   ],
   "leaves": [
    "fact:need",
    "fact:tool_ready",
    "negation:attempt"
   ]
  },
  {
   "query": "__query__(S, T) <- eligible(S, T)",
   "revision": 10,
   "roots": [
    "eligible([\"s1\",\"say_eta\"])"
   ],
   "leaves": [
    "fact:need",
    "fact:tool_ready",
    "negation:attempt"
   ]
  },
  {
   "query": "__query__(S, T) <- eligible(S, T)",
   "revision": 10,
   "roots": [
    "eligible([\"s2\",\"say_eta\"])"
   ],
   "leaves": [
    "fact:need",
    "fact:tool_ready",
    "negation:attempt"
   ]
  }
 ]
}

// Drives a live inputlayer-server over its WebSocket API.
const url = process.argv[2];
const ws = new WebSocket(url);
let n = 0; const pending = new Map();
ws.onmessage = (ev) => { const m = JSON.parse(ev.data); if (m.id && pending.has(m.id)) { pending.get(m.id)(m); pending.delete(m.id); } };
const send = (o) => new Promise((res) => { const id = String(++n); pending.set(id, res); ws.send(JSON.stringify({ ...o, id })); });
const exec = async (label, program) => {
  const r = await send({ type: 'execute', program });
  const brief = { type: r.type, code: r.code, message: r.message, rows: r.rows, errors: r.errors, statements: r.statements,
    proof_trees: r.proof_trees?.map(t => ({ query: t.query, revision: t.revision,
      roots: t.roots?.map(id => { const c = t.nodes[id].conclusion; return `${c.pred}(${JSON.stringify(c.args)})`; }),
      leaves: Object.values(t.nodes).filter(x => x.kind !== 'rule' && x.kind !== 'Rule').map(x => `${x.kind}:${x.conclusion.pred}`).sort() })) };
  console.log(`\n=== ${label}\n>>> ${program.replace(/\n/g, '\n>>> ')}\n<<< ${JSON.stringify(brief, null, 1)}`);
  return r;
};
await new Promise(r => ws.onopen = r);
const auth = await send({ type: 'login', username: 'admin', password: 'testpass-123' });
console.log('auth:', auth.type, auth.knowledge_graph);
await exec('setup kg', '.kg create pinned_live\n');
await exec('use kg', '.kg use pinned_live');
await exec('pack', `+il_txn(t: string)
+il_ghost(n: int)
+attempt(s: string, t: string, id: string)
+decision(id: string, s: string, t: string)
+il_ghost[(0)]
+need[("s1", "carrier_check"), ("s1", "say_eta")]
+tool_ready[("carrier_check"), ("say_eta")]
+eligible(S, T) <- need(S, T), tool_ready(T), !attempt(S, T, _)`);
const decide = (tok, t) => `-il_txn(""), +il_txn("${tok}") <- eligible(S, T), S = "s1", T = "${t}"
-il_ghost(0), +attempt("s1", "${t}", "${tok}") <- il_txn("${tok}")
-il_ghost(0), +decision("${tok}", "s1", "${t}") <- il_txn("${tok}")
-il_txn(T) <- il_txn(T), T = "${tok}"
.why ?eligible("s1", "${t}")`;
await exec('S1 token-form claim wins, proof of the guard state', decide('t-1', 'carrier_check'));
await exec('S1b state after claim', '?attempt(S, T, Id)\n');
await exec('S2 same claim again is refused, empty proof', decide('t-2', 'carrier_check'));
await exec('S2b only one attempt/decision', '?decision(Id, S, T)');
await exec('S3 standalone .why after the claim (the old shim problem)', '.why ?eligible("s1", "carrier_check")');
await exec('S4a proof not last -> unsupported', '.why ?eligible(S, T)\n+need("s9", "x")');
await exec('S4b query + proof -> unsupported', '+need("s9", "x")\n?need(S, T)\n.why ?eligible(S, T)');
await exec('S4c .rule query + proof -> unsupported (review fix)', '+need("s9", "x")\n.rule eligible\n.why ?eligible(S, T)');
await exec('S4d outside command + proof -> unsupported', '+need("s9", "x")\n.rel\n.why ?eligible(S, T)');
await exec('S4e nothing applied by rejected programs', '?need("s9", T)');
await exec('S5 failed proof keeps writes', '+need("s1", "escalate")\n.why ?need(S, T), X > 1');
await exec('S5b write committed', '?need("s1", "escalate")');
await exec('S6 .why full ends a write', '+tool_ready("escalate")\n.why full ?eligible(S, T)');
await exec('S6b .why_not ends a write, sees pre-write state', '+need("s2", "say_eta")\n.why_not eligible("s2", "say_eta")');
await exec('S6c .why_not afterwards', '.why_not eligible("s2", "say_eta")');
await exec('S7 failed program returns no proof and rolls back', '+need("s3", "say_eta")\n+attempt(1, 2)\n.why ?eligible(S, T)');
await exec('S7b rolled back', '?need("s3", T)');
await exec('S8 no-write program: .why still standalone', '?eligible(S, T)\n.why ?eligible(S, T)');
ws.close();

test protocol::handler::program_boundary::tests::a_proof_in_a_program_that_writes_must_end_it ... ok
test protocol::handler::program_boundary::tests::programs_without_writes_are_not_checked ... ok
test protocol::handler::program_boundary::tests::a_program_that_writes_holds_a_query_or_a_proof_not_both ... ok
test protocol::handler::program_boundary::tests::a_proof_may_end_a_program_that_writes ... ok
test protocol::handler::program_boundary::tests::outside_commands_cannot_share_a_program_with_writes ... ok
test protocol::handler::program_boundary::tests::writes_join_with_request_local_statements ... ok
test protocol::handler::pinned_proof_tests::a_proof_that_does_not_end_the_program_rejects_it ... ok
test protocol::handler::pinned_proof_tests::a_failed_program_returns_no_proof ... ok
test protocol::handler::pinned_proof_tests::a_failed_proof_fails_its_statement_and_keeps_the_writes ... ok
test protocol::handler::pinned_proof_tests::the_documented_example_runs ... ok
test protocol::handler::pinned_proof_tests::a_won_claim_returns_the_proof_of_the_state_its_guard_passed_on ... ok
test protocol::handler::pinned_proof_tests::why_full_and_why_not_can_end_a_program_that_writes ... ok
test protocol::handler::pinned_proof_tests::writes_after_the_commit_do_not_change_the_proof ... ok
test protocol::handler::pinned_proof_tests::a_refused_claim_returns_an_empty_proof ... ok
test protocol::handler::pinned_proof_tests::the_proof_revision_is_the_snapshot_before_the_program_changes ... ok
test protocol::handler::pinned_proof_tests::the_proof_follows_the_guard_through_a_restage ... ok
test protocol::handler::proof_snapshot_tests::why_not_explains_the_captured_snapshot_despite_concurrent_writes ... ok
test protocol::handler::proof_snapshot_tests::why_explains_the_captured_snapshot_despite_concurrent_writes ... ok
test result: ok. 18 passed; 0 failed; 0 ignored; 0 measured; 3029 filtered out; finished in 0.44s
test a_decision_returns_the_proof_of_the_candidate_it_claimed ... ok
test racing_decisions_one_wins_and_only_the_winner_has_a_proof ... ok
test the_proof_rejects_a_program_it_cannot_end_and_survives_restart ... ok
test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.11s