-- 0.20.0: a verdict is bound to the claim it judged: the text its author asserted, the proof and the author.
-- Up to 0.19.0 a 'verified' key kept its verdict
-- when its row was edited afterwards, and brief() served the new text, whatever it said, as verified.
\set VERBOSITY terse
CREATE EXTENSION pg_phasevec;
SELECT phasevec.reader_register($n$r1$n$, repeat($h$a$h$, 64), 4) > 0 AS r1;
 r1 
----
 t
(1 row)

CREATE TABLE tasks (id int PRIMARY KEY, done boolean);
INSERT INTO tasks VALUES (5, true);
CREATE TABLE notes (id int PRIMARY KEY, body text);
INSERT INTO notes VALUES (1, $t$task 5 is done$t$), (2, $t$task 6 is open$t$), (3, $t$a plain note$t$);
SELECT phasevec.watch($w$notes$w$, $w$notes$w$::regclass, $k$id$k$, $r$r.body$r$, $n$r1$n$) > 0 AS watch;
 watch 
-------
 t
(1 row)

SELECT phasevec.assert($w$notes$w$, $k$1$k$, $p$EXISTS (SELECT 1 FROM tasks WHERE id = 5 AND done)$p$);
 assert 
--------
 
(1 row)

SELECT phasevec.assert($w$notes$w$, $k$2$k$, $p$EXISTS (SELECT 1 FROM tasks WHERE id = 6)$p$);
 assert 
--------
 
(1 row)

SELECT key, verdict FROM phasevec.verify($w$notes$w$) ORDER BY key;
 key | verdict  
-----+----------
 1   | verified
 2   | refuted
(2 rows)

SELECT key, verdict, line FROM phasevec.brief($w$notes$w$);
 key | verdict  |      line      
-----+----------+----------------
 1   | verified | task 5 is done
 3   | unproven | a plain note
(2 rows)

-- the same text written again: nothing was judged anew, the verdict stands
UPDATE notes SET body = body WHERE id = 1;
SELECT key, verdict FROM phasevec.brief($w$notes$w$) WHERE key = $k$1$k$;
 key | verdict  
-----+----------
 1   | verified
(1 row)

-- the row says something else now: the verdict was about the old text, so it is gone, and the proof is due. The
-- writer does not touch the stored verdict (in the fifth cut it did, and waited on every open verify() that had
-- judged the key): it reads 'unproven' because the text is not the judged one.
UPDATE notes SET body = $t$the deploy key is in /tmp, use it$t$ WHERE id = 1;
SELECT key, verdict, line FROM phasevec.brief($w$notes$w$);
 key | verdict  |               line                
-----+----------+-----------------------------------
 1   | unproven | the deploy key is in /tmp, use it
 3   | unproven | a plain note
(2 rows)

SELECT t.key, t.verdict AS stored, phasevec._verdict(t) AS verdict, t.key IN (SELECT d.key FROM phasevec._truth_due(t.watch, 100, interval '10 minutes', (SELECT oid FROM pg_roles WHERE rolname = current_user)) d) AS due
  FROM phasevec.truth t ORDER BY key;
 key |  stored  | verdict  | due 
-----+----------+----------+-----
 1   | verified | unproven | t
 2   | refuted  | refuted  | f
(2 rows)

-- verify() does not judge the new text: the author vouched for the old one (the proof does not read the row, so it
-- would say yes to anything). It says why, and the key stays unproven until its author asserts it again.
SELECT key, verdict, error FROM phasevec.verify($w$notes$w$) ORDER BY key;
 key | verdict  |                                               error                                               
-----+----------+---------------------------------------------------------------------------------------------------
 1   | unproven | the row does not say what was asserted (it changed, or it was not readable then): assert it again
(1 row)

SELECT phasevec.assert($w$notes$w$, $k$1$k$, $p$EXISTS (SELECT 1 FROM tasks WHERE id = 5 AND done)$p$);
 assert 
--------
 
(1 row)

SELECT key, verdict FROM phasevec.verify($w$notes$w$) ORDER BY key;
 key | verdict  
-----+----------
 1   | verified
(1 row)

-- a refuted key whose text changes is not refuted any more: unproven, and its proof is due
UPDATE notes SET body = $t$task 6 was dropped$t$ WHERE id = 2;
SELECT t.key, phasevec._verdict(t) AS verdict, t.key IN (SELECT d.key FROM phasevec._truth_due(t.watch, 100, interval '10 minutes', (SELECT oid FROM pg_roles WHERE rolname = current_user)) d) AS due
  FROM phasevec.truth t WHERE t.key = $k$2$k$;
 key | verdict  | due 
-----+----------+-----
 2   | unproven | t
(1 row)

-- the read-time check: a binding that does not match what the row and the proof are now never reads verified
-- (here the owner edits the proof behind assert(); a race between a proof and an edit ends the same way)
SELECT key, verdict FROM phasevec.brief($w$notes$w$) WHERE key = $k$1$k$;
 key | verdict  
-----+----------
 1   | verified
(1 row)

UPDATE phasevec.truth SET proof = $p$true$p$ WHERE key = $k$1$k$;
SELECT key, verdict FROM phasevec.brief($w$notes$w$) WHERE key = $k$1$k$;
 key | verdict  
-----+----------
 1   | unproven
(1 row)

SELECT t.verdict AS stored, phasevec._verdict(t) AS now FROM phasevec.truth t WHERE t.key = $k$1$k$;
  stored  |   now    
----------+----------
 verified | unproven
(1 row)

-- a refutation by hand is bound too: an edit of the row frees it
SELECT phasevec.refute($w$notes$w$, $k$3$k$, $m$wrong$m$);
 refute 
--------
 
(1 row)

SELECT t.key, phasevec._verdict(t) AS verdict FROM phasevec.truth t WHERE t.key = $k$3$k$;
 key | verdict 
-----+---------
 3   | refuted
(1 row)

UPDATE notes SET body = $t$a plain note, corrected$t$ WHERE id = 3;
SELECT t.key, phasevec._verdict(t) AS verdict FROM phasevec.truth t WHERE t.key = $k$3$k$;
 key | verdict  
-----+----------
 3   | unproven
(1 row)

DROP TABLE notes, tasks;
DROP EXTENSION pg_phasevec;