include "bufio.m";
include "sexprs.m";
include "spki.m";

sexprs := load Sexprs Sexprs->PATH;
Sexp: import sexprs;

spki := load SPKI SPKI->PATH;
Name, Seqel, Subject, Valid: import spki;

verifier := load Verifier Verifier->PATH;

Speaksfor: adt {
   subject:   ref Subject;
   name:      ref Name;
   regarding: ref Sexp;
   valid:     ref Valid;
};

init:   fn();
verify: fn(seq: list of ref Seqel):
          (ref Speaksfor, list of ref Seqel, string);

Init must be called before any other operation of the module.

A Speaksfor value represents a claim that a given subject entity speaks for (on behalf of) a given name regarding a set of statements, with validity optionally limited to a given period. That is, when during the agreed time, subject makes a statement that is in the agreed set, it is treated as if name had said it directly. The set of statements is defined by a SPKI `tag' expression, represented as an S-expression. In particular, the (tag (*)) means that subject speaks for name about everything. A claim can be taken as true if supported by acceptable evidence, for instance a collection of signed certificates.

Verify does the actual verification of a sequence seq of SPKI certificates, signatures and operations that makes and supports a claim that an entity speaks for another. It returns a tuple (claim, badel, err). On success, claim refers to a Speaksfor value that summaries the statement verified by the sequence. On failure, claim is nil, badel is a list of sequence elements headed by the first element of seq that failed verification, and err is the reason it failed.