What the Lean verification establishes. The Lean library puts together the following items.
modelNextToken of the model being served, as a function from weights and a list of tokens to the next token (§2, Appendix C).flashProve for the claim that given output tokens are this model's output on a given prompt, at committed weights. It is formalized as a holographic IOP (§3, Appendix A).compile (flashProve setup) of (2) in the random oracle model (§4).blake2bHash, the hash function on bit strings built from it (Appendix B).leanVerifier, which the cards call the Lean verifier: the verifier of (3) with blake2bHash in place of the random oracle (its definition is in Final statements). Under the Fiat–Shamir heuristic it inherits the soundness proved in (4).executableVerifier, a Lean function that can be run and is proved to return the verdict of leanVerifier (the theorem executableVerifier_eq_leanVerifier, also in Final statements).Goals. FlashProve's code is cryptographic and was largely written by AI systems. Formal verification is meant to make its security independent of trust in that code. Items (1) to (4) specify the protocol in Lean and prove completeness, soundness and zero knowledge in the random oracle model (the precise forms are under “The statements, at a glance”, below). The following gaps remain.
In particular, a reader who only needs to trust the verifier has to:
Sound (§1) and the theorem sound of (4);executableVerifier_eq_leanVerifier of (7);That executableVerifier is then sound is a conclusion, not a theorem. By the theorem of (7) it returns the verdict of leanVerifier on the files of a public setup, and that leanVerifier is sound rests on the Fiat–Shamir heuristic of (6) and on assumptions listed in §11. The conclusion is about the Lean function executableVerifier; what a run of the command lean-verify adds to it is described in Running the verifier.
Checking the proofs yourself. To check the proofs, go to the directory lean/ of this repository and run lake exe cache get && LEAN_ABORT_ON_PANIC=1 lake build to compile and type-check the library. A build does not fail on an unfinished proof or on an added axiom. For these, and for a second check of every compiled module by Lean's kernel, run python3 -B scripts/check.py afterwards: it rebuilds the library in a scratch copy, replays it in the kernel and verifies that no declaration depends on an axiom other than Lean's standard ones (propext, Classical.choice, Quot.sound). On the machine used for this release (84 cores, 960 GiB of memory) the script took four and a half hours; lean/CHECKING.md gives the steps, the requirements and what a pass shows. For standard guidelines see the chapter “Validating a Lean Proof” of the Lean reference manual (lean-lang.org/doc/reference/latest/ValidatingProofs/). Lean's kernel is trusted, not proved correct, and the pinned version, 4.29.1, predates fixes for publicly known soundness bugs in the kernel (§11).
Further down
Six theorems (the repository's other pages call them the six lines) and one definition, the Lean verifier, about one argument system, compile (flashProve setup). In each of them:
setup is a public setup (PublicSetup): three public files that meet four conditions (see A public setup below and FilesInUse in §4.4);flashProve setup is the input of compile for these files.Both are described on cards in the next section.
The six theorems:
setup (PublicSetup)finalSoundnessError q, about q / 2^124 + 2^-101finalSoundnessError q, about q / 2^124 + 2^-101, is a bound on the soundness error, not a security level.Soundness requires only FilesTaken (§4.4) and holds for every choice of honest provers and settings. This more general theorem has no card on this page (Johnson/Face/FinalSoundProof.lean:24; see the remark in §1); sound is proved by applying it to the setup's files. The public setup requires more because of the other theorems.
a public setup setup (PublicSetup)
soundness and binding, with the same extractor and bound for both: the soundness clause also holds with error finalBindingError q, and the commitment cannot be opened to weights other than the extractor's, except with probability finalBindingError q, about q / 2^124 + 2^-100, where q bounds the total number of hash queries of whoever made the commitment and of the prover (in the soundness clause) or the opener (in the binding clause)
coinBound, binding would say almost nothing: at 0 there is only one choice of coins. For the honest provers and settings of the six theorems, the bound excludes none of the committer's choices of coins: coinBound + 1 is the committer's whole range, and for the files of a public setup every pair of an encoding randomness of the first table and a member of the list of its salts is given by a number at most coinBound (a theorem: AtFullSide/Face/FinalBindingOpeningsAtHonestProversAndSettingsOf.lean:39). No value is given for coinBound.a public setup setup (PublicSetup)
for all weights, at every request that can be served (CanServe) and whose output tokens are the model's,
the honest proof is rejected with probability at most 2^-40
CanServe, including those where the model has no result, or about outputs that are not the model's.At a request outside CanServe, or whose output is not the model's, the honest prover's reply is the empty proof (refusedHandsOutNoProof).
a public setup setup (PublicSetup)
a bound error, a function of a number of hash queries and a number of replies
it is at most finalZeroKnowledgeError, 2^-154, for up to 2^64 hash queries and 688,127 replies
zero knowledge within this bound on the requests that can be served and whose output tokens are the model's, with its own simulator, which may depend on the public setup and in the experiment is given no part of the weights: only the largest number of proofs, the verifier's hash queries and each request's prompt and output tokens
With refusedHandsOutNoProof it implies zeroKnowledgeAtEveryRequest (§6.3) within the same bound, finalZeroKnowledgeError, where the simulator is given one bit per request: served or refused. Hence, for every well-formed request of its choice, a verifier learns whether the claimed output is the model's result (§6.3).
The error function is existentially quantified, not a named function: the statement says that there is one and that it is at most finalZeroKnowledgeError within the stated limits on queries and replies; ZeroKnowledgeOn takes it as an argument.
a public setup setup (PublicSetup)
every reply that the prover can return
at a refused request (a request is refused if it is ill-formed, if the model has no result on it, or if its result is other tokens)
is the empty proof
That a refusal is justified: an empty proof proves nothing, and a prover can return it for a request that it could serve.
a public setup setup (PublicSetup)
688,127 (finalReplyCount) is at most onlineRunsPerCopy setup, the number of runs of the online IOP that the honest settings assign to one copy
with that many runs, the columns opened by the proofs fit each table's budget (TableBudgetFits)
one run each of the honest sampler of commitment randomness, the honest committer and the honest prover together make at most 2^48 hash queries
The prover does not count replies, so nothing in it enforces the first two.
The theorems on zero knowledge hold for up to 688,127 replies. Each reply, including a refused reply (the empty proof), is counted as one run of the online IOP; the statements contain only the count (the Lean comment says "is one run").
onlineRunsPerCopy is also the numeric literal 688,127, so (1) compares two literals. (2) relates that number to a table: 62 + 688,127 · 64 columns do not exceed a copy's 44,040,191.
(1) and (2) are conditions on numbers used in the proof of zero knowledge, which is why this theorem is one of the six. Copies are described in §6.4.
In the theorems on soundness, binding, completeness and zero knowledge, the hash function is sampled at random. The honest committer and prover are Lean definitions, not programs.
The Lean verifier:
a public setup setup (PublicSetup), a commitment, a prompt, output tokens, a proof
the compiled verifier with each of its hash queries answered by blake2bHash, the hash function on bit strings built from BLAKE2b
As a definition, leanVerifier cannot be run: parts of the verifier's term are defined using the axiom of choice, including the injective encoding of its hash queries. We therefore provide a second, executable verifier written in Lean, executableVerifier, and prove its equality to leanVerifier.
a public setup (PublicSetup), a commitment, a prompt, output tokens and a parsed proof (FormBytes: five files from a parser outside Lean, and further tokens; elsewhere on this page: the proof as submitted)
on the setup's three public files and these inputs, executableVerifier returns a verdict (never none), and it equals that of leanVerifier
setup.files). The command lean-verify does not enforce this: it does not reject public files that specify a policy other than exact match (A public setup).verdictOf. verdictOf parses the claim from the user's files (claimOf) and applies executableVerifier to it (verdictOf_eq_executableVerifier, proved by unfolding definitions). No theorem shows that claimOf implements the file format, and no theorem covers the parser outside Lean or the run itself. The other assumptions of a run are listed in Running the verifier.leanVerifier, executableVerifier or verdictOf is sound at BLAKE2b. Soundness is proved with the hash function sampled at random. That it carries over to leanVerifier at BLAKE2b is the Fiat–Shamir heuristic, an assumption.leanVerifier, executableVerifier also uses the protocol's second, fixed hash function, which is not modelled as a random oracle (The second hash function).executableVerifier (§5) says what "executable" means.A public setup consists of three public files (a parameter file, a layout file and a scale file) that satisfy four conditions (FilesInUse, §4.4):
protocolDataWellFormed, which the verifier also performs: the protocol's data can be built from them without error, no list of rounds is empty, the data for the key and for the proof have the full-size depth, and the sizes lie within fixed limits.The library defines one public setup, storedSetup (§4.4), as a Lean term. No theorem relates it to a file on disk; a program outside Lean compares it with the files of the shipped example.
Three definitions that the theorems use. A fourth, onlineRunsPerCopy, is in §6.4.
Three public files that a user has in addition to the commitment, fixed before the hash function is sampled. They determine the model shape and the instance of the protocol; only the scale file and five numbers of the parameter file (parameters of the normalizations) are free.
files: the parameter file, the layout file and the scale file
readParameters: what reading the files returns
the field inUse requires (FilesInUse, §4.4):
readParametersprotocolDataWellFormed: the protocol's data can be built from them without error, no list of rounds is empty, the data for the key and for the proof have the full-size depth, and the sizes are within fixed limits; the test is treated as a black box on this pageThe files are not the PublicParameters of an argument system (§1), which compile sets to Unit. What the files reveal about the weights (a fitted model's scale file is derived from its weights) is not covered by the theorems on zero knowledge (§6.3).
For some valid choices of the quantization scales, the outputs of the value and up projections are all zero, so no layer changes the residual stream (checked by hand, not proved: the head of Cm/Rel2Idle.lean, on sIdle, to which the comment on weightsAreValid in VerifiableInference/ModelWeights.lean points); for public files that state such settings the theorems say little. A reader has to inspect the scale file.
storedSetup (below) is the only public setup that the library exhibits. That its files form a public setup is a theorem (filesInUse_stored). Its scale file is that of an example with synthetic weights (according to the head comment of Ladder/Stored.lean; no theorem).
Whoever commits writes the scale file.
The input to compile: not a bare interactive oracle proof, but a record that contains the protocol with its layout into hash queries. There is one for each public setup: FlashProve is a family of protocols.
The protocol uses a second hash function, secondHashFunction, a fixed function that is not modelled as a random oracle (§5).
flashProveAtFiles (§4.4) with its three arguments determined by the public setup:
The protocol is a linkable holographic IOP (§3):
Holographic IOPs and their compilation are defined in Fractal, ePrint 2019/1076 (§3).
The honest provers and settings of the six theorems: a single closed term that gives, for every choice of public files and settings:
It contains no committer: compile constructs the honest committer.
It is a definition, not a program: it obtains the model's trace by a non-constructive choice.
The verifier reads none of it.
A black box on this page: it depends on about 16,000 named declarations of this library, of which the page shows about five hundred.
The provers consist of parts (in Lean: senders), one for each step of the protocol. Where a function called by such a part refuses, the part sends a fixed default value and does not stop.
The numbers in these theorems:
finalSoundnessError q = 16 (q + 1 + 2^23) / 2^128 + (q + 2^23 + 3)^2 / 2^256, about q / 2^124 + 2^-101finalBindingError q: about q / 2^124 + 2^-100finalCompletenessError = 2^-40finalZeroKnowledgeError = 2^-154finalVerifierQueries = 2^64finalReplyCount = 688,127honestQueryBudget = 2^48§4.4 specifies whose hash queries q counts.
At the library's stored example of the public files, with no argument setup:
The theorem soundAndBinding at storedSetup, the library's stored example of the three public files (a Lean value not tied to any file on disk): a closed statement, with no parameters.
The library's stored full-size example of the three files (VerifierAndGoals.storedPublicFiles, a Lean value not tied to any file on disk), with what reading it returns, chosen non-constructively. It is not stated here that these are the released files.
The theorem sound at storedSetup.
The theorem completeOnCanServe at storedSetup.
The theorem zeroKnowledgeOnCanServe at storedSetup.
Randomized and deterministic algorithms, queries to the hash function, query logs and probabilities are those of the random oracle model (§8).
a structure of four types and six functions
what a commitment commits to: the weights of one model
the public parameters: a part of the weights that the simulator is given at its start (§6.2), and the function that computes it; anything else that a simulator is given about the weights is a parameter of the statement (§6.3)
the committer's randomness
a proof
the model: a function mapping weights and a list of tokens to the next token, or to nothing if the model has no value on these tokens. It neither queries the hash function nor samples randomness.
the honest committer: it samples its randomness, computes the commitment to the weights under it, publishes the commitment and keeps the randomness
the honest prover: computes a proof from the weights, the committer's randomness, a prompt and output tokens. It may sample randomness and query the hash function.
the verifier: maps a commitment, a prompt, output tokens and a proof to a decision. It is deterministic (DeterministicAlgorithm) and accesses the hash function only through queries.
an argument system, weights, a prompt, output tokens
for every position of the output tokens:
the model's next token, after the prompt followed by the output tokens before that position, is the output token at that position
The empty output has no position to check, so it is the model's output for every prompt and all weights, and when the extractor outputs weights, Sound does not count its acceptance as a failure (§11).
system (the structure above)one function extractor, mapping a commitment and a query log to weights or nothing
committer: a randomized algorithm that makes at most committerQueries queries to the hash function and returns a commitment and a state of arbitrary type, passed to the prover
prover: a randomized algorithm that makes at most proverQueries queries, is given the state and returns a prompt, output tokens and a proof
The hash function is sampled uniformly at random. Then:
the committer runs; queryLog is the list of its queries with their answers
the prover runs
the verifier of system decides
result: what extractor outputs on the commitment and the query log; the prompt; the output tokens; the decision
extractor does not return weights for which the output tokens are the model's on the prompt (IsModelOutput, the card above)Pr[event] ≤ ε(committerQueries + proverQueries)
The theorem sound. For every public setup, the compiled argument system compile (flashProve setup), with the model settings read from the public files, satisfies Sound (above) with the error function finalSoundnessError.
Expanded. There is an extractor such that, for every committer with at most t₁ queries to the random oracle and every prover with at most t₂ queries, the following event has probability at most finalSoundnessError (t₁ + t₂): the verifier accepts output tokens that are not the model's output with the weights that the extractor outputs, given the commitment and the committer's queries.
Remark. The proof of sound uses sound_of_verify_at (Johnson/Goal/Skeleton/SoundOfVerifyAt.lean:69), the soundness theorem for verify, FlashProve's verifier. Its three hypotheses are the fields of FilesTaken. Soundness of compile at flashProveAtFiles follows from sound_of_verify_at for arbitrary honest provers and settings (Johnson/Face/FinalSoundProof.lean:24).
SoundAndBinding has a second clause, on openings of the commitment. An opening of a commitment to given weights is a pair of these weights and commitment randomness on which commit returns that commitment. The clause states the following. For every committer with at most committerQueries queries, and every opener with at most proverQueries queries that is given the committer's state, the probability that the opener outputs an opening of the committer's commitment to weights that the extractor does not output is at most ε(committerQueries + proverQueries).
SoundOpened is a statement without an extractor. SoundAndBinding with error ε implies SoundOpened with error 2 ε. The library proves SoundOpened for the compiled system, for public files that satisfy FilesInUse, with the bound 2 · finalBindingError (finalSoundOpened_value, AtFullSide/Face/FinalBindingAtTheValue.lean; no card on this page).
system (§1)one function extractor, mapping a commitment and a query log to weights or nothing
committer: a randomized algorithm that makes at most committerQueries queries to the hash function and returns a commitment and a state of arbitrary type, passed to the next algorithm
prover: a randomized algorithm that makes at most proverQueries queries, is given the state and returns a prompt, output tokens and a proof
The hash function is sampled uniformly at random. Then:
the committer runs; queryLog is the list of its queries with their answers
the prover runs
the verifier of system decides
result: what extractor outputs on the commitment and the query log; the prompt; the output tokens; the decision
extractor does not return weights for which the output tokens are the model's on the prompt (IsModelOutput, §1)Pr[event] ≤ ε(committerQueries + proverQueries)
opener: a randomized algorithm that makes at most proverQueries queries, is given the state and returns weights and commitment randomness
The hash function is sampled uniformly at random. Then:
the committer runs; its query log is recorded
the opener runs
recomputed: the commitment to the opener's weights under the opener's randomness, as the honest committer computes it
result: the output of extractor; the committer's commitment; the opener's weights; recomputed
recomputed is the committer's commitmentextractor does not output the opener's weightsPr[event] ≤ ε(committerQueries + proverQueries)
The theorem soundAndBinding. For every public setup, compile (flashProve setup) satisfies SoundAndBinding (above) with the error function finalBindingError. The two clauses share one extractor and one committer. In both clauses the bound is finalBindingError (t₁ + t₂), where t₁ bounds the committer's queries to the random oracle and t₂ those of the prover or the opener. For this system, the commitment randomness in an opening is a single number.
systemadversary: one randomized algorithm that makes at most queries queries to the hash function and returns a commitment, weights with commitment randomness, a prompt, output tokens and a proof
The hash function is sampled uniformly at random. Then:
the adversary runs
recomputed: the commitment to the adversary's weights under its randomness, as the honest committer computes it
the verifier of system decides, given the adversary's commitment
result: both commitments; the weights; the prompt; the output tokens; the decision
recomputed is the adversary's commitmentPr[event] ≤ ε(queries)
systemSoundAndBinding system εSound system ε
systemSoundAndBinding system εSoundOpened system, with the bound 2 ε(queries)
The model is a single function, the field nextToken of the argument system (§1).
IsModelOutput (§1).FlashProve's model is defined in Appendix C.
The verifier is compiled from a protocol, a linkable holographic IOP, which does not query the random oracle. Such a protocol has an encoder with a decoder, an out-of-domain sample on each encoding, and three interactive oracle proofs (IOPs): offline, link and online. The general definition follows; FlashProve's protocol is defined in Appendix A.
Credits, among them the paper that this protocol builds on: lean/CREDITS.md. The idea is public: holographic IOPs and their compilation to arguments in the random oracle model are defined in A. Chiesa, D. Ojha, N. Spooner, "Fractal: Post-Quantum and Transparent Recursive Proofs from Holography", ePrint 2019/1076 (eprint.iacr.org/2019/1076). This page's design, and its paragraph "Checking the proofs yourself", are modelled on veil.succinct.xyz (Succinct).
the library's definition of a linkable holographic IOP with an offline IOP and an out-of-domain sample on each encoding (HolographicProtocol), which the compiler takes as input. I: the indices (for FlashProve, what is committed: a matrix computed from the weights by the map indexOf, not the weights themselves). X: the instances (an instance is built from a request and further tokens)
the encoding's length wordLength and its alphabet Symbol: an encoding is an oracle string of wordLength symbols
the encoder's randomness EncodingRandomness (a finite, non-empty set) and the encoder encodeIndex, which maps an index and randomness to an encoding
the out-of-domain seeds OutOfDomainSeed: a finite, non-empty set. The verifier samples a seed after an encoding is sent
the out-of-domain answers OutOfDomainAnswer
the honest answer honestOutOfDomainAnswer, a function of an index, its encoding's randomness and a seed
collision hasCollisionAt: a property of an oracle string and a seed
the decoder decodeIndex: maps an oracle string, a seed and an answer to an index or nothing
the offline IOP offline, on one encoding, meant to show that it decodes; its instance is that encoding's seed and answer
the link IOP link, on two encodings, meant to show that the second decodes to the same index as the first; its instance is both seeds and answers
the batch size maxBatchSize: the number of batch positions in one run of the online IOP. The Lean comments call a batch position a slot and a run a session
the online IOP onlineBatch, for a batch, on one encoding, meant to show that each request's claim holds for the index to which the encoding decodes. An instance: an element of X, the seed and the answer
the honest provers of the offline IOP (honestOfflineProver), the link IOP (honestLinkProver) and the online IOP (honestOnlineBatchProver). Their private input is an index and, for each encoding, its randomness and its seed. For FlashProve, these three fields are set to fixed-message provers (Appendix A), which neither compile nor the verifier uses; the provers in the six theorems are those of honestProversAndSettings (§6.4)
the early part early of an instance: the first query of a Fiat–Shamir chain contains early x for the instance x (recomputeChain, §4.2)
the optional late round late: if present, the query of that round contains the whole instance
the honest provers of the three IOPs of a protocol protocol (HolographicProtocol, the card above)
the offline prover offlineProver. Its private input: the index, the encoding's randomness and the seed
the link prover linkProver. Its private input: the index, and the randomness and the seed of both encodings
the online prover onlineProver, a prover for the IOP of one batch position (loc of onlineBatch). Its private input: the index, the randomness and the seed of the copy (§6.4), and the copy's number
an interactive oracle proof (IOP) with instances of type X and external oracle strings (oracle strings fixed before the first message) specified by E (ExtSpec)
its rounds, in order (Shape)
blinded: a flag for each position of the prover's oracle strings (used in InteractiveOracleProof.dview)
the positions the verifier reads in the external oracle strings, as a function of the instance and the challenges of all rounds
the positions it reads in the prover's oracle strings, as a function of the instance, the challenges of all rounds and the parts of the prover's messages sent in the clear
its decision (accept or reject), as a function of the instance, the external oracle strings and the whole transcript
a batch IOP, for a type X of instances and a specification E of the external oracle strings
the IOP of one batch position
its round marking (RoundSplits): for each round, whether the verifier's message is shared, and how the prover's message splits into a shared part and the part of one batch position
a model in the form that the compiler takes: a type and a function. Sections 3 and 4 use nothing else from a model. For FlashProve: the integer model, printed in Appendix C
the type Weights: what a commitment commits to
the function nextToken, mapping weights and a list of tokens to the next token, or to nothing if the model has no value on these tokens
This section presents the library's compiler. It consists of an inner and an outer compiler (§4.3).
The inner compiler. It is defined for every input of type InnerCompilerInput. Such an input consists of any protocol of type HolographicProtocol (§3) and further data written by hand for that protocol, including the layout of its rounds and openings in hash queries. innerSystem constructs an argument system from such an input, and innerCompiledVerifier is the verifier of that system.
The outer compiler, compile. It is defined for every input of type Compilable. Its verifier performs a test on the public files, parses the proof (the field parse of the proof format, §4.3), performs two readings of the public files (queries to the hash function at strings computed from them), and then runs innerCompiledVerifier. Its committer and prover are constructed from the honest provers in its input. compile is not a compiler for arbitrary IOPs: some fields of its input follow FlashProve's format, namely the two readings of the public files, a test on a first hash block, and the proof format.
The Lean code has three layers, listed here from the bottom up:
The outer compiler constructs the committer and the prover from the honest IOP provers in its input, whereas the inner compiler takes the committer and the prover as fields of its input. As a result, the protocol's structure (§3) and the compiler's input (§4.3) have fields, such as honest provers, that are not used to construct the compiled system; see the remark in §6.4.
The definitions of the compiler's verifier. These definitions are written for any protocol of the library's type (§3).
compiledVerifier first performs a scope test on the public files. It then performs three steps that depend on FlashProve's files and proof format: one parses the proof and two read the public files. It calls innerCompiledVerifier.innerCompiledVerifier runs the next three definitions.Arg.buildInstance rejects if no instance can be built from the request.verifyDigestKey checks that the commitment equals the hash function's value at the encoding of the key in the proof (§4.3).verifyAtKeyRoot builds the whole key from the proof and calls verifyAtFullKey.verifyAtFullKey performs six checks: the number of the copy (§6.4), two seeds, and the verifiers of the three IOPs (offline, link, online).verifyOneProtocol is the verifier of one IOP. Each of the last three checks of verifyAtFullKey calls it. The definitions that it calls have their own cards below it in §4.2.This subsection shows how the compiled algorithms use the single hash function. None of its definitions mentions FlashProve. HashLayout is stated for any protocol of type HolographicProtocol (§3). typedOracleFamily, Check and hashTreeNode are stated for the batch protocol with a leaf body that typedOracleCarrier constructs from such a protocol. OracleCoding is stated for any family of oracles, and Opening for any alphabet.
the file's variables
A hash layout for a protocol and the round markings of its offline and link IOPs specifies how the protocol is mapped to queries to one hash function.
the type of a leaf's body, LeafBody: what a leaf of a hash tree contains in addition to its salt
the query layout queryLayout: how rounds and openings are written into hash queries
the two nested queries that give a table's out-of-domain seed, and the stored copy's number, seedQueries
how out-of-domain answers are written as a list of digests, answerCode
a fixed out-of-domain sample fixedSample, which fills both places for a sample in an online run's first query
the compiler's parameters, compilerParameters
the coding of all separate oracles into the one hash function, oracleCoding (OracleCoding, the next card)
the code of a key, keyCode (a key may have none); where a key has a code, the commitment is the hash function's answer at this code
how the instance is built from a prompt with output tokens and further tokens from the proof, buildInstance
for a family of separate oracles S and blocks of lam bits:
for each oracle, the number of blocks in one answer
for each oracle, a bijection between its answers and sequences of that many blocks
the bit string for an oracle, a query to it and the number of a block of its answer
the decoding of a bit string: the oracle, the query and the number of the block
decoding the bit string for an oracle, a query and a block returns the same three
decoding a bit string and encoding the result returns the same bit string
the type I of indices and the type X of instances
the length lam of a digest; the number K of blocks for a challenge
a protocol L with the three IOPs offline, L.link, onlineBatch
a family of separate oracles (in the Lean names: typed oracles):
their names, one for each purpose (OracleName)
what a query to each of them contains (domOf)
what each of them answers (rngOf)
the file's variables; the structure takes none of them
a Merkle opening, for digests of lam bits and symbols in σ:
the symbol
its salt
its authentication path: a list of digests
the file's variables; of these, the structure uses the types I of indices and X of instances
one opening to verify:
the leaf's hash input: a body and a salt (LeafIn)
the number of the leaf
the authentication path
the root
the depth of the tree
a protocol L; digests of lam bits; K blocks for a challenge
two digests
one query to the oracle node, on the two digests as bit strings
The BCS transformation makes one IOP non-interactive. Each of the prover's oracle strings is replaced by the root of a Merkle tree. Each challenge of the verifier is computed from an answer of a Fiat–Shamir oracle, queried on what was fixed before that challenge.
One definition is used for all three IOPs of the protocol (§3).
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
the two salt lengths; t, selecting one of the three IOPs; the IOP Q
its query layout wq; how its symbols are written into leaves, embS
how parts sent in the clear (embP) and the instance (xin, which may give nothing) are written into queries
how symbols of external oracle strings are written into leaves, embE; the depth depthReq of the Merkle tree over the batch
the list cms of digests, which the chain's queries contain and against whose entries the external oracle strings are opened; an instance x; a proof string π
an algorithm that queries the separate oracles and returns accept or reject
recompute the Fiat–Shamir chain of the proof string (recomputeChainOfProof, the next card, which calls recomputeChain)
it returns nothing: reject
it returns challenges, roots and a last phase:
if the proof string has the strict format (proofHasStrictFormat),
the decision of checkPrunedOpenings
else: reject
verifyOneProtocol does not constrain three things (see "Limits" at the head of its Lean file):
rtreq (any digest) and slot (any number below 2^depthReq)g, whose answer is the batch position's value (recomputeChain)It is not proved that no other change turns an accepted proof string into another accepted one.
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
which of the three IOPs, t; the IOP Q; its query layout wq
how parts sent in the clear (embP) and the instance (xin, which may give nothing) are written into queries
the list cms; an instance x; a proof string π
an algorithm that queries the separate oracles and returns either nothing or the challenges of the rounds of Q, the roots round by round, and the last phase
recomputeChain at t, cms and xin x, at the proof string's salt and at its root of the Merkle tree over the batch,
at all rounds of Q, their round marking and their layout in the hash queries, at embP, from round number 0 and the phase first,
at the proof string's roots and its parts sent in the clear
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
the two lengths of salts: sMT for a leaf, sFS for a chain; the IOP Q
its query layout wq; the depth depthReq of the Merkle tree over the batch; an instance x; a proof string π
the chain's output: challenges ρ, roots rts and a last phase ph
true or false; no query is made
with equality of positions decided as specified by wq (decO, ext.dec), the value is true if and only if all seven of the following hold:
the chain's salt has exactly sFS bits
there are at most as many roots as the chain has taken (RootsOfChain.count)
in each tree over the prover's oracle strings, at every position of a leaf (strictSB): an opening is present only if the tree has a root and the position is read, and its salt has exactly sMT bits
a position is read if the IOP's verifier reads it at x, ρ and the parts sent in the clear (effPlains); the openings are π.opens
at every position that wq lists for the external oracle strings (strictExt): an opening of π.ext is present only if the IOP's verifier reads the position at x and ρ, and its salt has exactly sMT bits
the number of the batch position is below 2^depthReq
the last phase has a batch position's value (slotVal: the chain has passed the first shared round), or the path in the Merkle tree over the batch is empty
it has one, or the bit string rsalt is empty
posAt0, posAtJ, ext.all). They cover every position if the layout is well-formed (WireRB.OKG, WireE.OK), which the theorems that use them assume.rsalt is not tested, and no part of rsalt is compared with the field slot. Nevertheless, rsalt is not free to change: a different rsalt gives a different input of the leaf's hash (by reading; no theorem).For each component of a round, effPlains returns its part sent in the clear, taken from the proof string if the component is sent and from a fixed message otherwise.
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
the IOP Q; its query layout wq
how its symbols are written into leaves, embS; how symbols of external oracle strings are written into leaves, embE
the depth depthReq of the Merkle tree over the batch; the list cms; an instance x; a proof string π
the chain's output: challenges ρ, roots rts and a last phase ph
an algorithm that queries the separate oracles and returns accept or reject
the openings to verify, tree by tree (forestsOf): the trees over the prover's oracle strings, round by round, then the trees over the external oracle strings
it returns a list Fs:
if there are at most wq.nOpen openings to verify,
and each has a path of length equal to its tree's depth, a leaf number below 2^depth (wellFormed), and depth at most wq.maxDepth,
the decision of afterF on Fs and the sibling digests needed by the joint verification, read from the paths (readsF)
else: reject
an opening is missing: reject
Of the digests in the openings' paths, only those that the joint verification needs are used; the others are not checked against anything (§4.2, Merkle paths).
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
the IOP Q; its query layout wq
how its symbols are written into leaves, embS
how symbols of external oracle strings are written into leaves, embE; the list cms; an instance x; a proof string π
from the chain's output: challenges ρ and roots rts
a list of Forest entries (each: openings to verify in trees of one depth), or nothing
with equality of positions decided as specified by wq (decO, ext.dec):
the trees over the prover's oracle strings, round by round (forestsB),
at the positions that the IOP's verifier reads at x, ρ and the parts sent in the clear (effPlains), with the openings π.opens;
the trees over the external oracle strings (forestExt), under the roots cms, at the positions that it reads at x and ρ, with the openings π.ext
both return a list: the first followed by the second
an opening is missing: nothing
forestsOf lists the openings to verify (Check, §4.1), at positions that the IOP's verifier reads:
x, ρ and the parts sent in the clear): at every read position of a leaf, in each tree that has a depth and a root. Nothing more is checked where the depths or the roots end (the component is not sent, or has no further tree)x and ρ): at every read position listed in wq, against the entry of cms that the layout specifies (a default digest if cms has none)Where the layout's pruning flag (pr0, prJ, pr) is set, the opened leaves are verified together; elsewhere each opening is verified along its own path.
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
the IOP Q; its query layout wq; the depth depthReq of the Merkle tree over the batch
an instance x; a proof string π; the chain's output: challenges ρ, roots rts and a last phase ph
the openings Fs to verify, tree by tree; sibling digests s
an algorithm that queries the separate oracles and returns accept or reject
the joint verification of each entry of Fs, with the sibling digests s (runForests);
the check in the Merkle tree over the batch, if the chain has passed the first shared round (reqPart);
accept if both hold and the IOP's verifier accepts (Q.loc.accept) at x, at external oracle strings built from the symbols of π.ext,
and at a transcript made from the proof string and the challenges ρ (mkTr)
afterF accepts if all three hold:
runForests: the leaves are hashed; then, level by level, adjacent siblings are hashed together, and a node without its sibling is hashed with the next sibling digest; every node remaining after depth levels equals the root of its treereqPart: if the last phase contains a batch position's value c, the check in the Merkle tree over the batch (reqCheck) passes: π.path has length depthReq, π.slot is less than 2^depthReq, and hashing from the leaf (the hash of c followed by π.rsalt) up the path gives π.rtreq; if the last phase contains no such value, this condition holdsQ.loc.accept: the IOP verifier's decision on x, on external oracle strings built from the symbols of π.ext (wq.ext.build), and on a transcript built from the proof string (mkTr): the challenges ρ, the parts sent in the clear (effPlains), the opened symbols where there are any and the tree of their position has a root, and the fixed symbol 0 elsewherethe file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
a proof string for the IOP Q; digests have lam bits:
the salt of the Fiat–Shamir chain
the Merkle roots of the prover's oracle strings, in the order in which the chain takes them (recomputeChain)
for each round, the part of the prover's message that is sent in the clear
for each position of the prover's oracle strings: an opening (Opening, §4.1), or nothing
the same for each position of the external oracle strings
the root of the Merkle tree over the batch
the number of this batch position
its authentication path in that tree
a bit string appended to the batch position's value (the answer c of g; see recomputeChain) in the input of its leaf in that tree
the file's variables: types I, X of indices and instances; numbers lam, K; a protocol L
the IOP's tag t; a list of digests cms, contained in the first query and in the first shared round's Fiat–Shamir query
the instance x, or nothing; the chain's salt; the root of the Merkle tree over the batch
the rounds that remain; their round marking (which rounds are shared, and which part of a message belongs to which component);
their layout in the hash queries
how a part sent in the clear is written into a query; the number of the round
the phase that the chain has reached (Phase); the roots that remain; the parts sent in the clear
an algorithm that queries the separate oracles and returns
the challenges of these rounds, the roots round by round, and the last phase; or nothing
no round remains: the current phase
otherwise, for the next round:
its marking and the phase determine the format of its query (actOf; Head: five formats);
the first query contains the early part of the instance
one query, on this batch position's own component: take as many roots as that component has trees;
query the Fiat–Shamir oracle of t
on the round's number, the header (in the round L.late, with the whole instance if the header has a field for it), these roots,
and the component's part sent in the clear;
then the later rounds, from the chaining value in the answer;
this round's challenge is computed from the answer's blocks (w.chal); the roots are recorded for the position's own component
a root is missing, or the component has more than maxRt trees: nothing
one query, on the shared component: the same, without the instance, with that component's trees, roots and part sent in the clear
the first shared round: take the roots of the position's own component, then those of the shared one;
query the oracle g of t: the answer c is the batch position's value;
the query contains the round's number, the chaining value so far and the position's own component
query the Fiat–Shamir oracle on the round's number, the list cms, the root of the Merkle tree over the batch, and the shared component;
then the later rounds, which keep c; this round's challenge as above
a root of the shared component is missing, or it has too many trees: nothing
the same for the position's own component
no format is defined for this marking in this phase: nothing
verifyOneProtocol calls three definitions, each with a card above:
recomputeChainOfProof, which calls recomputeChain on the parts of the proof string;proofHasStrictFormat, which checks the format;checkPrunedOpenings, which checks the openings, performs the check in the tree over the batch, and evaluates the IOP verifier's own decision.checkPrunedOpenings calls forestsOf and afterF, each with a card above. Thus, in the Lean code on this page, a challenge can be traced from what is hashed to its value, then to the positions that the IOP's verifier reads for it (Q.loc.reads, Q.loc.extReads), and into the IOP verifier's decision (Q.loc.accept, at the transcript constructed by mkTr). Of the definitions that these three, forestsOf and afterF call in turn, recomputeChain has a card above. The others (including forestsB, forestExt, runForests, reqPart, mkTr, effPlains, strictSB, strictExt) have no card on this page. The Lean code of these eight is in §9.
Merkle paths. The Merkle path of each opening must have length equal to the depth of its tree. The joint verification reads only those digests in these paths that it needs: where two opened nodes are siblings, it reads the digest of neither. The other digests are not checked against anything. Neither proofHasStrictFormat nor checkPrunedOpenings rejects them, so a typed proof can be altered at these places and still be accepted. This is malleability of the proof string, not a gap in soundness: the bound of sound holds for arbitrary values of these entries (lean/GAPS.md, 14 and 66).
The structure used by verifyOneProtocol. verifyOneProtocol is stated for a smaller structure, which typedOracleCarrier constructs from a protocol of type HolographicProtocol. It keeps the protocol's shapes and types, but not its index or its provers. That structure has no card on this page either.
compile takes one record, Compilable. Its main fields are the public side (the protocol, its hash layout, two readings of the public files, and the model), the honest provers with their settings, and the format in which a proof is written.
It returns an argument system. The verifier of that system depends only on the public side and on the parser of the proof format.
the file's variables
compile takes one argument, input : Compilable, which the Lean code declares in a variable line above the definition.
Compilable), and the protocol is one of the twelve fields of the first, publicSide.The outer compiler, which maps a Compilable to an argument system (ArgumentSystem). It places what FlashProve's files and proof format require before the inner verifier, and builds the honest committer and prover.
nextToken.compiledSide (§6.4), built from the given honest provers.The verifier is compiledVerifier at the public side and the parser: if that test passes, it runs that parser and those two readings, then innerCompiledVerifier (below); if not, it rejects.
The six theorems concern only compile at flashProveAtFiles.
The system has no public parameters.
The committer:
furtherCopies + 1 copies of itThe prover keeps no state:
the file's variables
The compiled verifier. Of compile's input it reads only the public side and the parser.
the parser parse, which computes a typed proof from a prompt, an output and a proof as submitted
a commitment, a prompt, an output and a proof as submitted, form
a deterministic algorithm that returns accept or reject
if the verifier takes these public files at all (filesInScope):
parse the proof as submitted;
the first public reading: the digest of the public files, obtained by querying the hash function;
the second public reading, at that digest;
the decision of innerCompiledVerifier (below) on the commitment, the prompt, the output and the typed proof, for the layout determined by the results of the two readings
else: reject
The next cards show what compiledVerifier runs after its scope test and its three steps, down to the verifier's own checks.
a record r of type InnerCompilerInput: a protocol with its hash layout
the verifier of innerSystem r, the argument system that the library builds from r (its card and those of the intermediate definitions are in the folded section How an input becomes an argument system, below). It builds the instance from the prompt, the output and further tokens in the proof, checks the commitment against the key in the proof, and runs verifyAtKeyRoot (below)
the file's variables
Runs a scheme (A), which queries separate oracles, over the one hash function:
m: OracleCoding, §4.1)the result: a scheme of the same types that queries the one hash function
the committer of A, run in this way by overOne m (OComp.overOne, Rom/Family.lean:69, which has neither a card nor a row in §9)
the prover of A, likewise
the verifier of A, likewise
The inner compiler's input: a protocol with its hash layout. It has twenty fields. The verifier reads thirteen of them, and only the verifier's side of the protocol (innerCompiledVerifier_eq, Johnson/Top/InnerCompiledVerifierSide.lean:79); it reads neither the type of what is committed nor the last six. All fields except the protocol and its two types are written by hand alongside it.
the type of what is committed, Index; the verifier does not read it
the type of what a run of the online IOP proves, Instance
the protocol protocol: three IOPs with the encoder and the decoder of an index
the type of a leaf's body, LeafBody: what a leaf of a hash tree contains in addition to its salt
which rounds of the offline IOP are shared by a batch, offlineRoundSplits
which rounds of the link IOP are shared by a batch, linkRoundSplits
how rounds and openings are written into hash queries, queryLayout
the two nested queries that give a table's out-of-domain seed, and the stored copy's number, seedQueries
how out-of-domain answers are written as a list of digests, answerCode
a fixed out-of-domain sample fixedSample, written in both places for a sample in an online run's first query
the compiler's parameters, compilerParameters
the coding of all separate oracles into the one hash function, oracleCoding
the code of a key, keyCode (a key may have none); where a key has a code, the commitment is the hash function's answer at this code
how the instance is built from a prompt with output tokens and further tokens from the proof, buildInstance
the model, nextToken
the prover's key, the committer and the prover (ProverKey, commit, prove)
the bound on the committer's coins, coinBound
a fall-back proof, fallbackProof
the file's variables
Turns a scheme on instances of type X into a scheme on instances of another type X'. The compiler uses it with a prompt and output tokens as the new instance.
A: the inner scheme, on instances of type Xbuild: maps a new instance and a first part of a proof to an inner instance or nothingaux: maps a new instance to a first part of a proofπ₀: a proof of the inner schemeX'; a proof is a pair of a first part and a proof of the inner schemethat of A
it builds the inner instance from the new instance x' and aux x'
where one is built: aux x', then the proof of A's prover for it
where none is built: aux x', then π₀
it builds the inner instance from x' and the first part of the proof
where one is built: the decision of A's verifier on it and the second part of the proof
and rejects where none is built
the file's variables
Checks the key in the proof against the commitment.
a proof is a key with a proof for that key
the verifier queries the hash function at the key's code
it rejects unless the answer is the commitment, and then runs the inner verifier with that key
it rejects a key without a code, and in that case makes no query
layouts W (hash queries) and S (seeds' queries); how an answer is written as digests, cA; a fixed seed with its answer, r₀
parameters p, a key k, an instance x, a proof π
an algorithm that queries the separate oracles and returns accept or reject
the decision of verifyAtFullKey (below),
on the key completed from the proof (KeyRoot.full): its proof string for offline, and its one copy (a further encoding) as the list;
on the instance, and on the rest of the proof (OfflineLinkOnlineProof.low): the place 0, the number, the proof string for onlineBatch
layouts W (hash queries) and S (seeds' queries); how an answer is written as digests, cA; a fixed seed with its answer, r₀
parameters p; a whole key v (FullKey): a root, its seed with its answer, a proof string for offline, a list of copies
an instance x; a proof π (RequestProof): a place in that list, a number, a proof string for onlineBatch
an algorithm that queries the separate oracles and returns accept or reject
take the proof string for offline, the copy at the place π.leaf of the list, and the proof string for onlineBatch
all three are present, and the copy contains a proof string for L.link:
the seed of the key's root is recomputed and compared (outOfDomainSeedIs)
so is the seed of the copy's root
offline is verified on the key's root
L.link on the key's root and the copy's root
onlineBatch on the copy's root and the instance
S.num accepts on input the number π.copy and the parts of the proof string for onlineBatch sent in the clearone of them is missing: reject
The number π.copy tested by S.num is chosen freely by the prover: nothing relates it to the place π.leaf of the copy that is used (the Lean comment on the field copy of RequestProof).
the file's variables
Checks an out-of-domain seed.
cm: the table's roots: an out-of-domain seedit asks the seed's two queries at the table's root: the first (seedQ0),
the second (seedQ1) at the chain value of the answer to the first,
and compares the result with the seed in the key or the proof (s)
the file's variables
the compiler's numbers p; a digest cm; an out-of-domain sample rec; a proof string π
an algorithm that queries the separate oracles and returns accept or reject
verifyOneProtocol at the offline IOP
its chain is given the first table's root and its out-of-domain answers
the file's variables
the compiler's parameters p; two digests cm, cm'; two out-of-domain samples rec, rec'; a proof string π
an algorithm that queries the separate oracles and returns accept or reject
verifyOneProtocol at the link IOP
its chain is given the roots and the out-of-domain answers of both tables
the file's variables
the compiler's numbers p; a digest cm; an instance x; an out-of-domain sample rec; a proof string π
an algorithm that queries the separate oracles and returns accept or reject
verifyOneProtocol for the online IOPxinBA: the instance with one fixed out-of-domain sample r₀ (seed and answers) in each of the two places for a samplex, rec): the request's instance and the out-of-domain sampleThe definitions in this folded section have at most a few lines each. They pass arguments from innerCompiledVerifier to Arg.buildInstance, verifyDigestKey and verifyAtKeyRoot. schemeOverOneHashFunction (above) does more: it implements the separate oracles of verifyAtKeyRoot by the single hash function (§4.1). ArgumentSystem.ofArgument presents the result as an argument system.
the file's variables
The inner compiler, which maps an input to an argument system whose verifier is innerCompiledVerifier. The verifier is built from the protocol and its layout (verifyAtKeyRoot); the committer and the prover are built from the input's fields commit and prove.
the file's variables
ArgumentSystem.ofArgument applied to the scheme tokenScheme, the committer commitE and the model nextToken. The key's code enc is one of tokenArgumentSystem's parameters.
the file's variables
Turns a scheme into an argument system. It uses the scheme's prover and verifier; the committer comes from the separate argument commit, not from the scheme.
the weights are the scheme's indices
there are no public parameters
the committer's randomness: a number from 0 to bound
a proof: a proof of the scheme, Pf
the model is nextToken
the committer samples one number
then the committer makes the queries of commit
the prover is the scheme's, with the weights and that number as its key
the verifier makes the queries of the scheme's verifier
commit or the scheme's verifier samples a number, the algorithm here continues with 0.verify defined here is deterministic by construction (deterministicOf, VerifiableInference/Deterministic.lean:21).the file's variables
Applies three transformations to the scheme on typed instances, innermost first: the key's digest becomes the verifier's key (digestKeyScheme), the committer's random choices are sampled first (Arg.coinsFirst), and the instance is built from the prompt, the output tokens and further tokens in the proof (Arg.buildInstance).
the file's variables
Arg.digestKey applied to the scheme with one request per proof (oneOf): the commitment is the digest of the verifier's key.
the file's variables
Shortens the commitment: the committer publishes the hash of the verifier's key, each proof contains that key, and the verifier is verifyDigestKey.
the file's variables
Makes the commitment randomness a single number that is sampled first, as an argument system requires. The verifier is unchanged. If the bound suffices for the committer, the verifier's key is distributed as before; for other bounds, nothing is claimed about how the two distributions compare.
the file's variables
The input's scheme over the separate oracles. Its committer and prover are the input's fields commit and prove. Its verifier is verifyAtKeyRoot, whose key is a root with its out-of-domain sample.
the file's variables
Everything that compile takes: one record with seven fields.
publicSide: the public side, including:
wiring:
provers: the honest provers of the protocol's three interactive oracle proofs
settings: what the honest committer and prover choose in addition to their three IOP provers, at each value of the family's public reading, including:
firstBlockTest: a test on a query and the first hash block of its answer; the committer and the prover query the other blocks only if it passes (meant for nonce searches)
coinBound: the honest committer samples one number from 0 to this bound
format: how a proof is written down and parsed
The verifier that compile builds reads only publicSide and the parser in format.
the file's variables
The public side of what is compiled, for one set of public files.
the type Index of the protocol's indices (what is committed)
the type Instance of the protocol's instances
the protocol: protocol (HolographicProtocol, §3)
which rounds of the offline IOP a batch shares: offlineRoundSplits
which rounds of the link IOP a batch shares: linkRoundSplits
whether the verifier takes these files at all: filesInScope
the first reading of the files, filesDigest: their digest, obtained from the hash function
the type Further of what the second reading returns
the second reading, furtherReading, which takes the digest as input
the layout in force, layoutAt, as a function of what the two readings return
the model: model
the map from weights to what is committed: indexOf
The verifier reads neither the model nor that map. Of the other fields, it does not read the type Index, reads only the verifier's side of the protocol, and does not read the six further fields of a layout shown on the next card (innerCompiledVerifier_eq, Johnson/Top/InnerCompiledVerifierSide.lean:79).
the file's variables
A hash layout (it extends HashLayout) with six more fields of the inner compiler's input (InnerCompilerInput), which the verifier does not read:
nextToken: maps an index and tokens to a token or nothing
ProverKey: a type
commit: maps an index to an algorithm that may sample numbers, queries the separate oracles, and returns a key root and a ProverKey
prove: maps a ProverKey and a batch of instances to an algorithm that may sample numbers, queries the separate oracles, and returns the batch's proofs (ZKCP.Gen.Slots)
coinBound: a number
fallbackProof: a key root and a proof
the file's variables
The layouts as read by the committer and the prover, for a public side side.
baseDigest, baseFurther: one fixed value for each of the two readings, used in the family's type
family: the layouts as one family, indexed by the value of the public reading
pair: maps the two readings' values to a value of the family's public reading (of type family.D)
a proof (agree) that they are the verifier's: for all values of the two readings, the family at their pair equals the input of side.layoutAt at those values
a default instance (fallbackInstance), used where a request cannot be turned into an instance
the file's variables
The proof format: the type of a proof as submitted, a parser and a writer.
Form: the type of a proof as submitted
parse, the parser, part of the verifier: given a prompt, an output and any form, it returns a typed proof
write, the writer, part of the honest prover: maps a typed proof to a form
the file's variables
types Weights and Form; a model, nextToken
the four parts that the verifier does not read, side (CompiledSide, the next card)
a verifier, verifier
The argument system made from these three:
the weights have type Weights
It has no public parameters.
the commitment randomness is side's
a proof is a Form
the model is nextToken
the sampler, the committer and the prover are those of side
the verifier is verifier
the file's variables
The four parts of an argument system that its verifier does not read.
The honest committer stores the weights as an encoded table, the first table, and answers requests from further encodings of it, called copies. Each copy has a link proof, which is meant to show that the copy decodes to the same index as the first table. The number of copies is a setting in honestProversAndSettings, which produces one copy (furtherCopies = 0).
The committer encodes the index as the first table, hashes that table into a Merkle tree, computes its out-of-domain sample and adds the offline proof. Each copy gets a link proof. The commitment has 256 bits. It is the hash function's answer on one bit string, the encoding of the key. The field keyCode of the hash layout computes this string from the key (the first table's Merkle root and its out-of-domain sample) and a part of what is read from the public files. The compiler does not fix which part. For FlashProve it is the digest of the files; this was found by reading the Lean code and is not stated by any theorem (lean/GAPS.md, 5).
The verifier takes the first table's root and out-of-domain sample from the proof, computes the same bit string, and compares the hash function's answer on it with the commitment.
It then recomputes the out-of-domain seeds of the first table and of the copy that the proof uses, and runs the compiled verifiers of the three IOPs: offline on the first table's root, link on both roots, and online on the copy's root and the request. Finally, it applies a test supplied by the hash layout (num) to the number that the proof gives for that copy and to the parts of the online proof that are sent in the clear. The compiler assumes nothing about this test.
Some rounds require proof of work. The prover must find a nonce for which the round's Fiat–Shamir answer passes a test on some of its bits, and the verifier rejects otherwise. In FlashProve's IOPs these bits are further bits of the round's challenge, and the IOP's verifier rejects unless all of them are 0 (Appendix A, The terms of this appendix, proof-of-work bits). The search for a nonce is called proof-of-work grinding; each failed attempt costs one hash query.
This section applies the compiler to one input, flashProveAtFiles, and states what is required of the result. compile (flashProve setup) is the compiled argument system: a committer, a prover and a verifier that query a random oracle. The six theorems (Final statements) are about compile at this input only.
finalSoundnessError q = 16 (q + 1 + 2^23) / 2^128 + (q + 2^23 + 3)^2 / 2^256. Here q counts the hash queries of the committer and the prover together, honest or adversarial (in sound, adversarial). finalBindingError is defined below, among the values substituted for the parameters. finalCompletenessError is 2^-40.
The record that compile takes as input. Its arguments:
files: the public filessettings: the settings of the integer modelhonest: the honest provers and settingsa Compilable (§4.3). flashProveAtFiles is the whole record that compile takes.
publicSide and wiring contain the protocol, the model and the layout of the hash queries
the fallbackInstance in wiring is taken from the honest provers and settings
provers and settings are taken from the honest provers and settings
firstBlockTest is the test on the first hash block of an answer that determines whether a nonce search queries the other blocks
coinBound is taken from the honest provers and settings
format contains the parser and the writer of a proof's bytes
Eight of the twelve fields of its public side are taken from another record in the library, the protocol's description FlashProve.flashProveDescription (Appendix A); the other four are the test on the public files, their digest, the model, and the map from weights to what is committed.
The protocol (§3) is a part of that description and a function of the public files; it is assembled from many parts (Appendix A, How FlashProve's description is assembled).
provers, settings, coinBound and the fallbackInstance inside wiring are taken from the honest provers and settings; the other fields depend only on the public files and the model's settings.
Three conditions on the three public files (parameter, layout and scale file). The verifier tests only the first (filesInScope):
inScope: the layout file is that of the stored full-size example, and the parameter file equals that example's byte for byte, except for eight numbers (five of the normalizations, three of the acceptance policy); the test also requires that the files are read without error and that 2^8 ≤ theta
read: readFiles returns parameters
exactMatch: the policy is exact match (the output must be the model's, token for token); the verifier does not test this
Thus the six theorems concern one model shape. The scale file and the five numbers of the normalizations are free, subject to what readFiles accepts. Exact match fixes the three numbers of the acceptance policy.
The condition on the public files under which the six theorems hold:
FilesTaken (the card above), and
the test protocolDataWellFormed, which depends only on the three public files and is computed with the second hash function (§5): the protocol's data can be built from them without error, no list of rounds is empty, the data for the key and for the proof have the full-size depth, and the sizes are within fixed limits. The verifier also performs this test: the decisions of its three IOPs reject everything if it fails (theKeyGateAt, theLinkGateAt, theProofGateAt; see Appendix A, How FlashProve's description is assembled)
All six theorems assume FilesInUse, through PublicSetup; the proofs of sound and refusedHandsOutNoProof use only FilesTaken.
2^-154, the bound in the zero-knowledge theorems zeroKnowledgeOnCanServe and zeroKnowledgeAtEveryRequest. It is a statistical distance, for up to 688,127 replies and 2^64 hash queries; it is not a security level.
The proof gives the same statement for any error that is at least stepErrorAtTheStops = 2^-157 + 688,127 · 2^-174 (AtFullSide/E2E/TheCompiledStepFilled.lean:132).
The library's stored full-size example of the three files (VerifierAndGoals.storedPublicFiles, a value written in Lean and not tied to any file on disk) satisfies FilesInUse.
So the hypothesis of the six theorems can be met.
The verifier of compile at flashProveAtFiles is finalVerifier, for arbitrary honest provers and settings (theorem compile_flashProve_verify).
The verifier of the final system: compiledVerifier applied to FlashProve's public side and parser. Its two arguments are the public files and the model's settings (IntegerTransformer.Settings); it takes none of the honest provers and none of the honest committer's and prover's settings.
For all public files, all settings of the model and all honest provers and settings, the verifier of compile at flashProveAtFiles is finalVerifier at these files and settings.
Hence the verifier does not depend on the honest provers and settings.
finalCompletenessError is the constant VerifierAndGoals.completenessErrorBound, which is (1/2)^40 = 2^-40. In the theorem completeOnCanServe it bounds the probability that the verifier rejects the honest prover's proof. A nonzero bound allows for the honest prover's searches for a proof-of-work nonce, which stop after a bounded number of tries.
The bound in the soundness theorem, as a function of the number of hash queries.
finalSoundnessError q is VerifierAndGoals.soundnessErrorInQueries q 1VerifierAndGoals.verifierQueryAllowance) is the allowance for the verifier's own queriesfinalBindingError q is VerifierAndGoals.levelError q, the larger of VerifierAndGoals.soundnessErrorInQueries q (2^23) and VerifierAndGoals.bindingErrorInQueries q. The first is 16 · T / 2^128 + (T + 2)^2 / 2^256 at T = q + 2^23 + 2^23; the second is 16 · (q + 2^23) / 2^128 + (q + 2^48 + 2^23 + 2)^2 / 2^256, where 2^48 is VerifierAndGoals.honestBudget. The value is about q / 2^124 + 2^-100.
honestQueryBudget is the constant VerifierAndGoals.honestBudget, which is 2^48. The theorem repliesFit uses it through WithinBudget (§6.1): one run each of the honest sampler of commitment randomness, the honest committer and the honest prover may together make at most this many queries to the hash function.
finalVerifierQueries is the constant VerifierAndGoals.queryBudget, which is 2^64. The theorems on zero knowledge bound the statistical distance only for verifiers that make at most this many hash queries.
finalReplyCount is the number 688127. The theorems on zero knowledge give their bound for up to this many replies under one commitment, and the theorem repliesFit shows that it is at most onlineRunsPerCopy. It is the largest s with 62 + s · 64 ≤ 44,040,191, the second inequality of TableBudgetFits. A reply to a refused request, which is the empty proof, also counts.
HonestProversAndSettingsAtFiles files settings collects what flashProveAtFiles needs for the honest committer and prover.
fallbackInstance, the instance used when no instance can be built from the request
provers, the honest provers of the protocol (HonestProvers, §3)
compiledSettings, the compiler's choices for the honest committer and prover (a CompiledSettings for each value of the public reading), such as the limits on the nonce searches and the number of copies of the committed table
coinBound, where the honest committer samples one number from 0 to coinBound
onlineRunsPerCopy, the number of runs of the online IOP that the honest settings assign to one copy
finalVerifier does not take this record as an argument.compile does not read onlineRunsPerCopy; among the six theorems, only repliesFit mentions it.The factor, 16, in the error bound soundnessErrorInQueries.
The number that soundnessErrorInQueries adds to the adversary's and the parser's queries to account for the verifier's own queries. VerifierWithin (Ladder/Bits.lean:128, no card on this page) says what is counted and in which unit. The number is a choice; no statement other than VerifierWithin says that it is enough. The error of the theorem sound contains it, and sound has no hypothesis about it. In bindingErrorInQueries, where no verifier runs, it is slack.
The soundness error, where t bounds the adversary's queries and n the parser's: with T = t + n + verifierQueryAllowance it is errorFactorPerQuery · T / 2^128 + (T + 2)² / 2^256. That is 16 / 2^128, or 124 bits, for each query, and about 2^-101 at t = n = 0.
The binding error, where t bounds the committer's and the opener's queries together:
the linear term: errorFactorPerQuery · (t + verifierQueryAllowance) / 2^128
plus the square term: (t + honestBudget + verifierQueryAllowance + 2)² / 2^256
At t = 0 this error is about 2^-101, and finalBindingError, the maximum of it and a soundness term, is about 2^-100.
The experiment in the second clause of SoundAndBinding runs the honest committer once more. That run's queries are not the adversary's; honestBudget accounts for them in the square term.
The bad event that such a run can cause is that one of its answers equals another answer or a value that the adversary wrote. A bound on only these events has the form 3 · (t + 2 q + 2)² / 2^256, where q bounds the queries of one run of the committer.
Wherever this error is less than 1, that bound is smaller than it because of the linear term, not the square term; without the linear term, the square term would have to take that form.
The linear term may also have to account for events that a committer can search for, such as a collision at a seed.
The larger of the soundness error at 2^23 parser queries and the binding error.
The numbers.
| property | bound | at |
|---|---|---|
| Soundness | finalSoundnessError q = 16 (q + 1 + 2^23) / 2^128 + (q + 2^23 + 3)^2 / 2^256, about q / 2^124 + 2^-101 | q hash queries by the committer and the prover together |
| Binding | finalBindingError q, about q / 2^124 + 2^-100 | q hash queries by the committer and the prover or opener together |
| Completeness | finalCompletenessError = 2^-40 | one request that can be served and whose output tokens are the model's |
| Zero knowledge | finalZeroKnowledgeError = 2^-154, a statistical distance | up to 688,127 replies and 2^64 hash queries |
Numerically, the soundness error is about 2^-100 at 2^23 hash queries, and about q / 2^124 above that (2^-60 at q = 2^64). The fixed term 2^-101 comes from the constant 2^23 in the formula, which accounts for the verifier's own hash queries. It is part of the bound as stated, and sound is proved without any hypothesis on these queries. None of these figures is a security level.
In the theorems on soundness, binding, completeness and zero knowledge, the hash function is sampled uniformly at random, so these are statements in the random oracle model. compile does not take the hash function as a parameter. A program uses one concrete hash function instead. leanVerifier uses blake2bHash, a function from bit strings to 256 bits built from BLAKE2b (Appendix B), in place of the random oracle.
leanVerifier is the verifier of §4.3 with each of its queries answered by blake2bHash. finalVerifierProgram is defined for arbitrary public files, using only the public part of the compiler's input. At the files of a public setup it equals leanVerifier (leanVerifier_eq, below).form of leanVerifier is what this page calls the proof as submitted: a list of tokens and five byte strings. It is not the file that the prover writes. A program outside Lean splits the prover's files into the five byte strings. The tokens are the tokens of the request that follow the checked positions; they are read from the request file (formOf, Johnson/PVR/Program.lean:113).verdictOf (card below) reads eleven files: the three public files; the user's three files, from which the commitment, the prompt and the output are parsed; and five parsed files, which are the five byte strings of form.verdictOf uses its own definitions of several objects. This page names three of them:The heuristic is the assumption that, in the theorems on soundness, binding, completeness and zero knowledge, blake2bHash may be treated as a function sampled uniformly at random (the random oracle model). For zero knowledge, the simulator also answers the hash queries in place of this function (§8). The heuristic is not a theorem and is not stated in Lean. It is an assumption about the hash function and this argument system together. It also carries one assumption about the second hash function: that blake2bHash behaves like a random function that is independent of it (below).
three public files, a commitment, a prompt, output tokens and the parsed proof; it returns a verdict or nothing
the verdict (verdictThe) read off the executable form's run (rideThe), both with Fmt.oracle, the hash function on byte strings built from BLAKE2b (Appendix B)
It is defined for all public files. It tests that they are in the verifier's scope, can be read and are well formed. It does not check that they specify the exact-match policy. leanVerifier is defined only for a public setup. It also uses the protocol's second, fixed hash function (§5).
Option Bool, but its value is never none. This follows from verdictThe_eq with Fmt.size_oracle; no theorem of the file states it.executableVerifier, which is not marked noncomputable. Lean's list of axioms for it also names the axiom of choice. Walks from the executable form's code (verdictThe, rideOf, letsThe), through definitions and never into a proof, made over Lean files that differ from this repository's, met no definition of the library that names the axiom of choice. The only definitions met that name it are two of Lean's core library (Classical.propDecidable, Classical.ofNonempty). So, as far as Lean's evaluator, compiler and runtime are trusted, no code that a run executes calls choice. This is not a theorem (lean/GAPS.md, 56).the bytes of the eleven files
the verdict of verdictOf
is obtained as follows: claimOf parses the claim from the user's files; if it fails, there is no verdict; otherwise executableVerifier is applied to the public files, the claim and the parsed proof (formOf)
It is proved by unfolding definitions (rfl).
a public setup, the bytes of the eleven files, and a claim
the three public files among them are those of the setup
and claimOf parses that claim from the user's files
verdictOf returns the verdict of leanVerifier on that claim and the parsed proof (formOf)
The command lean-verify does not enforce the hypothesis sameFiles (see the card executableVerifier_eq_leanVerifier, Final statements).
whenever the commitment, the prompt and the output can be read from the user's three files
the verdict of verdictOf
equals finalVerifierProgram applied to these; the two definitions agree
claimOf splits the user's three files as the format specifies (lean/GAPS.md, 37).sound does not cover acceptance under another policy.finalVerifierProgram equals leanVerifier only for a public setup's files (leanVerifier_eq, below); the theorem verdictOf_eq_leanVerifier (above) combines the two.The command lean-verify calls the three parts of verdictOf (claimOf, stepsOf, verdictAt) in order and prints between the calls. verdictOf is an executable form of the Lean verifier: a second implementation in Lean that uses the same definitions of the protocol's data and decisions.
The final verifier with each of its hash queries answered by blake2bHash, the hash function on bit strings built from BLAKE2b (Appendix B). By definition, finalVerifier is the verifier of compile applied to flashProveAtFiles (compile_flashProve_verify, §4.4, whose proof is rfl).
The argument form is the proof as submitted, a list of tokens and five byte strings.
For every public setup, commitment, prompt, output and proof form, leanVerifier equals finalVerifierProgram (§5) at the setup's files and the settings that they determine. This says nothing about a run of the executable form.
finalVerifierProgram is the value that verdictOf_eq_finalVerifierProgram refers to.
The executable form's accept-or-reject verdict on given bytes, if any.
an argument system, a hash function, a commitment, a prompt, output tokens, a proof
the verifier's decision under that hash function: accept or reject
an argument system, a hash function, a commitment, a prompt, output tokens, a proof
under that hash function, the verifier step of an experiment returns system.accepts hash commitment prompt output proof with probability 1
The IOP being compiled itself uses a second hash function, secondHashFunction. It is a fixed function, built from BLAKE2b's compression function with a number written into the block counter. It is part of FlashProve's description (Appendix A); the six theorems do not take it as a parameter. It is therefore part of the compiled verifier, and hence of leanVerifier.
protocolDataWellFormed, the extractor and the honest online prover are defined using it. Through protocolDataWellFormed it also appears in the hypothesis of the six theorems.G7', Ladder.lean) is stated in the library but not proved. Each theorem holds for every request in its scope, and hence also for a request in that scope that an adversary chooses knowing this function.blake2bHash, which is built from the same compression function. It therefore also assumes that blake2bHash behaves like a random function that is independent of the second hash function. This assumption is made outside Lean and is not a hypothesis of any theorem (lean/LIMITS.md, Assumption 2, second half).The command lean-verify evaluates the Lean function run, an IO wrapper that calls the three parts of verdictOf in turn (claimOf, stepsOf, verdictAt), with BLAKE2b as the hash function. The theorem verdictOf_at shows that these three parts compose to verdictOf. verdictOf parses the claim from the user's files and applies executableVerifier to it (verdictOf_eq_executableVerifier). The function verdictOf is a second implementation of the verifier in Lean. It uses the same definitions of the protocol's data and decisions, and has steps of its own (§5).
The eight theorems of this list (executableVerifier_eq_leanVerifier, executableVerifier_eq_leanVerifier_stored, verdictOf_eq_executableVerifier, verdictOf_eq_leanVerifier, verdictOf_eq_finalVerifierProgram, leanVerifier_eq, verdictOf_map, verdictOf_none) are equations between values of deterministic Lean functions. None of them involves a random oracle or makes a security claim.
executableVerifier_eq_leanVerifier (Final statements): for every public setup, executableVerifier applied to the setup's public files returns the verdict of leanVerifier. executableVerifier_eq_leanVerifier_stored (no card on this page) is its instance at the stored public files.verdictOf_eq_executableVerifier (card above): verdictOf parses the claim from the user's files and applies executableVerifier to the public files, the claim and the parsed proof. It is proved by unfolding definitions.verdictOf_eq_leanVerifier (card above): the same fact as the first, stated for verdictOf. It therefore has two further hypotheses: the claim can be parsed, and the public files are those of the setup.verdictOf_eq_finalVerifierProgram and leanVerifier_eq (cards above) relate verdictOf and leanVerifier to a common term, finalVerifierProgram (the compiled verifier evaluated with blake2bHash on given public files).verdictOf_map (Johnson/PVR/ProgramTotal.lean; no card on this page). For arbitrary public files, whenever the commitment, the prompt and the output can be parsed from the user's files, verdictOf returns the verdict of VerifierAndGoals.verify (Ladder.lean; no card on this page) for FlashProve's description (flashProveDescription), which includes the second hash function, evaluated with BLAKE2b. VerifierAndGoals.verify is the verifier in the soundness theorem sound_of_verify_at, whose hypotheses are that the public files are in scope, parse, and specify exact match. It equals the compiled system's verify by compile_flashProve_verify_eq and theDescription_eq.verdictOf returns no verdict (verdictOf_none).The agreement is not special to BLAKE2b: for every function O from byte strings to 32-byte strings, the executable form run with O returns the verdict of VerifierAndGoals.verify evaluated with hashOf O (PV.Ride.verdictThe_eq, Johnson/PVR/RideEveryHash.lean:116). Hence its decision satisfies SoundOfDecision, a restatement of Sound, with a sampled hash function, under the hypotheses and the bound of sound_of_verify_at (PV.Ride.sound_of_the_form_events_oOf, Johnson/PVR/SoundOfTheFormEvents.lean:264). Neither theorem has a card on this page, and neither gives soundness at the concrete hash function.
The security statements for the compiled system are stated with the hash function sampled at random. Soundness at BLAKE2b is therefore not a theorem (see the card executableVerifier_eq_leanVerifier, Final statements).
verdictOf, executableVerifier, finalVerifierProgram and leanVerifier, not the run of the command lean-verify. No theorem is about the command itself, which consists of a script, an IO wrapper in Lean (run), natively compiled helper code, and Lean's compiler, interpreter and runtime.executableVerifier, and hence verdictOf, does not check every condition of a public setup. It tests that the public files are in the verifier's scope, can be read and are well formed; it does not check that they specify the exact-match policy. If the public files pass the scope test (InScope) but specify another policy, the verifier may accept, and sound does not apply. The serving scripts use such a policy, the tolerant policy.leanVerifier fixes it to blake2bHash. Hence no theorem bounds the probability that leanVerifier accepts a false claim, and no theorem shows that it accepts even one honest proof.run, the natively compiled helper code, and Lean's compiler, interpreter and runtime are trusted.claimOf, with the functions that it calls, parses the user's three files into the commitment, the prompt, the output and the remaining tokens of the request. The first three form the claim, and the last is passed to the verifier as part of the proof. No theorem shows that claimOf implements the file format (lean/GAPS.md, 37).parse of the proof format (§4.3), is defined in Lean and maps the prompt, the output and the proof as submitted to a typed proof. The verifier calls it, so it is covered by sound.These are tests, not theorems. All used synthetic weights. One Lean file, with one definition and four theorems, which nothing else imports, was added after the runs reported here and checked on its own (lean/CHECK-RESULTS.md). The runs executed the parts of verdictOf, not executableVerifier under that name.
For a provider who cares that the weights stay hidden. Three things to read:
ZeroKnowledgeOn (§6.3), with its two experiments (§6.2)requestOutcome: served or refused, §6.1), and what the three public files reveal about the weights, which none of the six theorems covers, nor zeroKnowledgeAtEveryRequest (§6.3)zeroKnowledgeOnCanServe and refusedHandsOutNoProof, and what follows from them for every request (§6.3). They concern the honest committer and prover as Lean definitions, which compile constructs from honestProversAndSettings (a black box on this page). Nothing is proved about the programs.Completeness and zero knowledge are statements about the honest committer and the honest prover. A reader who relies on proofs does not need them; the provider does.
Completeness and zero knowledge are stated for one commitment by the honest committer and one request per proof, with the prover's own coins fresh and uniform for each reply. In the completeness theorem the weights and the request are fixed before the hash function is sampled; a request chosen after seeing the commitment or the hash function is not covered. With honestProversAndSettings the committer makes one copy of the committed table (on copies, see §6.4). The theorems of this section say nothing about an honest committer that makes more copies.
A request can be served (CanServe) if its tokens are in the vocabulary, its output is not empty, and the model has a value on the whole window of 1,024 tokens. The completeness theorem says nothing about a request that cannot be served or whose output is not the model's. No theorem states that a request is served at a real model's weights (see the folded section below that begins Notes: two definitions).
systemdomain: a condition on weights, a prompt and output tokensall weights, prompts and output tokens
that are in domain and whose output tokens are the model's
The hash function is sampled uniformly at random. Then:
the commitment randomness is sampled
the honest committer commits to the weights
the honest prover computes a proof for the prompt and the output tokens
the verifier of system decides
the honest committer and the honest prover are rejected
Pr[event] ≤ α
The claim that there is a request whose output is the model's and that FlashProve's verifier rejects for every hash function, commitment and proof rests on an informal argument; no theorem states it.
A condition on the weights may be part of the system's type Weights.
CompleteOn is the plain completeness property (stated for every request whose output is the model's) with one added side condition on the requests. If there is such a request that the verifier rejects for every hash function, commitment and proof, then the plain property fails for every α below 1 (not_complete_of_rejected, VerifiableInference/NotComplete.lean:36).
Side conditions on a prompt and an output, in addition to "the output tokens are the model's":
canServe_nowhere_atHaltingWeights, VerifiableInference/ModelGuardsAtReference.lean, at the settings of the reference table of scales, which are those that the stored public files give: settingsOfRead_full, Johnson/Goal/Files/FilesReadAtRef.lean:143).wellFormed_and_result_iff, VerifiableInference/WellFormedRequests.lean:48; a well-formed request has both). This definition's Lean comment says "by hand", but the theorem says more.For the settings of the reference table of scales and the valid weights haltingWeights, no prompt and output satisfy CanServe.
At the index of haltingWeights no request is true (Cm.empty_language, Cm/RelTrueExp.lean).
The theorem completeOnCanServe, in full. For every public setup, compile (flashProve setup) satisfies CompleteOn (above) with CanServe and finalCompletenessError. That is:
Remark. The library proves it equivalent to a second form, stated for well-formed requests whose result is the claimed output (finalComplete_iff_completeOn, Johnson/Face/Checks.lean:57); both terms are defined below.
Where the theorem says nothing. The theorem completeOnCanServe says nothing about a request whose result is none or tokens other than the claimed ones. For such a request requestOutcome is refused, and refusedHandsOutNoProof states that the prover's reply is the empty proof (noProofForm: a form all of whose parts are empty). None of the six theorems states that a refusal can be checked.
A well-formed request. A request (a prompt with a claimed output) is well formed (RequestForm) if every token is in the vocabulary, neither list is empty, and the two together have at most 1,025 tokens.
The model's result (requestResult, Appendix C) is obtained from one run of the model on a window of exactly 1,024 tokens: the prompt, the claimed output, then token 0 as often as needed, all truncated to 1,024 tokens (IntegerModel.zeroFilledWindow). If the request has 1,025 tokens, the last output token is outside the window: the run does not read it, and it is only compared with the run's choice at the window's last position.
none if the model has no value on that window, including the padded positions.some of the tokens that the run chooses at the positions just before the output tokens.The bit. requestOutcome assigns each request one of two values, served or refused. A request is refused if it is ill-formed, if the model has no result on it, or if the result differs from the claimed output. The bit depends on the weights and is not hidden: zeroKnowledgeAtEveryRequest gives it to the simulator. In that statement each reply shows the verifier nothing in addition to a proof.
At valid settings, a request is served if and only if it can be served and its output tokens are the model's (served_iff_canServe, VerifiableInference/AtEveryRequestGuards.lean:127).
A Request is a pair of lists of tokens: the prompt, then the claimed output. Every such pair is a request; the conditions on it are in RequestForm (Appendix C).
The bit of a request: served or refused. Neither value carries any data, in particular no token.
The function assigning each request its bit, which depends only on the settings, the weights and the request.
served if the request is well formed
and the model's result on the request's window (requestResult, Appendix C) is the claimed output
refused otherwise; the same value is returned for an ill-formed request, a result of none, and a result of other tokens
Whether a request is well formed depends on the model's settings and the request, not on the weights.
The simulator of zeroKnowledgeAtEveryRequest is given this bit (§6.3); in that statement each reply shows the verifier nothing in addition to a proof.
system (§1)unserved: a predicate on the weights and a request; the statement applies where it holdsisNoProof: which proofs count as no prooffor all weights, values of the committer's randomness, requests, hash functions and proofs form
at the requests satisfying unserved
the system's prover outputs no proof: every value it can return satisfies isNoProof
(for a fixed hash function, the prover can return form if and only if the probability of form over the prover's own coins is not 0)
The theorem refusedHandsOutNoProof, in full. The theorem concerns the output of the compiled prover. For every public setup,
requestOutcome is refused, well-formed or not, and every hash function,noProofForm: a form all of whose parts are empty).Not covered. A refusal is not checked: an empty proof proves nothing, and a prover can return it for a request that it could serve.
Remarks.
rejectsEmptyProof).zeroKnowledgeAtEveryRequest simulates a failed nonce search. It does not simulate the aborts that depend on the online prover's private input; their probability, at most 2^-174 for each reply, is counted in the bound 2^-154 (§4.4). In each of these cases the reply looks like the reply to a refused request.refusedHandsOutNoProof is proved more generally, for public files that meet FilesTaken: finalRefusedHandsOutNoProof_value (AtFullSide/Face/TheFinalStatementOneBitHolds.lean:60).The form that contains no proof: an empty list of tokens and five empty byte strings.
The form equals noProofForm, the form that contains no proof.
for every hash function, public setup, commitment and request
the compiled verifier rejects the empty proof
An empty proof does not show that the request was refused.
Hence the empty proof is never accepted.
Proved for all public files and settings as rejectsNoProof_value (AtFullSide/CompletenessAndZeroKnowledge/RejectsTheEmptyForm.lean:77).
Hash, evaluate: §8; noProofForm: above.
The honest sampler, committer and prover, run once each, make at most budget hash queries in total.
there are three numbers
whose sum is at most budget, such that
the sampler of commitment randomness makes at most sampling hash queries
for all weights and all commitment randomness, the committer makes at most committing hash queries
for all weights, all commitment randomness, every prompt and all output tokens, the prover makes at most proving hash queries
Two definitions of "the model's output".
CompleteOn and ZeroKnowledgeOn use IsModelOutput (§1), which runs the model on the prompt followed by each proper prefix of the output, without padding.requestOutcome uses the model's result, computed by one run on the padded window; CanServe requires that this run has a value.One direction is proved. At the settings given by public files (these settings pass settingsAreValid, the library's test on sizes and quantization ranges), if a request is well formed and its result is the claimed output, then each output token is the model's next token in the sense of §1 (from wellFormed_and_result_iff, VerifiableInference/WellFormedRequests.lean:48).
The other direction fails for the empty output, which is the model's in the sense of §1, while a request with empty output is not well formed. It may also fail for a well-formed request if the model has no value at the last output token's position or at a padded position: such a request would be refused although its output is the model's in the sense of §1. No theorem rules this out, except for weights that meet a condition stated in the library but not on this page. No example of this is proved.
Not vacuous. For every set of public files that meets FilesInUse (one exists: filesInUse_stored), some request is served at some weights (someRequestIsServedInUse, below). Those weights are artificial: all their layers are zero. No theorem states that a request is served at a real model's weights, and at the settings that the stored public files give there are weights at which no request can be served (canServe_nowhere_atHaltingWeights, above).
For the files of every public setup, some request is served for some weights.
For any files in use, some request is served at some weights. For the existence of files in use, see filesInUse_stored above.
A malicious verifier is given the commitment and then proofs. The request for each proof is picked by a chooser: a function that maps the verifier's view so far to a request, or to nothing, in which case the experiment ends. In the real experiment, the hash function is sampled uniformly at random, and the honest committer and the honest prover run. In the simulated experiment, the simulator replaces all three; it is given each request and the information about the weights that the statement specifies.
This page has two definitions of a simulator, each with its own simulated experiment; the real experiment is the same for both.
Simulator is the general one: for each request it is given only the request. ZeroKnowledgeOn is stated with it.AtEveryRequest.Simulator takes one more argument: the information it is given about each request. ZeroKnowledgeWhere, and hence the theorem zeroKnowledgeAtEveryRequest, is stated in terms of it. Its card is in a folded section in §6.3.a structure with four fields
the commitment
the proofs obtained so far, each with its prompt and output tokens
the verifier's queries to the hash function with their answers
the numbers that the verifier sampled
a strategy, for a given type of proofs: one of
it stops
it queries the hash function at a bit string and continues with the answer
it samples a number from 0 to bound uniformly and continues with it
it requests the next proof and continues with the prompt, the output tokens and the proof that it is given
for a malicious verifier and a number of queries
stopped: true
a query, and the number is 0: false
a query, and the number is at least 1: every continuation meets the bound reduced by 1
a sampling step: every continuation meets the same bound
a request for a proof: every continuation meets the same bound
an argument system, the chooser, the weights and the committer's randomness; then the verifier's next step, the number of proofs that it may still request, and its view so far
the verifier stops: return the view
the verifier queries the hash function: the query and its answer are added to the view
the verifier samples a number: it is added to the view
the verifier requests a proof and none remains: return the view
otherwise the chooser is asked
it returns nothing: return the view
it returns a prompt and output tokens: the honest prover generates a proof; all three are added to the view and given to the verifier
an argument system, a verifier, a chooser, weights, the number of proofs
the honest committer samples its randomness
and computes the commitment to the weights
the verifier's steps (the card above), from a view containing only the commitment
A simulator consists of a type of states and three functions.
Apart from the arguments of these three functions, it is given neither the weights nor the committer's randomness.
Its running time is not bounded.
the state it keeps between steps; each function below may sample at random (PMF) and returns the new state (start returns the initial one)
it produces a commitment from the public parameters and the maximum number of proofs
it answers the verifier's queries to the hash function
it computes each proof from the prompt and the output tokens
The same steps as realSteps, with the simulator in place of the hash function and the prover.
the verifier stops: return the view
the verifier queries the hash function: the simulator answers, and the query and its answer are added to the view
the verifier samples a number: it is added to the view
the verifier requests a proof and none remains: return the view
otherwise the chooser is asked
it returns nothing: return the view
it returns a request: the simulator produces a proof from it; both are added to the view and given to the verifier
an argument system, a simulator, a verifier, a chooser, weights, the number of proofs
the simulator is given the public parameters of the weights and the largest number of proofs
and outputs the commitment
the simulated steps (the card above), from a view containing only the commitment
two distributions on the same set, each given by its probabilities of events
the supremum, over all events, of the absolute difference of the two probabilities
a query log
two entries with the same query have the same answer
The theorem zeroKnowledgeOnCanServe is stated in terms of ZeroKnowledgeOn, for the requests that can be served and whose output tokens are the model's. The compiled system has no public parameters (PublicParameters := Unit, §4.3), so the simulator is initially given nothing about the weights. It may depend on the three public files, and a fitted model's scale file is derived from its weights; what these files reveal about the weights is not covered. Whether a request can be served depends on the weights, and this is not hidden: the chooser of requests may know the weights and is the same in both experiments.
In the theorem zeroKnowledgeOnCanServe, 2^64 bounds the verifier's hash queries and 688,127 bounds the replies under one commitment. Within these limits the error is at most 2^-154 (finalZeroKnowledgeError).
systemdomain: a condition on weights, a prompt and output tokensone simulator, which is given:
all weights
chooser: it picks each prompt and output tokens from the verifier's view so far; it may know the weights and is the same in both experiments
the prompts and output tokens it picks satisfy domain at the weights, and the output tokens are the model's
verifier: it is given the commitment and up to proofCount proofs
it makes at most queries queries to the hash function
the statistical distance between
its view with the honest committer and prover
and what the simulator produces
is at most ζ queries proofCount
the simulator never gives two different answers to the same query
domain may depend on the weights; then whether a request meets it is not hidden.It is the plain zero-knowledge property, for requests whose output is the model's, with one more condition on the requests; without it the two are equivalent (zeroKnowledge_iff_zeroKnowledgeOn, VerifiableInference/MoreStatements.lean:170).
At every request. On its own, the theorem zeroKnowledgeOnCanServe says nothing about a refused request. Together with refusedHandsOutNoProof, it implies zeroKnowledgeAtEveryRequest within the same bound, where the simulator is given one bit per request: served or refused. This bit depends on the weights and is not hidden.
a public setup setup (PublicSetup)
a single simulator, which may depend on the public setup, simulates any verifier's view, for one commitment, at every request (fun _ => True: no condition on the request)
where the simulator is given only one bit about the weights for each request (served or refused), for up to 688,127 replies and 2^64 hash queries,
within statistical distance 2^-154
The bit itself is not hidden (the statement gives it to the simulator): for every well-formed request of its choice, a verifier learns whether the claimed output is the model's result. The full list of what is not covered is below.
It is not proved that this theorem recovers zeroKnowledgeOnCanServe.
A corollary of zeroKnowledgeOnCanServe and refusedHandsOutNoProof, by zeroKnowledgeAtEveryRequest_of_lines (in the folded section below).
ZeroKnowledgeBelowWhere: in the folded section below; requestOutcome: §6.1; settingsOfRead: Appendix A; finalVerifierQueries, finalReplyCount, finalZeroKnowledgeError: §4.4.
The simulator is given the bit of every request: up to 688,127 bits, at requests that the verifier picks. Over many requests the bits reveal what the model outputs, and the statement does not bound what they jointly reveal about the weights. In this theorem, 688,127 bounds the number of replies under one commitment; a reply to a refused request, which is the empty proof, also counts.
The theorem zeroKnowledgeAtEveryRequest, in full. For each public setup there is one simulator, fixed before the weights, such that for
(1) the statistical distance between the verifier's view with the honest committer and prover and the simulator's output is at most finalZeroKnowledgeError, 2^-154;
(2) the simulator never answers one hash query in two ways.
Remark. The theorem is stated as ZeroKnowledgeBelowWhere (in the folded section below) for compile (flashProve setup) itself: at each request, the verifier is given the request and the compiled prover's reply (a proof or the empty proof), and nothing else.
What the simulator is told. The simulator is given the maximum number of replies, each request and, of the weights, only one bit for each request: served or refused (requestOutcome, §6.1). A reply is what the compiled prover returns: a proof or the empty proof (noProofForm). The strength of the statement depends only on this function (requestOutcome): its value is the only function of the weights that the simulator is handed with a request.
What the bit reveals. The bit depends on the weights, and it is not hidden (the statement gives it to the simulator):
Public parameters. The type of public parameters of compile (flashProve setup) is Unit, so this system has none. Hence, in the experiment, the simulator of zeroKnowledgeAtEveryRequest is given the bits and nothing else about the weights (it may depend on the public files).
What a refusal does not reveal. For a well-formed request, a refusal does not reveal whether the model has no result or a result other than the claimed output. This is hidden only from a verifier that makes few requests:
Not covered by either theorem:
completeOnCanServe; on its own, the property in each of these two theorems is satisfied by a prover that outputs nothing (§11)).a public setup setup (PublicSetup)
the statement of the theorem zeroKnowledgeOnCanServe
the statement of the theorem refusedHandsOutNoProof
zero knowledge at every request
where the simulator may depend on the public files and is otherwise told, of the weights, only one bit per request (served or refused), within the same bound
Its two hypotheses are these two statements verbatim.
By a general theorem that holds for every argument system (zeroKnowledgeFollowsFromOn, VerifiableInference/AtEveryRequestFollows.lean:509), with served_iff_canServe (VerifiableInference/AtEveryRequestGuards.lean:127) to pass from the requests that can be served to the served requests.
ZeroKnowledgeWhere with one bound on the error:
system, hypothesis and told, as therequeries and proofs, and the bound barthere is an error function
that is at most bar for every number of hash queries up to queries and every number of proofs up to proofs
and ZeroKnowledgeWhere holds with it
system (§1)hypothesis: a predicate specifying which requests the statement is abouttold: a function of the weights and the request, whose value the simulator is givenerror: a bound, as a function of the number of queries to the hash function and the number of proofsThere exists a simulator such that
for all weights and every chooser
A chooser picks each request as a function of the verifier's view so far; it may depend on the weights and is the same in both experiments.
that picks only requests that satisfy the hypothesis
all numbers queries and proofCount (the maximum number of proofs that the verifier receives) and every verifier
The verifier makes no queries before the commitment.
with at most queries queries to the hash function
the statistical distance between
the verifier's view with the honest committer and prover
The real experiment is realExperiment (VerifiableInference/Statements.lean): the honest prover runs on every request that the chooser picks, and told is not among its arguments.
In the real experiment the hash function is sampled uniformly at random.
and what the simulator produces
is at most error queries proofCount
and the simulator never gives two different answers to the same query
(the probability that a query in the view has two different answers is 0)
A second structure of that name, in the namespace AtEveryRequest: this simulator is also given information about each request. A simulator consists of a type of states and three functions.
Beyond what these three functions are given, it is given neither the weights nor the committer's randomness.
It is computationally unbounded.
its internal state; each function below may sample at random (PMF) and returns the updated state (start returns the initial one)
it produces a commitment from the public parameters and the maximum number of proofs
it answers the verifier's queries to the hash function
it produces each proof from the request and from what it is given about that request
The steps of realSteps (VerifiableInference/Statements.lean), with the simulator in place of the hash function and of the prover.
told (what it is told about each request) and the chooserthe verifier stops: return the view
the verifier queries the hash function: the simulator answers, and the query and its answer are added to the view
the verifier samples a number: it is added to the view
the verifier requests a proof and none remains: return the view
otherwise the chooser is asked
it returns nothing: return the view
it returns a request: the simulator produces a proof from the request and the value of told at that request; the request and the proof are added to the view and given to the verifier
an argument system, a simulator, the function told, a verifier, a chooser, weights, the number of proofs
the simulator is given the public parameters of the weights and the largest number of proofs
and outputs the commitment
the simulated steps (the card above), from a view containing only the commitment
for each request, the simulator is given the value of told at the weights and that request
The theorem repliesFit, in full. For every public setup, three numerical conditions hold:
finalReplyCount (688,127) is at most onlineRunsPerCopy setup, whose value is also the numeric literal 688,127; so (1) compares two literals, and (2) is what relates this number to a table;TableBudgetFits: 62 + (furtherCopies + 1) · 62 on the first committed table, 62 + onlineRunsPerCopy setup · 64 on a copy);WithinBudget, §6.1).A copy. The committed table of weights is stored encoded, with random masks, and each proof opens some of its columns. Informally, one encoding supports only a limited number of openings before its masks are used up. A copy is a further encoding of the same table, with a link proof (compile, §4.3): a proof of the link IOP, which is meant to show that the copy decodes to the same index as the first encoding.
Condition (1) requires that the number of replies be at most the number of runs that the honest settings assign to one copy, because the prover samples its copy at random and keeps no count; condition (2) states that this many runs fit in one copy.
The number of runs of the online IOP that the honest settings assign to one copy: the field onlineRunsPerCopy of HonestProversAndSettingsAtFiles, a number that compile does not read. Nothing in the prover counts them.
compile (§4.3) constructs the honest committer and the honest prover from the three honest IOP provers in its input's field provers; for FlashProve these are the provers of honestProversAndSettings.
Remark. The protocol's record has fields for honest provers (honestOfflineProver, honestLinkProver, honestOnlineBatchProver), and the public side's layout has fields for a committer, a prover and the model's next-token function (commit, prove, nextToken). The compiled system is not constructed from these fields (their contents are described at the beginning of Appendix A):
provers (honestSide);compile);innerCompiledVerifier_eq, Johnson/Top/InnerCompiledVerifierSide.lean:79, which has no card on this page).the file's variables
The honest committer and the honest prover of the compiled system. The committer samples one number from 0 to coinBound as its randomness and runs the committer of compiledScheme with it; the prover is given the weights, that number, a prompt and output tokens.
the file's variables
The compiled scheme before it is brought into the form of an ArgumentSystem.
what is published is the 256-bit commitment
the prover's key
a proof as submitted
the honest committer and prover, built from the provers
a proof contains:
with the compiled verifier
Not covered. The prover does not enforce these numbers: compile does not read onlineRunsPerCopy, and the compiled prover is stateless, samples its copy at random and does not count replies.
The table lists every party of the statements: its name, its Lean type, who chooses it, what it is given, what it returns, and what limits it. The model, the honest committer, the honest prover and the verifier are fields of the record ArgumentSystem; the hash function is sampled uniformly at random; the others are quantified in the statements.
| Role | In Lean | Chosen by | Is given | Returns | Limit |
|---|---|---|---|---|---|
| hash function | Hash | sampled uniformly at random, in every probability | a bit string | 256 bits | the same answer to the same query |
| model | nextToken : Weights → List Token → Option Token | the argument system | weights; tokens | the next token, or nothing | a function: no query, no randomness |
| honest committer |
| the argument system | weights | its randomness, which it keeps; a commitment, which it publishes | none stated |
| honest prover | prove : Weights → CommitmentRandomness → List Token → List Token → RandomizedAlgorithm Proof | the argument system | the weights, the committer's randomness, a prompt, output tokens | a proof | none stated |
| verifier | verify : Commitment → List Token → List Token → Proof → DeterministicAlgorithm Bool | the argument system | a commitment, a prompt, output tokens, a proof | accept or reject | deterministic |
| committer, in §1 | committer : RandomizedAlgorithm (Commitment × State) | arbitrary: for all | nothing | a commitment and a state | at most committerQueries queries |
| prover, in §1 | prover : State → RandomizedAlgorithm (List Token × List Token × system.Proof) | arbitrary: for all | the committer's state | a prompt, output tokens, a proof | at most proverQueries queries |
| opener, in §1.1 | opener : State → RandomizedAlgorithm (system.Weights × system.CommitmentRandomness) | arbitrary: for all | the committer's state | weights and commitment randomness | at most proverQueries queries |
| extractor | extractor : Commitment → QueryLog → Option system.Weights | one for all committers: exists | a commitment; the committer's query log | weights, or nothing | a function: no query, no randomness; no bound on running time |
| adversary, in the last form of §1.1 | adversary : RandomizedAlgorithm (Commitment × (system.Weights × system.CommitmentRandomness) × (List Token × List Token × system.Proof)) | arbitrary: for all | nothing | a commitment, weights with commitment randomness, a prompt, output tokens, a proof | at most queries queries |
| malicious verifier, in §6.3 | verifier : Commitment → MaliciousVerifier system.Proof | arbitrary: for all; not the verifier of the argument system |
the commitment; then, for each proof that it requests, the request and the proof in both theorems the proof is what the compiled prover returns: a proof or the empty proof | nothing; the experiment returns its view | at most queries queries in all; at most proofCount proofs |
| chooser | chooser : View system.Proof → Option (List Token × List Token) |
arbitrary: for all
the chooser may depend on the weights | the verifier's view so far | the next request, or nothing | a function; the same in both experiments |
| simulator | simulator : Simulator system.PublicParameters system.Proof |
one for all weights, choosers and verifiers: exists in the theorems on zero knowledge it may depend on the public files |
the public parameters (in these theorems: none) and the largest number of proofs then hash queries then, for each proof, the request (in the theorem | a commitment; answers; proofs | no bound on running time; never two answers to one query |
The model has one hash function, sampled uniformly at random among all functions from bit strings to 256 bits (the random oracle model). Every algorithm of the statements has query access to it; the statements bound the number of queries and, in zero knowledge, of replies, and nothing else. In the simulated experiment of zero knowledge the simulator answers the hash queries in the hash function's place.
Two types of algorithm, and where the hash function is sampled. RandomizedAlgorithm and DeterministicAlgorithm are both types of oracle algorithm: an algorithm of either type may query the hash function and continue with the answer, but neither fixes nor samples it. "Randomized" refers to the algorithm's own coins: a RandomizedAlgorithm may also sample random numbers of its own, whereas a DeterministicAlgorithm, the type of verify and of commit, may not. toRandomized views a deterministic algorithm as a step of an experiment and adds no randomness. In the statements on this page the hash function is sampled in Prob: the probability is taken over uniformHash, the uniform distribution on hash functions, and over the experiment's own random choices. evaluate instantiates the hash function with a concrete one, as in leanVerifier (§5).
The second hash function. FlashProve's second hash function is a different function: it is fixed, and it is part of the argument system. The model does not sample it. §5 states what the theorems assume about it (nothing) and what the Fiat–Shamir heuristic assumes about it.
a function from bit strings (BitString) to 256 bits (Digest)
a probability measure on hash functions
the product measure: at each bit string a uniform value of 256 bits, independently of the others
an algorithm with a result in α: one of
it stops with a result
it queries the hash function at a bit string and continues with the answer
it samples a number from 0 to bound uniformly and continues with it
a randomized algorithm, and a second one that depends on the first's result
the first has stopped with a result: run the second on that result
the first makes a query: make it, and continue in the same way with the answer
the first samples a number: sample it, and continue in the same way
the notation do for randomized algorithms:
pure: stop with a result
←: one algorithm after another
for an algorithm and a number of queries
stopped: true
a query, and the number is 0: false
a query, and the number n is at least 1: every continuation makes at most n − 1 queries
a sampling step: every continuation meets the same bound
the same algorithm, returning its result together with its query log (QueryLog): its queries with their answers, in order
stopped: the empty log
a query: the query with its answer, then the log of the continuation
a sampling step: the log of the continuation
for a hash function hash: the distribution of the result
stopped: the result, with probability 1
a query: continue with the answer of hash
a sampling step: the average, over the bound + 1 numbers, of the continuations' distributions
a distribution and an event (a set of results)
the probability of the event
an experiment (a randomized algorithm) and an event (a set of results)
the expectation, over a uniformly random hash function (uniformHash), of the probability that the result under that hash function is in the event (RandomizedAlgorithm.run, eventProbability)
The random oracle model enters the statements through this definition, which samples the hash function once for the whole experiment.
an algorithm with a result in α: one of
it stops with a result
it queries the hash function at a bit string and continues with the answer
a hash function
stopped: the result
a query: continue with the hash function's answer
converts a deterministic algorithm into a randomized algorithm (RandomizedAlgorithm) that samples nothing
stopped: return the result
a query: make it, continue with the answer
This section lists the definitions that are named in a card's Lean code and have no card of their own, arranged by folder. Each row gives the declaration's keyword, its name, the first sentence of its comment in the Lean file (if it has one) and the line number. These comments were written for the library's authors, and Lean does not check them. Click a name to read its Lean code.
ScalesAndPolicy of Inst/Model/ProgTests.lean:32KeyPub of the written sizes: KeyPub.of (E2E/KeyBook.lean) at keyFull and at its number of answers to an OOD sample.:127ride for the sending of the multiplicities: at message number 1, from 0, a fold's fresh table of 4 rounds, with h = 4; none at every other number.:125ride for W's sending: at message number 1, from 0, a fold's fresh table of 5 rounds, with h = 1; none at every other number.:129withTestsOnUAndOmega lays it.:65withTestsOnUAndOmega lays it.:70rowOfPoint of all parts of all lookups, in the lookups' and the parts' order.:108KeyInst: both copies of the answers are the key's list of answers; the copy's number is 0.:288data gives no entry.:121ride).:128ride).:144settingsArraysOf, IntegerModel/Arrays/OfTensors.lean).:51place.:209kindsBeforeBatching lays once, first in the head's segment.:242Seat, K3Lookup.lean, at HeardG).:357Block.claims.:64Block.after.:70Block.after, behind k8LsTail: the smallness test's sixteen tests on the sums, with the rows' weights set between them (testsP, SelfRows.lean).:77Block.oracles says of it.:100frontE).:111Proof.SharedEnd; nothing unless all is tested.:247firstChainEnded; no ledger is open; all lookups are laid; the ranges' group is there; it and every group behind it but the last one have begun their tests and hold no open row.:76tests of Johnson/Desc/K12/Seat/Fill.lean, at these places' numbers).:79Aff), or one that reads the planes (PlaneClaim).:59Wf.lookupsOf) at the one-time chain's public values.:66ChainState), with the lookups' record.:100Model.Verify.planned, in its order, and the list of the sendings, of which the key's three and the proof's three are kept; the fourth, the entry chain's, is made and dropped (the record has no field for it).:45Key.startOf).:69wanted.:63owed.:74wanted.:76wanted.:86owed.:95owed.:103laidPOf, so that a test can make the public record of the three files anew without naming a hash.:95publicOf (OnBytes/Model/VerifyPublic.lean) with the second hash function as the argument o.:125plannedAt (OnBytes/Tie/ChainsAtCfg.lean) with the second hash function as the argument o.:180FileDescription Inst.:202built, first and W are computed from the public files alone.:21WiderIn.:74bookRaw, then the book's own tests.:154n rounds in which the prover sends nothing.:176ofF, ofE).:229Placed.parts).:342ch, from 0.:433ch, from 0, may be given, by address: the first chain those of its own parts; the shared chain those of its own parts; the second chain those of all three.:444num of den.:648Block.lift (Johnson/Desc/Block.lean) places a sub-protocol in a wider state: one definition, with type parameters of its own, can be used at many places.:702Kind (Johnson/Desc/Block.lean) is for the sub-protocol.:759ofF, OnBytes/Slice/Field.lean).:889unfit.:916Seen.:1080groupsOf (Johnson/Desc/Block.lean) has them.:1154run prepares before it plays: the two inputs, and the three chains' rounds, each with its move and its coins supplied.:1295Lot, LotCore.lean), from the public part and the segments' data.:1517onlineDescription: the table's key in the instance's public part.:1538K11.parOf, Johnson/Desc/ProofFile/Lot/K11.lean).:133rowsOf at the two readers.:179Local.x, Honest/Frame.lean): so a message whose data depends on words of the request has a place, and no reader is given a fixed value for them.:112Fall, Honest/Side.lean): most descriptions' chains have none.:116Fmt.Drawn (what the format says was drawn), as the library's drawnSL reads it.:116ChainProgress.heard returns an error (a column of a table that is not available).:71ChainProgress.say; the round's fixed substitute if that returns an error; none if there is no Step.:77Told), marked as made by no prover's side.:115none) if either earlier chain has been rejected, or if the description's start of the second chain rejects.:126Step.hear.:197onlineDescription uses.:34secondHashFunction, OnBytes/Hash/SecondHashFunction.lean): from a number and bytes to bytes.:188codingHonest at cellWords.:169otherLinesOf) is not the reference's.:282sendsOf make of the three public files.:384VerifierAndGoals.verify takes it at VerifierAndGoals.atSecondHashFunction VerifierAndGoals.theDescription.:113rideOf at letsThe.:54theDescription: that of verdictFrom, and reject where the public files are in scope and protocolDataWellFormed rejects them (theDescription_dead).:102PV.Front.KFull (a function of the data alone), and at least 139.:159InnerCompilerInput, of which innerCompiledVerifier_sound speaks.:214innerCompiledVerifier takes from the prover's side at the protocols F: further tokens, a key and a proof.:339ansL of the record; the copy's number is not tested.:161wqX at the same letters.:52SgX.:58Sz.ix, with the sample map Z in the place of Sample.nil.:97LdIx.dec, a constrained minimum): of ALL tables of full messages whose message parts have the record's answers at the record's seed, the one whose code words are nearest to the table, ties broken by a fixed order (ix.rank); its message parts, if it is within eM columns; else nothing.:117LdIx.Coll).:125GF.:45recZ of one row, written after the programs': 402,653,184 entries, 29 coordinates, one answer.:82Params.entrySpecOf, at an empty statement.:183annT, annL.:119a that begins at byte off, as sixteen words.:98blake2b_init_param on the blake2b_param that blake2b_init (for keylen = 0) or blake2b_init_key in blake2b-ref.c of the BLAKE2 reference source code package fills in.:170PQ.CK) of the pulled form.:108e0 and the kind nothing there is exactly one verifier message (front).:154RandomizedAlgorithm.:52algorithm and continues with the number 0 wherever algorithm samples a number.:21haltW, Inst/Model/SanityRef.lean; the proof of Cm.empty_language, Cm/RelTrueExp.lean).:144The Lean code uses short names for some types, fields and variables, such as I, lam, enc and Pub. The folded section below lists some of them with their meanings.
Ans: the out-of-domain answers.aT: the offline IOP's round marking (which rounds a batch shares).Bd: the type of a leaf's body (what the leaf contains in addition to its salt).Digest: an output of the hash function (256 bits).early: the early part early x of an instance x, which the first query of a Fiat–Shamir chain contains (HolographicProtocol, §3).enc: several meanings, including the encoder in ConfigurationWithOutOfDomainSample (it maps a message and randomness to an encoding) and, as an argument of verifyDigestKey, Arg.digestKey and Rec.tokenArgumentSystem, the code of a key; the commitment is the hash function's answer at this code.Further: the return type of the second public reading.honestOfflineProver, honestLinkProver, honestOnlineBatchProver: §6.4.I: the indices (for FlashProve, the committed data, derived from the weights).Inst: either the namespace and folder of the integer model's definitions, or the instance (request file bytes, table key, reply file bytes).Isk: the prover's key (the index and the tables of its stored copies); it does not contain the first table.lam: the length in bits of a digest; 256 in the six theorems.late: the number of the late round, if there is one; the query of that round contains the whole instance (HolographicProtocol, §3).lowKey: the whole key's root and out-of-domain sample, for the compiled verifier.lowPrf: the whole key and a proof, written as the compiled verifier's typed proof.n: the encoding's length.N: the batch size (the number of batch positions in one run of the online IOP).ofUpload: a ZKCP oracle algorithm rewritten as a RandomizedAlgorithm.Pub: either three public files as bytes (parameter, layout and scale files), or what the description takes from the three public files.Rec: the out-of-domain sample (also a namespace: Rec.tokenArgumentSystem).Seed: the out-of-domain seeds.Wn: the witness type of the relations.X: the instances (an instance is built from a request and further tokens).ZKCP.Arg (ZKCP: zero-knowledge commit-and-prove): an argument consisting of three oracle algorithms: committer C, prover P, verifier V.sound depends on about 17,000 named declarations of this library. The general parts are small: Sound depends on 28, the model on about 160, blake2bHash on about 130, compile on about 720. Three declarations, whose dependencies overlap, account for nearly all the rest: FlashProve's description (flashProveDescription, about 12,000), the test on the public files (protocolDataWellFormed, about 9,100) and the honest provers and settings (honestProversAndSettings, about 16,000).sound, about 11,000 have their own declaration line, and about 9,100 of these are declared with def.the argument system rejectAll, whose verifier rejects every proof, satisfies Sound with ε = 0
sound, soundAndBinding, completeOnCanServe, zeroKnowledgeOnCanServe, refusedHandsOutNoProof, repliesFit, with the definition leanVerifier. These seven are this library's own wording of what is to be proved. So are the statements of soundness, completeness and zero knowledge as an IOP, which this page does not print (their files: lean/LIMITS.md, under "That a statement says what is meant").blake2bHash behaves like a random function that is independent of it (The second hash function). None of these uses is essential to the protocol: the digest of the request is redundant, and the digests of public data can be made with the main hash function. The second hash function will be removed in a future version.exactMatch of FilesTaken, §4.4): the verifier does not check this, and the theorem sound applies only to such files (A public setup). The serving scripts use a different, tolerant policy, and the six theorems do not apply to it.PublicSetup). No theorem or test on this page determines which scale files have such scales.RandomizedAlgorithm, §8; MaliciousVerifier, §6.2).ArgumentSystem.accepts, or that a prover program computes prove. These are facts about programs. The honest prover in these statements is a definition, not a program.Sound does not count its acceptance as a failure.Sound concerns one proof. For N proofs submitted together, a union bound gives N times the error of one proof, evaluated at the number of hash queries of the whole list. For proofs checked one after another, no bound is stated.requestOutcome).finalSoundnessError q, about q / 2^124 + 2^-101, is a bound on the soundness error, not a security level (see the card sound).filesInUse_stored), whose scale file is that of an example with synthetic weights (according to the header of Ladder/Stored.lean, not a theorem).protocolDataWellFormed) and the honest provers and settings (honestProversAndSettings). Their sizes are under “Counts of declarations” above.noncomputable section. Many definitions on the cards are inside such a section, which no card shows, so a def on a card may be one that Lean does not compile. leanVerifier, flashProve, compile, compiledVerifier and finalVerifierProgram are inside one; verdictOf, whose three parts the command lean-verify evaluates, is not.sound depends on. Among other things, it uses theorems of coding theory from files that are adapted from others' work (lean/CREDITS.md). Nothing in these coding-theory files has a card here. The axioms that Lean lists for sound cover them, as they cover every file on which the proof depends.G3'pol, G7', G7'bits and the six Package… statements (Ladder.lean, Ladder/Bits.lean, Ladder/Package.lean). None of them is used in the statements of the six theorems or in the definitions under these. The plain properties Complete and ZeroKnowledge are discussed in §6: ZeroKnowledge is not proved for any system, and Complete is proved only for a verifier that accepts everything (acceptAll_complete).The assumptions Files fixed first and Hash values treated alike (above) can be judged only from the protocol's definitions. A reader can check the following.
We have read FlashProve's own definitions with both questions in mind. The findings below come from reading the definitions, not from theorems.
verifyDigestKey). The definitions used by verify do contain one explicit answer of the concrete hash function, namely a digest of the stored public files; as far as we can tell from reading, it is not used anywhere.No attack is known, and neither point is settled by a theorem (lean/GAPS.md, 5 and 51).
This page prints 1,558 declarations. The statement of the theorem sound depends on about 17,000 named declarations of the library (counted as described in §11); the page prints those nearest to it, and the protocol's three IOPs, the compiler, BLAKE2b and the integer model. The rest are in the files, most of them under Johnson/Desc/, OnBytes/Model/, OnBytes/Params/, OnBytes/Iop/ and Inst/Model/.
A protocol is a linkable holographic IOP, from which the verifier is built. It makes no queries to the random oracle. It has an encoder that encodes an index, here the weights, as an oracle string, with a decoder; an out-of-domain sample on each encoding; and three interactive oracle proofs: offline, link and online.
An IOP is defined for a batch of instances: one prover serves them together, and each instance has its own verifier.
This appendix gives the three IOPs from which FlashProve.flashProveDescription is assembled. The first folded sections contain the Lean definitions nearest to the six theorems: the verifier's side, the public files, the honest provers and settings. Next are the terms of this appendix, a count of sub-protocols by kind, and each IOP, sub-protocol by sub-protocol. The last folded sections contain the protocol itself: the format in which an IOP is written, how a written IOP is run, the public checks on it, the two decisions, the three IOPs chain by chain, the kinds of sub-protocol, and the assembly.
This appendix shows the verifier's side of the protocol and, in the folds named here, the honest provers. The honest provers and settings of the six theorems are on the card honestProversAndSettings, in What the theorems refer to.
honestProvers.linkSide. The last of them contains the types of which these two provers are made, and can be read first.The fixed-message provers, the constant committer and the constant prover in this appendix supply fields of the protocol's record, which the types need and which neither compile nor the verifier reads. Fixed-message provers are provers that send the same messages whatever the weights, and so show nothing of them; at public files in use (FilesInUse, §4.4) the protocol's honest provers are different provers: only where a function that makes them refuses do they fall back on these. The constant committer is a committer that returns one constant whatever the weights, and so commits to nothing; the committer of the six theorems is a different committer: the one that compile makes (Johnson/Face/Compiler.lean), which encodes the weights and hashes the key. The constant prover returns empty strings.
Run one algorithm, then another on its result.
FlashProve's public side, obtained from the description FlashProve.flashProveDescription at the public files and settings, with the map from weights to indices. Its fields include the protocol, its round markings and whether the verifier takes these public files at all (filesInScope).
the file's variables
Constructs a public side from a description, public files, settings and a map from weights to indices.
the file's variables
The layout consisting of the fields of the inner compiler's input that a description specifies.
the file's variables
A proof as the compiled verifier reads it: further tokens, a key and a proof.
Three public files, as bytes: the parameter file, the layout file and the scale file.
The public files that verify takes: it rejects on all others. The six theorems require more: FilesTaken requires that InScope is true (field inScope) and imposes further conditions.
the layout file is that of the stored full-size example (Ladder/Stored.lean)
the reader (readFiles) accepts the three files
the parameter file equals that example's byte for byte, except for the eight free numbers (FreeLines), which are written as the reader read them; and 2^8 ≤ theta. Hence only the scale file and these eight numbers are free, within what the reader accepts. All security settings, the version line and the layout are fixed, so files of a changed format are out of scope.
Policies that leave every counted token unconstrained remain in scope: (256, 256, 1) for requests with one counted token, and theta = C with cap = 1,024 for every request.
Why 2^8 ≤ theta: every token costs at least 2^8. For smaller theta, no output with a counted token meets the policy (theta < C), or the policy bounds little except the number of counted tokens (theta = C). ("Cost" and "counted token": see MeetsPolicy.)
The digest of the three public files, obtained by querying the hash function.
The string that the format hashes to obtain the digest of the three public files: Fmt.oStr (Fmt/Rules23.lean) applied to their bytes with half 0, number 169, tree 0, index 2. Fmt.zero32 is the "start" argument of that call, not a digest.
The description of FlashProve's protocol. A black box on this page: it depends on about 12,000 named declarations of this library, of which the page shows a few hundred.
The description built from the data L at each set of public files (dataAtFiles), with proofs in the byte form FormBytes: the five byte strings of the parsed files, and the further tokens.
The library's values for all parameters of the description.
All parameters of flashProveData, with an extractor that finds nothing.
The three public files, as one OnBytes.K.Pub value.
the file's variables
The parsed files as they are stored on disk, and the further tokens.
the file's variables
One round: a prover message, consisting of an oracle part and a plain part that is read in full, followed by a challenge. The compiler (Compile/) takes only oracles that are strings. Linear oracles also fit the type, but no other file of this library mentions them.
the oracle part, an abstract type. For oracles that are strings, Orc = ∀ p, Sym p; for linear oracles, a vector. A message without oracles has Orc = Unit
the queries p. For linear oracles, linear functionals. A message without oracles has Pos = Empty
the answers to a query p
how Orc is read by queries. For oracles that are strings, this is function application (see Round.IsPoint)
the plain part. A message without a plain part has Plain = Unit
the challenge, uniform in the finite set Chal. A round without a challenge has Chal = Unit
a fixed message of the right format: its oracle part and its plain part
the list of all challenges; Chal is not empty
the file's variables
The list of a protocol's rounds, in order.
For each round, its kind (local or shared) and how its message splits into the shared part and one batch position's part.
The test on the public files: protocolDataWellFormedAt (folded section How FlashProve's description is assembled) instantiated with the second hash function. It is a black box on this page: it depends on about 9,100 named declarations of this library, of which the page shows about two hundred. If files in scope fail it, the verifier rejects everything. Soundness holds without it: the proof of sound uses FilesTaken alone.
The link IOP's chain. Its end (chainEnd) is given the rounds of exactly the sub-protocols in the field back.
The inner compiler's input whose protocol is made of the three IOPs: offline, link and online.
the file's variables
The key: the root of the first table, and its out-of-domain sample.
the file's variables
A proof consists of the number of the stored copy; the offline IOP's proof on the first table; a copy's root, its out-of-domain sample and the link IOP's proof; and the online IOP's proof; each of the three IOPs' proofs may be missing (an Option).
The test on first hash blocks for given public files: a nonce search queries the other blocks of a try only if its first block passes.
The reader of the public files returns the table of scales and the policy specified by the parameter file and the scale file. It rejects files that it cannot read, scales that are not valid, a policy that violates one of C < 2^32, theta ≤ C and cap ≤ 1,024 (both tested by Inst.Model.Lawful), and a parameter file in which a line about the model, other than its sizes and scales, differs from the reference model's. It does not read the layout file.
The settings: the scales of the 48 layers, the final normalization, and the three numbers of the acceptance policy.
The three numbers of the acceptance policy: the clip, the bound on the mean cost, the limit on the number of positions above the clip.
The policy of exact match: C = θ = 2^8, cap = 0.
The integer model's settings, computed from what the file reader returned.
The numbers of the parameter file that InScope leaves free: the constants of the two normalizations of a layer and of the final normalization (eps1, eps2, epsF), the final normalization's exponent and shift (MF, KF), and the acceptance policy (C, theta, cap). Each of eps1, eps2 and epsF is written on two lines: _lo, the value modulo 2^32, and _hi, the quotient by 2^32.
The eight free numbers of the parameter file, taken from a value returned by readFiles, which writes eps1 and eps2 into the two normalizations of every layer; here they are read from the first layer.
The stored example's parameter file with the eleven lines of the free numbers set to the given values, written in decimal.
The three public files, as bytes: the parameter file (pol), the layout file (lay) and the scale file (KL).
The honest provers and settings at every set of public files and model settings.
the file's variables
The honest provers and settings: honestProversAndSettingsAtFiles applied to parts files and to compiledPartAtHonestProvers, what compilation adds to the honest provers.
FlashProve's honest provers and settings, built from the protocol's honest provers.
A fixed fall-back request, used when no instance can be built from the given request.
The protocol's honest provers, which refuse when the request is not served.
the file's variables
The same provers, except that for a request that is not served the online prover aborts whatever the verifier's messages are: it shows nothing. For a served request nothing changes.
A served instance: for some weights with the given index, some prompt and output tokens form a request, the model's result on it is these output tokens, and the verifier's builder maps them to the instance.
the file's variables
The three provers, one for each IOP of the protocol: offlineProver, linkProver and onlineProver.
the file's variables
The type of a triple of honest provers, one for each of the protocol's three IOPs. T is the offline prover (IOP offline), Lk the link prover, and B the online prover (the IOP of one batch position, onlineBatch.loc). The private input is the index with its encoding randomness and seed; the link prover has the randomness and seeds of both tables, and the online prover also has the copy's number (a copy is a further encoding of the index).
The protocol structure at the public files Z, with its three IOPs: offline, link, and onlineBatch (a batch of requests). It is the structure (flashProveDescription.F files).withProvers (flashProveDescription.P files) over which FlashProve's provers are defined. Its type HolographicProtocol is a holographic interactive oracle proof in which the party that encodes the index is not trusted, with an out-of-domain sample after each encoded index.
the file's variables
If the public files yield a description, offlineProverWithEncodedTable with Parts.prover of that description; otherwise, the prover that sends the fixed messages.
the file's variables
The link's honest prover at committerCoinCountLessOne, the number of the committer's coins minus one.
the file's variables
The online provers, one for each copy number, from the output of onlineMaker; if it, placesOfMade or onlineFirstChainAt fails, the provers that send the fixed messages.
the file's variables
The arguments of honestProvers other than the public files, all of which belong to the offline prover: its coin counts, its two state types and the type LookupInput, its value senders of type KeyParts, and what its test on the ranges reads.
the file's variables
The value of Parts at given public files. If the files yield a description, the field senders is offlineSenders of that description and the list of groups rangeGroups is multiplicitiesGroups of its source; otherwise senders is fallbackSenders and rangeGroups is empty. The other fields do not depend on the description: book, the two states (both Unit), LookupInput and rangeEntry.
the file's variables
The library's three provers as a value of HonestProvers.
the file's variables
The number of the committer's coins, less one: the product of the sizes of the two enumerations riDigits and saltsDigits, less one.
What compilation adds to the honest provers, for given public files and settings.
the file's variables
What compilation adds at the honest provers.
the file's variables
The settings that the honest committer and prover choose in addition to their three provers, given a hash layout layout and honest provers provers.
leafFiller: a leaf body of the layout
searchLimitOffline, searchLimitLink, searchLimitOnline: in round i the search for a nonce may try limit(i) + 1 nonces
furtherCopies: there are furtherCopies + 1 copies
copyNumber: the number of the copy at a position in the key's list; it is public
RunValues: strings determined by a prover's coins and also sent by the prover in the clear; wellFormed: a condition on them
runValuesOffline, runValuesLink, runValuesOnline: these strings as functions of the coins of the offline, link and online prover, respectively
readOffline, readLink, readOnline: these strings as functions of the parts sent in the clear in the offline, link and online IOP, respectively
The public prefixes of a compiled run's salts (saltStartOffline, saltStartLink, saltStartOnline) are computed from them.
slotTail: a bit string for each number; windowFiller: a bit string
coinNumbers (CoinNums): the public prefix of a table's salt, the free bits of a salt, paddings and batch positions
The verifier does not read any of these fields.
At zeroSaltStarts, RunValues is Unit and the prefixes are constants.
the file's variables
The protocol of FlashProve at public files.
the file's variables
A value of FlashProve's public reading.
the file's variables
The layout of FlashProve at a value of the public reading.
the file's variables
The settings of FlashProve, for all public files, all values of the reading and any provers. There is one copy, numbered 0. The salts' prefixes, the search limits and the bits that follow a batch position's value are arguments of the definition. The prefix of a table's salts depends on the digest given by the reading.
the file's variables
The settings for any layout, given the salts' prefixes, the limits, the copies, the coin numbers and the public prefix of a table's salts. windowFiller has as many bits as the free part of a leaf's salt.
the file's variables
The three search limits: in round i a search may try limit(i) + 1 nonces.
The search limits of FlashProve: 2 ^ (work + 6) tries in a round with work bits of proof of work.
the file's variables
The honest committer samples one number from 0 to this bound.
The proofs open no more columns of each table than its budget, the total number of its columns that may be read:
furtherCopies: the number of further copiesonlineRunsPerCopy: the number of runs of the online IOP on one copyindexPrivacyNumbers onlineRunsPerCopy 0 0 0 0 0 0: the numbers of the next card; the six zeros are errors and measures, which this definition does not useon the first table, the bounds on the columns opened by the offline proof and by one link proof per copy: 62 + (furtherCopies + 1) · 62 is at most 44,040,191
on a copy, the bounds on the columns opened by its link proof and by its online runs: 62 + onlineRunsPerCopy · 64 is at most 44,040,191
Of the links, only the one that made a copy has its columns counted on that copy.
The numbers:
readsG_atFiles, one_atFiles)The honest committer and prover may fail with at most this probability. This allows for an honest proof-of-work search that aborts after a bounded number of attempts.
The maximum number of hash queries that one run each of the honest sampler, committer and prover may make together. The value is a design choice.
RepliesFit imposes this bound, via WithinBudget, on the total for one run each of the sampler, the committer and the prover (one commitment and one request, not a batch)bindingErrorInQueries it accounts for one run of the committercommit and of D's own parser, for files in scope2^64 hash queries. Beyond this number the zero-knowledge theorems give no bound. The statements of Ladder.lean with a constant upper bound on their error, which are not among the six theorems, say nothing about an adversary that makes more queries.
FlashProve's value of CompilerWiring: the layouts as the committer and the prover read them, and the instance used when no instance can be built from the request.
the file's variables
Constructs a CompilerWiring from a fall-back instance and a family of layouts that agrees with the description's input.
The writer outputs a proof's files as they are stored on disk: five byte strings (kb, sb, leaf, seeds, pb) and the further tokens. If a proof string is missing, it outputs an empty form.
the file's variables
The proof format given by a writer and a parser of a description.
the file's variables
Puts the three provers into the structure ThreeProvers (folded section The three honest provers of the interactive protocol). The online prover is given as a family indexed by copy number, and is combined into one prover that reads the number.
The type of indices: the matrices of the full-size shape over the extension field.
the file's variables
An honest prover of an interactive oracle proof: its type of coins; the external strings associated with the private input; its strategy; the public part of its abort set, which depends only on the challenges; and the rest, which may depend on the private input and the instance.
the file's variables
The honest prover of a protocol with batch positions. A batch position is one entry of a batch (one request).
the shared part's coins
one batch position's coins
the external strings
the shared part's strategy
one batch position's strategy
the public abort set of one batch position
the rest of the abort set of one batch position, which may depend on the private input and the instance
a public test on the shared challenges; where it returns true, every batch position is withheld
the file's variables
Like Iop.Honest, except that the external strings, the strategy and the rest of the abort set depend on the copy number; the type of coins and the public part of the abort set do not.
the file's variables
Provers that send, in every round, the message fixed by the round's shape.
The constant family: the given honest prover for every copy number.
the file's variables
Computes the offline IOP's description from the three public files, or returns an error, using the reader and the maker of that description.
the file's variables
The arguments from which the offline IOP's description is built (those of keyFileDescription): source; numbers, the numbers of the place of the test on the ranges; later, the numbers of the places of the three later proximity tests.
The offline IOP's description: the verifier's protocol for the offline part, written as data.
the file's variables
The offline prover for a description: keyProver applied to senders, with the four proximity tests set by withTests.
the file's variables
The offline prover, built from the fields of KeyParts.
the first chain: the index-mask message, the multiplicities, two lookups, the test on the ranges, the batching, the message W
the shared chain: its own rounds and two oracle messages, then two proximity tests
the second chain: one proximity test
what the second chain's sides are given at their start
In these folded sections the chains are named after their Lean fields first, shared and second. These are chains 1, 2 and 3 of the table of terms, so "the second chain" here is the table's third chain.
In a Lean name, K followed by a number denotes a kind of sub-protocol; the fifteen kinds are listed below in this appendix. The kinds here are oracle message with out-of-domain sample (K1; a "sending" in Lean names), product-tree lookup argument (K3), proximity test with linear constraints (K12), committed-table claim merge (K13; "the batching" in these folded sections) and committed-table claim reduction (K14; the shared chain's own rounds in these folded sections). The two sub-protocols of K14.proverSidesOfSharedSendings are of kind K1.
The offline prover's arguments: 25 fields, among them the stored table's columns, the readers, the oracle messages, the lookups, the proximity tests, the batching and the shared chain's data.
the file's variables
Sets the four proximity tests in senders: the test on the ranges, the tests on the groups U and Omega, and the test of the second chain.
the file's variables
The data of the offline prover's proximity test on the ranges: its parameters, what has been sent, and the state on entry.
the file's variables
The offline prover's proximity test of the second chain, as a side, with a guard: each move returns an error if the field for the opened columns is absent (none).
the file's variables
Sets the fields onU and onOmega: the two tests of the shared chain.
the file's variables
The offline prover's test on the group U, as a side.
the file's variables
The offline prover's test on the group Omega, as a side, with a guard: each move returns an error if the field for the opened columns is absent (none).
the file's variables
The parameters of the offline prover's test on the group U, at its place in the shared chain.
the file's variables
The parameters of the offline prover's test on the group Omega, at its place in the shared chain, computed from the description's numbers for Omega, or from U's numbers if the description has none.
The numbers of a proximity test at a place, as the verifier's description reads them (P12: a proximity test's parameters). If the place's chain differs from the chain of the numbers, or the numbers yield no rounds, the value is noP12 at that place, in which all other numbers are 0, all lists are empty and both flags are false.
the file's variables
The value of KeyParts for a description: withSendingsAndLookups and then withStoredColumnsAndPlan, applied to the fixed value fixedKeyParts. These two and withTests, which is applied to this value later, overwrite all 25 fields.
the file's variables
Sets sixteen fields of KeyParts: the range test and its named index, the state passed on, the three oracle messages of the first chain, the two lookups with their data and witness, and the batching.
the file's variables
The data for sending the index-mask message, which has no main row and contains only coins.
the file's variables
The data for sending the multiplicities message: the bits of the number of times each row of each table occurs in the matrix. It reads the index.
the file's variables
The data for sending the message W: the batching weights on the matrix's rows, times the matrix. It reads the index and the challenges received. If the shape has no message W, indexMaskSending is used instead.
the file's variables
The rows on the matrix at the claims' points, which the batching combines. Their masks and targets are not the verifier's.
the file's variables
Sets five more fields. The stored table's columns are given by storedColumn: the encoding of the index's rows under the committer's coins, at sizes read from the public chains. The index's reader and the committer's coins are arguments; the coins are read at item 0. The public parameters of the shared chain's rounds and oracle messages (the fields lin and send) are computed from public data alone (parKey).
the file's variables
A column of the stored table: at item 0, if the rows fit and the position is below the code's length 2^a, the encoding of the index's rows at the given position; otherwise nothing.
The index's reader: the weights are the first coordinates of the matrix's cells, and 0 outside its shape.
the file's variables
The matrix read from a side's input.
the file's variables
The groups of the multiplicities message.
The offline prover's coin counts at the written sizes: the number of coins of each part. The value is empty if the public data at those sizes are not constructed.
the file's variables
The value of KeyParts for public files that yield no description, built with fixedKeyParts.
the file's variables
A value of KeyParts with fixed fields, built from its six arguments.
the file's variables
The offline prover as an honest prover of the IOP offline at the public files, with its KeyAndJoiningRoundMessages and the encoder's table.
the file's variables
offlineProverAtFilesDecision, with the type of the first prover of the protocol structure.
the file's variables
offlineOneInstanceProverAtFiles, with the type of an honest prover of the offline IOP at the public files.
the file's variables
offlineOneInstanceProver at the public files.
the file's variables
The single-run prover of offlineBatchProver with its instances pulled back along keyInstanceOfOutOfDomainSample.
the file's variables
honestBatchProverOfFile over the offline IOP's description.
the file's variables
The first state of the offline prover's shared chain, computed from the table's TableKey (its item number, out-of-domain seeds and answers).
Thirty-two bytes that the prover sends in a plain round, in place of the hash that the file format has at the start of a chain.
A run value as a byte string.
the file's variables
explicitLinkProver (next card), with its type stated for the link IOP of the structure at the public files Z.
The link IOP's honest prover, given by a next-message function (linkSide).
Coins: the type Kc, which coinsFull maps to the prover's free parameters. The first stage of the link IOP's proximity test samples 97 positions at the full size.
External strings: the two encodings of the index, one under each table's randomness (homeExt). The prover's data: the instance, both encodings and the polynomials of their rows (homeIn).
The online IOP's first chain, computed from the public part, with the function that returns the empty byte string in place of the second hash function. The chain does not depend on this function.
The online provers for a value of type OnlineReturn (the type of what onlineMaker returns), with the places and the first chain as arguments. The definition onlineProver passes the places and the first chain computed from the public part.
the file's variables
A family of online provers: onlineProversAlongInstanceMap instantiated with the library's instance map instanceAsPlainRecord, the online IOP's description (built with OnBytes.secondHashFunction), the prover structure (cmAlong …).proverAt 0 H, the committer's KeyAndJoiningRoundMessages with the copy number in the front round, and the committer's external string.
the file's variables
onlineProversAtOwnInstances, read along the instance map wr, as a family of the protocol for one request.
the file's variables
honestProversByCopyNumber with the online IOP's round data and fixed plain parts.
the file's variables
The family of honest provers for one request, indexed by the copy number n. Member n is the single-run prover of honestBatchProverOfFile: its strategy and abort set Hid are written with J n, that copy's KeyAndJoiningRoundMessages for each value of R₂ and R₃; its coins and public abort set Bad are written with J 0.
the file's variables
onlineProverFromPublicFiles applied to the second hash function OnBytes.secondHashFunction, the three public files and onlineFilling.
the file's variables
The function that builds the online prover from a value P of OnlineProverParts.
it computes the public part Z, the segments' records G at a request of zeros (via blankBy), the description F and the coin counts B
it evaluates the sides of P at Z and G, one list for each of the three chains; each side carries its own place
one of its errors: a side's place is not in its chain
What onlineProverFromPublicFiles returns.
the public part Z
the segments' records at a request of zeros, computed from the public part: G, of type Ground
the description F
the coin counts B
the prover H
its readers readers
the data of its rows rows
the file's variables
OnlineProverWithDescription at the types of onlineFilling.
the file's variables
The value of OnlineProverParts for the online prover: onlineProverPartsInUse, instantiated at the matrices via matrixInput and at the structure's randomness via tableCoins.
The fields from which onlineProverFromPublicFiles builds the online prover.
a request's trace trace
the readers readers
the data of the main rows rows
the range test inRange, and a named element dummy
the encoded index's columns enc
what the parts pass on at the start of the first chain and of the shared chain: own₀, ownShared₀; what the second chain's sides are given at their start: meet
each chain's sides: lots, shared and second
the file's variables
A value of OnlineProverParts, generic in the type W₀ of the private input. The prover's sides of the following are added, in order, to its other fields and sides: the sub-protocols that close a segment, the first chain's proximity test, the tests on the groups U and Omega, the second chain's proximity test, and the sub-protocol that sends the message W.
the file's variables
Five of the lists of sides in onlineProverPartsInUse, one for each of five kinds. No side reads or writes its own state.
oracle message with out-of-domain sample (kind K1): k1
product-tree lookup argument (kind K3): k3
output-head sumchecks (kind K6): k6
output-head committed-table sumcheck (kind K11): k11
committed-table claim merge (kind K13): k13
The functions that onlineProverPartsInUse leaves open.
claims: the claims on the weights (output-head committed-table sumcheck, kind K11)
pile: the rows combined by the committed-table claim merge (kind K13)
req returns a default value
keyOf reads the key points at a segment (attention-segment sumchecks, kind K5)
cells returns nothing
enc returns nothing. onlineProverPartsInUse does not read req, cells or enc: at onlineFilling its trace comes from matrixInput and its encoded columns from encW
What onlineFilling reads from a matrix.
its weights weights
the trace at the index that the matrix represents: trace
the range test inRange: the matrix represents an index
a fixed matrix dummy; onlineProverFromPublicFiles tests whether it is in range
The committer's randomness for a table, as read by the online prover at every item of the statement.
the file's variables
The honest prover of a written IOP, given coin counts B, a prover H and, for each pair of coins, a value J of type KeyAndJoiningRoundMessages.
its two strategies: sharedPartStrategyTrackingVerifier and requestStrategyTrackingVerifier
its abort sets, defined by the prover's abort conditions
the file's variables
The value key given to the prover's sides in the shared chain, and the messages sent in the challenge-free round before each chain.
the value key given to the prover's sides in the shared chain: keyOf
the front round, before the first chain: front
the joining round, before the shared chain: join
the challenge-free round before the second chain: seam
the file's variables
A batch position's strategy.
it sends the front round's plain part
it runs the first chain, updating a ChainProgress after each round
it advances over the sealing round (the first chain's last round, named SEAL), in which it sends nothing; the progress halts unless the test sealQuiet passes
it advances over the shared chain to its end
it sends the plain part of the challenge-free round before the second chain
it runs the second chain, updating a ChainProgress after each round
the file's variables
Prepares a run: it performs all of the run's tests that do not read a challenge and prepares the three chains' rounds. It returns an error if the request has no trace.
the file's variables
The ChainProgress at a chain's start, or a halted ChainProgress if computing it returns an error.
the file's variables
A batch position's strategy over a first or second chain, updating a ChainProgress after each round.
the file's variables
Advances a ChainProgress over a list of Steps and a list of challenges, pair by pair, for the rounds that a batch position does not send itself. If the lists differ in length, it stops at the end of the shorter one and returns the ChainProgress as it is, without calling halt.
the file's variables
After a round's challenge, the round is added to the ChainProgress. If computing the message or adding the round returns an error, the ChainProgress halts but the round is still added. If there is no Step, it halts and no round is added.
the file's variables
The state of a chain between two rounds. The Lean comments call such a state "the walk".
the prover's state mid. A ChainProgress has halted once mid and ver are none
the verifier's state: ver
the place of the first sub-protocol that rejected: refused
the rounds produced so far, what has been read, and the sub-protocols not yet asked: laid, reads, cols, todo, own
the file's variables
A round's message, or an error, given by Step.tell. If mid is none (after the verifier rejects, after ChainProgress.halt, or from a start that returned an error or lacked one of the two states), the message is the round's fixed substitute: zeros in the declared shape.
the file's variables
One round of a chain.
the sub-protocol's name name, the part's address addr, and what the sub-protocol declares for the round: decl, oracles
if a prover's side is defined there, the two abort conditions bad and hid of the round's part
the round's number nth in its part, and whether it is the part's last round (last)
that side's move move
the file's variables
A round's message.
the two abort conditions are checked
the move computes the message; if there is no move, the message is the values of the stored run's round, or is empty
its shape is compared with what the sub-protocol declares
the file's variables
A prover, given as lists of sides. In these folded sections the chains are named after their Lean fields: first, shared and second are chains 1, 2 and 3 of the table of terms, so "the second chain" here is the table's third chain.
the stored tables' columns stored
a request's trace trace
a function key of the public instance; its value is what the shared chain's sides are given of the instance
the range test inRange, and a named element dummy
what the parts pass on at the start of the first chain and of the shared chain: own₀, ownShared₀
the sides of the first, shared and second chains: first, shared, second
what the second chain's sides are given at their start: meet
the file's variables
The input of a side of the first or second chain: the index, the stored tables' pads and encoding randomness, the public instance and the request's trace.
the file's variables
What a side of the shared chain is given: the index, the stored tables' pads and encoding randomness, and a value key, which is what the shared chain may read of the public instance.
The counts of a prover's coins.
for each chain, the parts with coins of their own and their counts: first, shared, second
the entries ahead
for each place, the number of rounds of each of its parts: cuts
the file's variables
The prover's side of a sub-protocol: its place (its address, Place in the Lean code) and a list of parts.
the file's variables
The prover's side of consecutive rounds.
the coins that it takes: takes, spends, carries
its two abort conditions bad and hid, which the Lean comments call stops
for each abort condition, a stated number, which is not a bound: badShare, hidShare
one move for each round: moves
the file's variables
The prover's side of one round.
the message say, computed from the coins, what has been shown and the state
what it passes on: hand
the file's variables
The prover's side of a sub-protocol of the kind "oracle message with out-of-domain sample", at its place: one part.
the file's variables
The prover's side of one lookup, at its place in a chain. Arguments: o, for each phase of the lookup, the two messages whose coins it uses; R, how the lookup's points are read off the challenges received so far; J, each phase's summands; wit, how the lookup's witness is read off the chain's witness; a, the place, the lookup's sizes and the number of rounds before the place.
one part for each phase of the lookup, in the order of the rounds. A phase that has a masked sumcheck has that sumcheck's part; every other phase has a part that sends nothing
the parts neither read nor change the state that the chain's parts pass on
the file's variables
The prover's side of a proximity test, at its place: its first part and the rest.
the file's variables
The prover's side of the committed-table claim merge, at its place.
The fixed instance used when a request is ill-formed and no instance can be built from it.
the file's variables
The layout at a value of the public reading: the seed's queries and the answers' code depend on the reading; the layout of queries does not.
the file's variables
The format's salt prefixes for honestProvers. If honestProvers equals honestProversGivenDescriptions at some arguments, they are formatSaltStartsGivenDescriptions at these arguments, transported along that equality by saltStartsAlongEquation; otherwise they are zeroSaltStarts.
the file's variables
The format's salt prefixes for honestProversGivenDescriptions, with rounds flashRounds and link value linkRun.
the file's variables
Transports salt prefixes along an equality of provers.
the file's variables
Three provers built from parts and from a description, a value of type OnlineReturn (the type of what onlineMaker returns), places and a first chain. They are the value of honestProvers when the public files yield the latter four.
the file's variables
All-zero salt prefixes: every prefix is 256 zeros.
the file's variables
Of the provers, the salt prefixes use only the types of coins, which refuseUnserved leaves unchanged, so they carry over to the provers that refuseUnserved returns.
the file's variables
The public prefixes of a compiled run's salts (called starts in the Lean code), and the run values from which they are computed.
the type of run values RunValues, with the condition wellFormed
the run values determined by each prover's coins
the run values read off each IOP's plain parts
the public prefix of each IOP's salts, from the run values
the file's variables
formatRequestLeafSaltLayout at FlashProve.
the file's variables
What follows a batch position's value, in the format: saltBytes bytes of free bits, then the tail. The batch position is 0 in the offline IOP's and the link IOP's trees.
the file's variables
What follows a batch position's value in a request tree's leaf: free bits, then a public tail.
the number of free bits freeBits. In the byte format: the 8 · saltBytes bits of the stored salt (OnBytes/Prover/Print/Carrier.lean, field rsalt), a value not written here
the public tail tail; in the byte format, the 64-bit index of the batch position's leaf
the public batch position of each of the three kinds of run
the public prefix tableStart of a table's salts, at the digest that the public reading returns
the file's variables
FlashProve's value of the field leafFiller (the body of the leaves beyond the word's length) is the empty list of bits.
the file's variables
The numbers on coins are those of the library at 320 free bits per leaf, with the three public batch positions, one for each kind of run.
the file's variables
The public reading at the all-zero digest and the empty list.
the file's variables
The record from which the compiler builds the honest committer and prover. It is constructed from a layout, the honest provers and the settings s.
the provers, unchanged
the compiled prover withholds on the provers' two abort sets; membership is decided by excluded middle
fields taken from the settings s, the protocol and the layout
every finite type of coins is enumerated in full; salts and run coins have public prefixes and uniform free bits
the file's variables
A scheme of type ZKCP.Arg. Its committer and prover are built from those of readOneF: they query the first hash block of each answer, and the other blocks if the test more returns true on that first block. The committer then queries the hash function for the digest of the key's code (ZKCP.keyDigest). κ maps the key and ϖ the proof. Its verifier is Vf.
The protocol's objects.
| term | what it means in this appendix | the Lean's word |
|---|---|---|
| public files | Three byte strings, parameters of the whole argument system: the parameter file, the layout file and the scale file. | VerifierAndGoals.PublicFiles (pol, lay, KL) |
| IOP | A public-coin interactive oracle proof with a fixed list of rounds, an instance, and external oracle strings that are fixed before the first message. The queried positions are functions of the instance and the challenges (in the prover's oracle messages also of the messages' plain parts). By its type, the decision takes the whole transcript; that it depends on the oracles at the queried positions alone is a separate property, InteractiveOracleProof.IsLocal. | Iop.InteractiveOracleProof |
| configuration | What the three IOPs share: index and instance types, two relations Ryes and Rno (no field relates them; in this protocol they are the same), the encoding of an index as a word of n symbols, seeds and answers, and the index decoder. | Hiop.ConfigurationWithOutOfDomainSample; here DecR.configurationOfStoredTable A R |
| pads | (1) Of the configuration: a value of the type Pad that hold places in the message beside the index. (2) Of a tenant: the entries reserved for its answers (see "seed; answer"). | ConfigurationWithOutOfDomainSample.Pad, hold; Msg.pad |
| committed table | The encoded index as an external oracle string: 2^a symbols, which the verifier queries by position; a is the table depth. What is encoded is a message of field elements, indexed by row and entry. | stored table; encoded index; oneExternalString (2 ^ a) SgX, ConfigurationWithOutOfDomainSample.E0 |
| out-of-domain sample | (1) Of a committed table: seeds, each a point and a nonzero factor, and the answers of every row to each seed. It is part of the instance of each of the three IOPs. In this protocol: one seed, a point of 29 coordinates and a nonzero factor, and one answer for each of the table's 2^v rows. (2) Of a tenant whose flag sampled is set: the verifier samples seeds in the round that sends it, and the prover's next message contains the answers. | (1) record; ConfigurationWithOutOfDomainSample.Rec = Seed × Ans; RecFull (2) SymbolComponent.sampled |
| the offline IOP | Instance: one out-of-domain sample. Oracle: one committed table. Three chains. | Files.key; key file |
| the link IOP | Instance: two out-of-domain samples. Oracles: two committed tables. One chain. In the Lean: the entry file. | Files.entry; entry file; HolographicProtocol.link |
| the online IOP | A request's proof. Instance: a request and one out-of-domain sample. Oracle: one committed table. Three chains. | Files.proof; proof file |
| request | The instance type of the online IOP. It is not printed in this appendix. | XF := Flat.Req |
| full parameter size | The library has two fixed sets of size parameters. This protocol uses the larger one. | frS, frP, recordLines against srS, srP, smallRecordLines |
| statement | (1) A top-level statement: one of the theorems' statements on the argument system, in the main part of this document. (2) A chain's statement, in the byte format: a list of items; a committed table's root is held by one of them, whose number is the table's item. (3) The trivial statement: what an interactive oracle reduction reduces to when nothing is left to prove. | (2) statement, itemRoot (3) Unit, extNone |
How an IOP is written.
| term | what it means in this appendix | the Lean's word |
|---|---|---|
| written IOP | An IOP written in the format that this appendix prints: a value of FileDescription (three chains) or OneChainFileDescription (one chain). | description |
| chain | A consecutive part of an IOP that has a verifier state and a view of its own. The three chains are the fields first, shared, second, here called first, second, third (chains 1, 2, 3). Addresses and before number them 1 to 3; tree sources and BookPlan number them 0 to 2. | Chain |
| segment | A part of a chain in which sub-protocols state claims and one sub-protocol, batch, is handed the function that gathers them. | Link |
| sub-protocol | The unit in which an IOP is written: some rounds, their oracle messages and queries, and a step of the verifier's decision. | Block |
| kind | A family of sub-protocols: fifteen, each with a plain name; in Lean their labels are K1 to K15. (In Lean, Fmt.Kind is another thing, here called the challenge kind: what a round's challenge consists of, read off the round's name by Fmt.kindOf.) | KindName, Kind; Fmt.Kind |
| address | The location of a sub-protocol: chain, segment, number, kind. ("Position" is reserved for a queried position.) | Place |
| verifier state | The value that the verifier's decision carries from one sub-protocol of a chain to the next. | S; "the carried record" |
| claim | A value of the type Cl that a sub-protocol states from the verifier state, to be gathered for its segment's sub-protocol batch. What a claim asserts depends on the written IOP. | Cl; Block.claims |
| schedule; declared round | A chain's schedule lists for each round a name and eleven numbers. A declared round is such an entry together with the committed tables that the round queries, each at its share of the sampled positions, and the Merkle trees that it opens. | plan, Fmt.Entry; Fmt.DeclaredRound |
| matrix entries | Values in {−1, 0, 1} that a round's challenge may hold beside field elements and positions. | Drawn.trits, Entry.trits; challenge kind entries |
| oracle message; tenant | An oracle message is the data under one Merkle root: 2^logLength symbols of a fixed number of words. Its tenants are the data that share its symbols, each with a fixed number of main and mask words in every symbol. A tenant's groups are numbers; the definitions printed here only compare these lists, and only add up the counts of main and mask words. | Oracle; SymbolComponent |
| tree, root, to open | The schedule counts each oracle message as one Merkle root in its round's message; the message's tree is that commitment in the compiled protocol. A committed table has a tree too. "A round opens a tree" means: the verifier queries that oracle at the positions sampled in the round. | Entry.roots, DeclaredRound.opens, Shape |
| shape; column; key; width | A shape is what a round declares of a tree that it opens: depth a, width W, whether it is a committed table's, the tree number. A column is the symbol at one queried position: a key, which names the oracle, the position, and W 64-bit words, each a base-field element. | Fmt.Shape; OpenedColumn |
| round's values; view | A round's values are the items of the prover's message, Merkle roots left out, and the sampled challenge. A view is what the decision sees of one chain: its rounds' values and the list of opened columns. | Fmt.RoundView; Fmt.View |
| public check; file check | A public check is a Boolean that depends on public data alone (the written IOP, the public files, what the planner returns), not on the instance or a view. The file check is the Boolean fileOk that a written IOP has as a field. | "test on the plan"; planOk; fileOk |
From a written IOP to the protocol.
| term | what it means in this appendix | the Lean's word |
|---|---|---|
| round data | For each chain the typed list of rounds from which the IOP's list of rounds is formed, with the table depth. | OnBytes.Maker.WholeD; for the link IOP a list of RD |
| table queries | For the link IOP: which round queries which of the two committed tables, at which share of the round's positions. | XO (round, which, from_, count) |
| challenge-free round | A round in which the prover sends a plain message, no oracle, and the verifier's challenge has one possible value. | plainRound |
| proof-of-work bits | Further bits of a round's challenge, as many as the schedule entry's work. The verifier rejects unless all are 0. | GChal, GChal.pass; Entry.work |
| round marking; N | A marking says of each round of an IOP whether it is shared. N is the batch size: the number of batch positions. Neither is read by the definitions of the format or of the interpreter. | RoundSplits; Files.N |
| hash oracle | The hash function, to which an algorithm has query access only. | DeterministicAlgorithm, .query |
| second hash function | A second hash function of the byte format. The general description (theDescription) takes it as a parameter o; atSecondHashFunction substitutes the concrete function OnBytes.secondHashFunction for o. The six theorems are stated after this substitution. | VerifierAndGoals.SecondHashFunctionType; OnBytes.secondHashFunction |
| a proof as submitted; typed proof | A proof as submitted is a value of the type Form: for this protocol a list of tokens and five byte strings. The parser turns it into a typed proof: further tokens and two values in the compiler's types (KeyRoot, OfflineLinkOnlineProof). | Form, FormBytes; TypedProof |
| compiler | The construction that turns the three IOPs, packed as Iop.HolographicProtocol, and further data into the non-interactive verifier. It is not printed in this appendix. | innerCompiledVerifier, innerInputOfThreeProtocols |
| planner; planner's values | The functions that compute the schedules and sizes from the public files, the second hash function and a value in the digest's place. They are not printed in this appendix. The planner's values are what they return in the type FilesParameters. | Key.madeAt, plannedAtO, ProofFile.Plain.planned; G |
| public parameters; maker | Public parameters are values computed from the public files, or written as constants, on which a written IOP or a sub-protocol depends: sizes, codes, numbers of rounds, declared rounds. A maker is a function that builds a written IOP, with its round data and its decision, from the public files or from public parameters. | Key.Source, H2U.PlaceNums, Key.LaterPlaces; ProofFile.Pub; P14, P15, K1.Par, P2, P12. Makers: keyDataAndDecisionOrRefusalAt, proofDataAndDecisionOrRefusalAt, linkAt and what they call |
| parts | A value of DescriptionData, DescriptionDataAtFiles or DescriptionFields: the components from which a Description is built. | "letters" |
Words of the sub-protocols.
| term | what it means in this appendix | the Lean's word |
|---|---|---|
| group | A set of tenants, opened with one main code and one mask code, on which a proximity test is run. Linear constraints are imposed on a group until its test begins. | Statement.groups; newGroupP, joinP, addRowsP; SymbolComponent.groups |
| tested, untested group | A group is tested once a proximity test has begun on it, untested before. A chain's last sub-protocol rejects if a group is untested, or a sampled tenant is in no tested group; the first two chains leave out one group, which the third chain tests. | inRun; untestedL, untestedButOwnL |
| linear constraint | A linear equation on the entries of tenants, with coefficients that the verifier computes and a target value. It is imposed on a group (after a fold: on the group's folded rows) and not checked there; the group's proximity test takes it as input. (A claim, by contrast, is gathered for its segment's sub-protocol batch.) | OnBytes.Row, GroupRow |
| seed; answer | A seed is a sampled point z with a sampled nonzero factor β. A tenant's answer y to a seed is sent by the prover and gives the linear constraint ⟨eq(z, ·), g⟩ + β·⟨θ, pad⟩ = y, where g is the tenant's entries outside the pads, the pad is a few entries reserved for that answer, and ⟨θ, pad⟩ weights them by the powers of a fixed element θ. A tenant's seeds and answers are its out-of-domain sample. | rounds "SEND seed", "SEND answer"; cutSeeds, sampleRow |
| masked sumcheck | A sumcheck on H + ε·S: the prover first sends the sum μ of a mask polynomial H, then ε is sampled, and the running claim starts at μ + ε·(the claimed sum). In each round the prover sends the round's polynomial without the one coefficient that the running claim fixes, and a challenge is sampled. No equation is checked round by round; one claim or one linear constraint is left. | rounds "PSC …", "FOLD …"; pscBeginAt, pscRound; complete, after, hear |
| batching | One element x is sampled; each of a list of claims or linear constraints is multiplied by a power of x fixed by its number, and all are added into one. | rounds "BAT", "BAT-sigma"; weightNext, addOne; batch; chiOf |
| claim on the committed table | A linear equation ⟨g ⊗ eq(ψ, ·), M⟩ + (a form in mask entries) = target on the matrix M that the table encodes. | TensorRow, WsClaim |
| stage | One level of a proximity test, given by a main code, a mask code and three numbers k, h, t. Every stage but the last has a fold of 1 + k rounds and a code switch of 2 rounds. | Fmt.M1.Stage |
| code switch | Two rounds: the prover sends new oracle messages and seeds are sampled; the prover sends the answers and positions are sampled. Earlier oracle messages of the chain are opened at these positions, and the opened values give linear constraints on the new tenants, imposed on a new group. | K2.codeSwitchKind; the proximity test's "the switch"; switchBehind |
| sealed chain | A chain whose last round is the round named SEAL. | chainEnd … sealed; sealRound |
| adopted | An oracle message of an earlier chain is adopted by a later one: it is entered in the later chain's verifier state under its own tree number and source. Rejected unless it has a tree to itself, has the declared shape, and was sampled in the earlier chain under the same shape and codes. | takeOver; adoptP, elsewhereP |
| array | A numbered datum of the layout. An oracle-message sub-protocol inside a segment marks the arrays in its list as committed. | arrays : Option (List Nat); commitOne |
| rows folded at a point; fold | A table's or a group's rows folded at a point γ: the one row Σ_r eq(r, γ)·row_r. A fold, which occurs at the close of a segment and in a proximity test, is a masked sumcheck of 1 + k rounds whose challenges form such a point. It takes one linear constraint on a group and leaves one linear constraint on the group's rows folded there, its kept tenants and two mask rows. | weights, eqTable; rounds "FOLD epsilon", "FOLD round"; foldD |
| base case | The two rounds that end a proximity test. The prover sends a value τ*, and λ is sampled; the prover sends in the clear the message and tail of w* + λ·w and of u* + λ·u (w, u: the last tenant's main and mask word; w*, u*: a masking tenant's), and t positions are sampled. The oracle message that contains both tenants is opened there. Checked: ⟨c, M0⟩ + ⟨d, M1⟩ = τ* + λ·τ (M0, M1: the two messages sent; c, d, τ: the linear constraint that is left), and at each position x the re-encoded symbol equals w*(x) + λ·w(x), and likewise for u, at x's place in the shorter word. | rounds "BASE lambda", "BASE"; baseDecide, baseChecks |
| product tree | Over 2^D leaves, the binary tree of their products. A claimed value of a level at a point z is moved one level down by a masked sumcheck whose summand is the product of the two children's values vL·vR, followed by one sampled element ξ: the next point is (ξ, r), the next claimed value (1 − ξ)·vL + ξ·vR. | level, stepDown, run; round "LINE" |
| shift | In a lookup argument: a field element (theta in the Lean code) that is sampled before the point α where the parameters say so; the padding values and the table's rows are functions of it. | Face.shifted; round "LKP shift" |
| key | Used in "key file" and as the first component of a column, and nowhere else: a committed table's TableKey is "its out-of-domain seeds and answers"; Product-tree lookup argument's keys are "looked-up values". |
KindName and a Lean definition of that kind (for the last two, the list that contains its sub-protocols).frame).K1; VerifiableInference.Desc.K1.sendOwn): two rounds. The prover sends oracle messages and out-of-domain seeds are sampled; then the prover sends the answers.K2; VerifiableInference.Desc.First.K2.codeSwitchKind): two rounds. The prover sends oracle messages and out-of-domain seeds are sampled; then the prover sends the answers, and positions are sampled at which listed oracle messages of the same chain are opened.K3; VerifiableInference.Desc.K3.lookupKind): rounds that send no oracle message; it states the lists of claims objects, planes and guests in the offline IOP's form, and objects and guests in its other form (VerifiableInference.Desc.K3.Law.blockVia).K4; OnBytes.Desc.First.K4.block): the rounds specific to a segment of layers, in which no oracle message is sent or opened; they leave the lists of claims front and back and a check after the batching.K5; VerifiableInference.Desc.First.Att.P.attentionKind): the rounds specific to an attention segment, which send no oracle message; it takes its lists of claims as an argument.K6; VerifiableInference.Desc.Kinds.Head.kind): the rounds specific to the output head, which send and open no oracle message and leave the lists of claims norm, policy and logits, with join inserted after the first (VerifiableInference.Desc.Kinds.Head.kindWithJoin).K7; VerifiableInference.Desc.Kinds.Reply.kind): one round in which the prover sends the next token as one element and nothing is sampled; the verifier rejects if an element was already stored or the element is not a token of the vocabulary.K8; VerifiableInference.Desc.First.K8.whole): the smallness test, consisting of one round that samples a matrix with entries −1, 0 or 1 and sends no oracle message, one list of claims, and two steps after the segment's batching.K9; VerifiableInference.Desc.K9.batch): a segment's batching; two further sub-protocols of this kind come just before and just after the segment-closing row fold.K10; VerifiableInference.Desc.First.Close.kind): 2 + k rounds that close a segment: a batching of linear constraints of the segment's group, then a fold of 1 + k rounds; no oracle message is sent or opened.K11; Johnson.Desc.First.ForkMerge.headClaimMergeKind): lk + 4 rounds in the head's segment: a batching challenge and a masked sumcheck on the head's one claim on the committed table, which leave one claim; no oracle message is sent or opened.K12; VerifiableInference.Desc.K12.proximityTestKind): a batching round; for each stage except the last, a fold of 1 + k rounds and a code switch of 2 rounds; then a base case of 2 rounds.K13; VerifiableInference.Desc.K13.claimCombinationBlock): 2 + kCol rounds after the segments: one sampled element batches the two or more claims left on the committed table, and a masked sumcheck reduces them to one; no oracle message is sent or opened.K14; Desc.K14.blocks): the test on the committed table. Six sub-protocols in the second chain, around two sub-protocols of the kind "oracle message with out-of-domain sample", sample two points and the positions at which the table is opened, impose linear constraints and assign tenants to groups. One sub-protocol in the third chain (VerifiableInference.Desc.Third.batchLinearConstraintsSecondPart), with no rounds, adopts an oracle message of the second chain and adds a linear constraint.K15; Desc.K15.linkBlocksBeforeTest): the link IOP's steps on its two committed tables, around a sub-protocol of the kind "oracle message with out-of-domain sample". They are: a sampled point; one sub-protocol with no round on the two tables' out-of-domain samples; sampled positions, with the first table opened at the first columnsFirst of them and the second table at the next columnsFurther; and a further sampled value, from which one linear constraint is added to the group.first, shared and second are the first, second and third chain, respectively. Names of the IOPs in Lean: the offline IOP is the field key of Files and the field offline of Iop.HolographicProtocol; the link IOP is entry and link; the online IOP is proof and, with its round marking, onlineBatch. Comments in the Lean code call the three IOPs the key file, the entry file and the proof file, after the files that contain their proofs.| kind | offline IOP | link IOP | online IOP | all |
|---|---|---|---|---|
| Oracle message with out-of-domain sample | 5 | 1 | 54 | 60 |
| Code switch between segments | 0 | 0 | 25 | 25 |
| Product-tree lookup argument | 2 | 0 | 50 | 52 |
| Layer-segment sumchecks | 0 | 0 | 12 | 12 |
| Attention-segment sumchecks | 0 | 0 | 12 | 12 |
| Output-head sumchecks | 0 | 0 | 1 | 1 |
| Next-token message | 0 | 0 | 1 | 1 |
| Draw of the approximate range proof | 0 | 0 | 25 | 25 |
| Segment claim batching | 0 | 0 | 75 | 75 |
| Segment-closing row fold | 0 | 0 | 25 | 25 |
| Output-head committed-table sumcheck | 0 | 0 | 1 | 1 |
| Proximity test with linear constraints | 4 | 1 | 4 | 9 |
| Committed-table claim merge | 1 | 0 | 1 | 2 |
| Committed-table claim reduction | 7 | 0 | 7 | 14 |
| Two-table comparison steps | 0 | 4 | 0 | 4 |
| none | 16 | 2 | 81 | 99 |
| all | 35 | 8 | 374 | 417 |
| number in its chain, and address | kind | what it does | how often | rounds | oracle messages sent |
|---|---|---|---|---|---|
| 0 ⟨1, –, 1⟩ | Oracle message with out-of-domain sample | The prover sends an oracle message of mask entries; out-of-domain seeds are sampled and answered. | 1 | 2 | – |
| 1 ⟨1, –, 2⟩ | Oracle message with out-of-domain sample | The prover sends the oracle message that the lookups use; out-of-domain seeds are sampled and answered. A group is opened. | 1 | 2 | – |
| 2, 8 ⟨1, i, 0⟩ | none | A lookup's segment starts. No round. | 2 | 0 | – |
| 3, 9 ⟨1, i, 1⟩ | none | No round. Fixes which entries of the two oracle messages above are the masks of the masked scalars of the lookup's rounds. | 2 | 0 | – |
| 4, 10 ⟨1, i, 2⟩ | Product-tree lookup argument | Lookup argument number i. | 2 | 9,581 and 9,220 | – |
| 5, 11 ⟨1, i, 3⟩ | none | No round, nothing sampled. It receives the segment's claims and turns them into linear constraints and claims on the looked-up values. | 2 | 0 | – |
| 6, 12 ⟨1, i, 4⟩ | none | No round; it checks nothing here. | 2 | 0 | – |
| 7, 13 ⟨1, i, 5⟩ | none | The segment ends. No round. | 2 | 0 | – |
| 14 ⟨1, –, 4⟩ | none | No round. All lookups' linear constraints are imposed on the group that the next test tests. | 1 | 0 | – |
| 15 ⟨1, –, 5⟩ | Proximity test with linear constraints | Proximity test on that group. | 1 | 23 | – |
| 16 ⟨1, –, 13⟩ | Committed-table claim merge | The lookups' claims on looked-up values become claims on the committed table; one sampled element and a masked sumcheck reduce these to one. | 1 | 20 | – |
| 17 ⟨1, –, 14⟩ | Oracle message with out-of-domain sample | The prover sends the chain's last oracle message; out-of-domain seeds are sampled and answered. A group is opened for it and one linear constraint imposed on it. | 1 | 2 | – |
| 18 ⟨1, –, 15⟩ | none | The chain's end: one round named SEAL in which nothing is sent or read; rejects if a count of claims is still outstanding, if a group other than the one that the third chain tests is untested, or if a sampled tenant outside that group is in no tested group. | 1 | 1 | – |
| 0 ⟨2, –, 0⟩ | none | No round. It contains public checks. | 1 | 0 | – |
| 1 ⟨2, –, 1⟩ | Committed-table claim reduction | The verifier samples a point. | 1 | 1 | – |
| 2 ⟨2, –, 2⟩ | Oracle message with out-of-domain sample | The prover sends an oracle message whose tenants are the committed table's rows folded at part of that point, and a mask; out-of-domain seeds are sampled and answered. | 1 | 2 | – |
| 3 ⟨2, –, 3⟩ | Committed-table claim reduction | No round. For each out-of-domain answer of the committed table, one linear constraint on the folded tenant. | 1 | 0 | – |
| 4 ⟨2, –, 4⟩ | Committed-table claim reduction | The verifier samples positions; the committed table is opened there; one linear constraint on the folded tenant for each position. | 1 | 1 | – |
| 5 ⟨2, –, 5⟩ | Oracle message with out-of-domain sample | The prover sends two further oracle messages, the second a mask; out-of-domain seeds are sampled and answered. | 1 | 2 | – |
| 6 ⟨2, –, 6⟩ | Committed-table claim reduction | No round. The new tenants are assigned to the two groups that the two proximity tests test. | 1 | 0 | – |
| 7 ⟨2, –, 7⟩ | Committed-table claim reduction | The verifier samples a second point. | 1 | 1 | – |
| 8 ⟨2, –, 8⟩ | Committed-table claim reduction | The prover sends one masked value; the linear constraint that equates the values of the two tenants at the two points is split into one constraint for each group. | 1 | 1 | – |
| 9 ⟨2, –, 9⟩ | Proximity test with linear constraints | Proximity test on the first group, with all linear constraints imposed on it. | 1 | 35 | – |
| 10 ⟨2, –, 10⟩ | Proximity test with linear constraints | Proximity test on the second group. | 1 | 24 | – |
| 11 ⟨2, –, 11⟩ | none | The chain's end: one round named SEAL in which nothing is sent or read; rejects if a group is untested or a sampled tenant is in no tested group. | 1 | 1 | – |
| 0 ⟨3, –, 0⟩ | Committed-table claim reduction | No round. An oracle message of the second chain is adopted and joins the group that this chain's proximity test tests; one linear constraint on it and another tenant is added. | 1 | 0 | – |
| 1 ⟨3, –, 1⟩ | none | No round. Checks that every oracle message which the next test opens and this chain has not sent is declared as taken from the chain that sent it. | 1 | 0 | – |
| 2 ⟨3, –, 2⟩ | Proximity test with linear constraints | Proximity test on that group. | 1 | 30 | – |
| 3 ⟨3, –, 3⟩ | none | The chain's end, no round; rejects if a group is untested or a sampled tenant is in no tested group. | 1 | 0 | – |
The numbers of rounds are given by L₁, L₂, L₃ and the theorem laid_rounds_in_scope. The addresses and kinds are given by the definitions Key.wantedFirst, Key.wantedShared, Key.wantedSecond and the theorem desc_lists.
| number in its chain, and address | kind | what it does | how often | rounds | oracle messages sent |
|---|---|---|---|---|---|
| 0 ⟨1, –, 0⟩ | none | No round. It contains the public checks on the parameters. | 1 | 0 | 0 |
| 1 ⟨1, –, 1⟩ | Two-table comparison steps | The verifier samples one point for both committed tables. | 1 | 1 | 0 |
| 2 ⟨1, –, 2⟩ | Oracle message with out-of-domain sample | The prover sends one oracle message with two tenants, each one table's rows folded at that point, and a mask tenant; out-of-domain seeds are sampled and answered. | 1 | 2 | 1 |
| 3 ⟨1, –, 3⟩ | Two-table comparison steps | No round. For each out-of-domain answer of either table, one linear constraint on that table's folded tenant. | 1 | 0 | 0 |
| 4 ⟨1, –, 4⟩ | Two-table comparison steps | The verifier samples positions; the first table is opened at the first columnsFirst of them, the second table at the next columnsFurther; one linear constraint for each position. | 1 | 1 | 0 |
| 5 ⟨1, –, 5⟩ | Two-table comparison steps | The verifier samples a second point; one linear constraint says that the two folded tenants agree on their first entries, up to a fixed cut. | 1 | 1 | 0 |
| 6 ⟨1, –, 6⟩ | Proximity test with linear constraints | Proximity test on the one group, with all these constraints. | 1 | 36 | – |
| 7 ⟨1, –, 7⟩ | none | The chain's end, no round; rejects if the group is untested. | 1 | 0 | 0 |
The order and kinds are read off the definitions Desc.K15.linkBlocksBeforeTest and Desc.K15.linkProtocolChain. The numbers of rounds are obtained from these definitions and the written parameters Desc.K15.frP.
The first chain has 25 segments: numbers 0, 2, …, 22 treat layers, numbers 1, 3, …, 23 attention, and number 24 the head. An ordinary segment l has 14 sub-protocols, numbered 1 + 14·l + j, j = 0 … 13.
| number in its chain, and address | kind | what it does | how often | rounds | oracle messages sent |
|---|---|---|---|---|---|
| 0 ⟨1, –, 0⟩ | none | The chain's first sub-protocol: no round, no check. | 1 | 0 | 0 |
| 1 + 14·l + 0 ⟨1, l, 0⟩, l = 0 … 23 | none | The segment starts. No round. It contains the public check that the fixed order of claims names exactly the lists that the segment's sub-protocols state. | 24 | 0 | 0 |
| 1 + 14·l + 1 ⟨1, l, 1⟩, l = 0 | Oracle message with out-of-domain sample | Segment 0 only. The prover sends the chain's first oracle messages; out-of-domain seeds are sampled and answered. The segment's group is opened. | 1 | 2 | 2 |
| 1 + 14·l + 1 ⟨1, l, 1⟩, l = 1 … 23 | Code switch between segments | Code switch: the prover sends a new oracle message, with out-of-domain seeds and answers; earlier oracle messages are opened at sampled positions. | 23 | 2 | 1 |
| 1 + 14·l + 2 ⟨1, l, 2⟩, l = 0 … 23 | Product-tree lookup argument | The segment's first lookup argument. | 24 | 1,046 (l even), 984 (l odd) | 0 |
| 1 + 14·l + 3 ⟨1, l, 3⟩, l even | Layer-segment sumchecks | Even l: the rounds specific to layers: sampled points, batching challenges, masked sumchecks. | 12 | 170 (l = 0), 168 | 0 |
| 1 + 14·l + 3 ⟨1, l, 3⟩, l odd | Attention-segment sumchecks | Odd l: the rounds specific to attention: prover scalars, sampled points, batching challenges, masked sumchecks. | 12 | 162 | 0 |
| 1 + 14·l + 4 ⟨1, l, 4⟩, l = 0 … 23 | Oracle message with out-of-domain sample | The prover sends an oracle message; out-of-domain seeds are sampled and answered. | 24 | 2 | 1 |
| 1 + 14·l + 5 ⟨1, l, 5⟩, l = 0 … 23 | Draw of the approximate range proof | The verifier samples matrices with entries −1, 0, 1; the prover sends nothing. | 24 | 1 | 0 |
| 1 + 14·l + 6 ⟨1, l, 6⟩, l = 0 … 23 | Oracle message with out-of-domain sample | The prover sends an oracle message; out-of-domain seeds are sampled and answered. | 24 | 2 | 1 |
| 1 + 14·l + 7 ⟨1, l, 7⟩, l = 0 … 23 | Product-tree lookup argument | The segment's second lookup argument. | 24 | 746 (l even), 716 (l odd) | 0 |
| 1 + 14·l + 8 ⟨1, l, 8⟩, l = 0 … 23 | Segment claim batching | Batching: one sampled element; all claims of the segment are added into one equation, weighted by its powers. | 24 | 1 | 0 |
| 1 + 14·l + 9 ⟨1, l, 9⟩, l = 0 … 23 | none | No round. The segment's checks on the batched equation, then the steps that its sub-protocols specify for the stage after the batching. | 24 | 0 | 0 |
| 1 + 14·l + 10 ⟨1, l, 10⟩, l = 0 … 23 | Segment claim batching | No round. The batched equation becomes one linear constraint on the segment's group. | 24 | 0 | 0 |
| 1 + 14·l + 11 ⟨1, l, 11⟩, l = 0 … 23 | Segment-closing row fold | One sampled element batches the group's linear constraints; a masked sumcheck leaves one linear constraint on the group's folded rows. | 24 | 10 (l even), 9 (l odd) | 0 |
| 1 + 14·l + 12 ⟨1, l, 12⟩, l = 0 … 23 | Segment claim batching | No round, no check: the segment is marked as closed. | 24 | 0 | 0 |
| 1 + 14·l + 13 ⟨1, l, 13⟩, l = 0 … 23 | none | The segment ends. No round. | 24 | 0 | 0 |
| 337 ⟨1, 24, 0⟩ | none | The head's segment starts. No round. | 1 | 0 | 0 |
| 338 ⟨1, 24, 1⟩ | Next-token message | The prover sends one field element, the next token; nothing is sampled. | 1 | 1 | 0 |
| 339 ⟨1, 24, 2⟩ | Code switch between segments | Code switch, as in the other segments. | 1 | 2 | 1 |
| 340 ⟨1, 24, 3⟩ | Product-tree lookup argument | The segment's first lookup argument. | 1 | 1,080 | 0 |
| 341 ⟨1, 24, 4⟩ | Output-head sumchecks | The rounds specific to the head: sampled points, batching challenges, masked sumchecks. | 1 | 82 | 0 |
| 342 ⟨1, 24, 5⟩ | Oracle message with out-of-domain sample | The prover sends an oracle message; out-of-domain seeds are sampled and answered. | 1 | 2 | 1 |
| 343 ⟨1, 24, 6⟩ | Draw of the approximate range proof | The verifier samples matrices with entries −1, 0, 1. | 1 | 1 | 0 |
| 344 ⟨1, 24, 7⟩ | Oracle message with out-of-domain sample | The prover sends an oracle message; out-of-domain seeds are sampled and answered. | 1 | 2 | 1 |
| 345 ⟨1, 24, 8⟩ | Product-tree lookup argument | The segment's second lookup argument. | 1 | 746 | 0 |
| 346 ⟨1, 24, 9⟩ | Output-head committed-table sumcheck | A batching challenge and a masked sumcheck on the head's one claim on the committed table. | 1 | 22 | 0 |
| 347 ⟨1, 24, 10⟩ | Segment claim batching | Batching of the segment's claims. | 1 | 1 | 0 |
| 348 ⟨1, 24, 11⟩ | none | No round. Checks on the batched equation; steps after the batching. | 1 | 0 | 0 |
| 349 ⟨1, 24, 12⟩ | Segment claim batching | No round. The batched equation becomes one linear constraint. | 1 | 0 | 0 |
| 350 ⟨1, 24, 13⟩ | Segment-closing row fold | Batching of the group's constraints and masked sumcheck, as in the other segments. | 1 | 10 | 0 |
| 351 ⟨1, 24, 14⟩ | Segment claim batching | No round, no check: the segment is marked as closed. | 1 | 0 | 0 |
| 352 ⟨1, 24, 15⟩ | none | The segment ends. No round. | 1 | 0 | 0 |
| 353 ⟨1, –, 1⟩ | Code switch between segments | Code switch after the last segment. | 1 | 2 | 1 |
| 354 ⟨1, –, 2⟩ | Proximity test with linear constraints | Proximity test. | 1 | 33 | 5 |
| 355 ⟨1, –, 3⟩ | Committed-table claim merge | One sampled element and a masked sumcheck reduce the pending claims on the committed table to one. | 1 | 20 | 0 |
| 356 ⟨1, –, 4⟩ | Oracle message with out-of-domain sample | The prover sends the chain's last oracle message; out-of-domain seeds are sampled and answered. One linear constraint is imposed on its group. | 1 | 2 | 1 |
| 357 ⟨1, –, 5⟩ | none | The chain's end: one round named SEAL in which nothing is sent or read; rejects if a count of claims is still owed, if the group that the third chain tests is not the last group, if the chain's last oracle message is not in that group alone, if a group other than the one that the third chain tests is untested, or if a sampled tenant outside that group is in no tested group. | 1 | 1 | 0 |
| 0 ⟨2, –, 0⟩ | none | No round. It contains public checks. | 1 | 0 | 0 |
| 1 ⟨2, –, 1⟩ | Committed-table claim reduction | The verifier samples a point. | 1 | 1 | 0 |
| 2 ⟨2, –, 2⟩ | Oracle message with out-of-domain sample | The prover sends an oracle message whose tenants are the committed table's rows folded at part of that point, and a mask; out-of-domain seeds are sampled and answered. | 1 | 2 | 1 |
| 3 ⟨2, –, 3⟩ | Committed-table claim reduction | No round. For each out-of-domain answer of the committed table, one linear constraint on the folded tenant. | 1 | 0 | 0 |
| 4 ⟨2, –, 4⟩ | Committed-table claim reduction | The verifier samples positions; the committed table is opened there; one linear constraint on the folded tenant for each position. | 1 | 1 | 0 |
| 5 ⟨2, –, 5⟩ | Oracle message with out-of-domain sample | The prover sends two further oracle messages, the second a mask; out-of-domain seeds are sampled and answered. | 1 | 2 | 2 |
| 6 ⟨2, –, 6⟩ | Committed-table claim reduction | No round. The new tenants are assigned to the two groups that the two proximity tests test. | 1 | 0 | 0 |
| 7 ⟨2, –, 7⟩ | Committed-table claim reduction | The verifier samples a second point. | 1 | 1 | 0 |
| 8 ⟨2, –, 8⟩ | Committed-table claim reduction | The prover sends one masked value; the linear constraint that equates the values of the two tenants at the two points is split into one constraint for each group. | 1 | 1 | 0 |
| 9 ⟨2, –, 9⟩ | Proximity test with linear constraints | Proximity test on the first group, with all linear constraints imposed on it. | 1 | 35 | 4 |
| 10 ⟨2, –, 10⟩ | Proximity test with linear constraints | Proximity test on the second group. | 1 | 24 | 4 |
| 11 ⟨2, –, 11⟩ | none | The chain's end: one round named SEAL in which nothing is sent or read; rejects if a group is untested or a sampled tenant is in no tested group. | 1 | 1 | 0 |
| 0 ⟨3, –, 0⟩ | Committed-table claim reduction | No round. An oracle message of the second chain is adopted and joins the group that this chain's proximity test tests; one linear constraint on it and another tenant is added. | 1 | 0 | 0 |
| 1 ⟨3, –, 1⟩ | none | No round. Checks that every oracle message which the next test opens and this chain has not sent is declared as taken from the chain that sent it. | 1 | 0 | 0 |
| 2 ⟨3, –, 2⟩ | Proximity test with linear constraints | Proximity test on that group. | 1 | 30 | 4 |
| 3 ⟨3, –, 3⟩ | none | The chain's end, no round; rejects if a group is untested or a sampled tenant is in no tested group. | 1 | 0 | 0 |
The addresses, kinds, numbers of rounds and oracle messages sent are given by the values PlanWritten.cutFirstFull, PlanWritten.cutSharedFull, PlanWritten.cutSecondFull, with the theorems laidPOf_pins_scope and cut_of_row.
The label of a sub-protocol's kind: one of the fifteen kinds K1 to K15, each with a plain name in Appendix A, or frame for a sub-protocol that does not belong to any kind, such as the start or end of a segment or the end of a chain.
The address of a sub-protocol within a file's IOP: its chain (1, 2 or 3), its segment's number if it belongs to a segment, its number within that segment or at the chain's end, and its kind.
A schedule entry: a round's name and eleven numbers, including the numbers of proof-of-work bits, prover-message bytes, Merkle roots, sample answers, and sampled extension-field elements, positions and matrix entries.
The data that a round declares about a tree that it opens: the depth a (positions are taken modulo 2^a), the width W in base-field words, whether the tree is a committed table's tree, and the tree number.
A committed table as queried in one round: its tree's shape, the length in bytes of a leaf's salt, the number item of the statement item that contains its root, and its share of the round's positions (count positions starting at number lo).
A committed table's share of a round's sampled positions: up to count positions starting at number lo (from 0).
If the tables' shares follow one another without a gap, starting at position number i, the result is the number of the position after the last share; otherwise it is none.
True if a list of numbers is strictly increasing.
The key of a committed table's columns in a view: 2^16 plus the table's number.
Inserts a number into a strictly increasing list, unless it is already there.
The distinct entries of a list of numbers, in strictly increasing order.
The sort of an item in a prover's message: base-field element, extension-field element, word, Merkle root, or sample answer.
An item of a prover's message as read: one 64-bit word (f, word), three words (e, answer), or a byte string (root).
A round's challenge as sampled values: extension-field elements, positions, matrix entries, and an optional digest.
A round's values: the parsed items of the prover's message (in a view, without the Merkle roots) and the challenge.
The view of one chain that the verifier's decision receives: the values and challenges of its rounds, and the opened columns as triples (key, position, words).
An opened column: key, position, and its list of 64-bit words.
Identifies the Merkle tree that a round opens: the n-th tree whose root the round's own chain sends, or tree number sent of another chain in the same file. Trees are numbered from 0, and here chain is a list index starting at 0, so chain 0 is chain 1.
A declared round: its schedule entry; the committed tables it queries, each at its share of the round's sampled positions; and the other Merkle trees it opens at all positions, each with its shape and source.
One tenant of an oracle message's symbols: its numbers of main and mask words per symbol, its field degree (1 or 3), whether it has an out-of-domain sample, and its group numbers.
The declared shape of an oracle message where it is sent: 2^logLength symbols, each of words base-field words, and the list of tenants that share a symbol.
One sub-protocol, for verifier state type S and claim type Cl
the name name, which labels its rejections
the address place
the public check planOk
the declared rounds rounds, each with the committed tables and trees that it queries
the oracle messages oracles: for each round, the oracle message under each root that the round sends
the oracle messages before that must have been sent and, if sampled, have had their sample answered before the sub-protocol's first challenge. Each is given by its chain (1, 2 or 3) and its number, from 0, in that chain's order of sending
the decision decide, which takes the verifier state, its rounds' values and the answers to its queries (one list of positions with their words for each table or tree opened) and returns the next state or a rejection
the named functions claims: each takes the number of claims its segment has gathered so far and the state, and returns further claims with the state, or a rejection
the named functions after: each takes the state after batching and returns the state or a rejection
A kind of sub-protocol: a function from parameters of an arbitrary type P to a sub-protocol.
A kind that takes, besides its parameters, a list of items of an arbitrary type G.
A segment of a chain, with verifier state type S and claim type Cl. Its parts run in the order lay, hear, batch, tests, the after functions listed in orderAfter, close, clear
the name name, which labels the segment
the numbers chain and number of its chain and of the segment
the state update lay
the sub-protocols hear, which state claims
the list order of claims functions of hear: each is given by its sub-protocol's position in hear and its name
the check each, run after every function that order lists
the list orderAfter of after functions of hear, in the same form
the sub-protocol batch, which takes as its argument the function that runs the claims functions listed in order and collects their claims
the checks tests, which by their type cannot change the state
the sub-protocols close
the state update clear, which ends the segment's part of the state
A chain of sub-protocols with a common verifier state type S and claim type Cl. Its parts run in the order listed below. The offline and online IOPs have three chains each, and the link IOP has one
the sub-protocol first
the sub-protocols front
the segments links
the sub-protocols back
the sub-protocol last, which ends the chain and, in a sealed chain, declares the round named SEAL
The written IOP of a file with three chains, for instances of type Xi
the state types S₁, S₂, S₃ of chains 1, 2 and 3, and their common claim type Cl
the declared rounds plans of each chain
the committed table's depth tableDepth
the table wanted, intended to be computed from the schedule: the address and number of rounds of every sub-protocol of the three chains, in order. Sub-protocols joined by andThen share one row
the table owed, intended to be computed from the schedule: each row gives an address and the oracle messages that the sub-protocol there must name in before
the Boolean check fileOk on the schedule that relates the chains to each other
the check okStart on the instance only
the type XiPub and the map pub to it: intended to be the instance without the claimed next token (its public part); the offline description takes pub := id
the initial states start₁ and start₂ of chains 1 and 2, computed from that public part
the initial state start₃ of chain 3, from that public part and the final states of chains 1 and 2; it may reject
the chains first, shared and second: chains 1, 2 and 3
the final check fin on the instance and the three final states
The written IOP of a file with one chain, for instances of type Xi
the state type S and the claim type Cl
the declared rounds plan of the chain
the committed tables' depth tableDepth
the number tables of committed tables that the file's statement contains, as its items 0, 1 and so on
the file's Boolean check fileOk on the schedule
the check okStart on the instance
the function start, which maps the instance to the chain's initial state
the chain chain
the final check fin on the instance and the chain's final state
the file's variables
Turns an optional value into a result: the value if present, otherwise a rejection with the given name.
the file's variables
Succeeds if the Boolean check is true; otherwise rejects with the given name.
the file's variables
The queries of a list of declared rounds, given each round's sampled challenge: for each round in turn, one list for each committed table that it queries and then one for each other Merkle tree that it opens. Each list consists of triples (key, position, width).
A committed table is queried at its share of the round's sampled positions, each taken modulo 2 ^ a, where a is the depth. Fmt.listOf sorts the positions in increasing order and removes duplicates. The key is Fmt.storedKey of the table's number, and the width is W of the table.
A tree is queried at all of the round's sampled positions, taken modulo 2 ^ a and ordered in the same way. The key is the tree's number minus firstTree, truncated at 0, and the width is W of the tree.
The result ends when either input list ends.
the file's variables
The sort of a message item that was read: base-field element, extension-field element, word, root, or sample answer.
the file's variables
Checks, for one round, that each sampled element that the schedule entry marks as nonzero is not the triple of words (0, 0, 0). It fails if Fmt.kindOf does not recognize the round's name.
the file's variables
Checks a list of round values against a list of declared rounds, pair by pair.
The sorts of the message items must equal the declared items with the Merkle roots left out, and the challenge must contain the declared number of extension-field elements.
The challenge must contain the declared numbers of positions and matrix entries (trits).
Every position must be below 2 ^ logN.
Every matrix entry must be −1, 0 or 1, and drawsMarkedNonzeroHaveNonzeroWords must hold.
The check fails if the two lists differ in length.
the file's variables
Splits a list of opened columns into consecutive groups of the given lengths, keeping each column's position and words and dropping its key.
the file's variables
A round's values with the challenge's field digest set to none. Rounds are passed to decide in this form.
the file's variables
Runs one sub-protocol: checks its rounds by roundsFit, checks that the next opened columns match its queries in key, position and width, then calls decide. Returns the next state and how many columns it consumed.
the file's variables
Looks up the claim function that o names (the index of a sub-protocol in bs, and a name) and runs it on the number of claims gathered so far and the state. It then runs the check each on o and on the claims and state that the function returned, appends those claims to the list and keeps that state. It rejects if there is no such function, or if the function or each rejects.
the file's variables
Runs the claim functions listed in order in sequence with claimsInStep, starting from the empty list of claims. Returns all claims and the final state, or the first rejection.
the file's variables
Runs the after functions listed in order, each on the state returned by the previous one. It rejects if one of them rejects or does not exist.
the file's variables
Checks two lists of names against each other: no name occurs twice in all, each name of all occurs exactly once in order, and order has no other name.
the file's variables
Public check: no sub-protocol has two claim functions with the same name, and order lists every claim function of the given sub-protocols exactly once, and nothing else.
the file's variables
Public check: no sub-protocol has two after functions with the same name, and order lists every after function of the given sub-protocols exactly once, and nothing else.
the file's variables
True if a sub-protocol has no claim function and no after function.
the file's variables
The step of a segment directly after its batch: first the segment's tests on the state, then the after functions of the sub-protocols in hear, in the order orderAfter. It stops at the first rejection.
the file's variables
Lists a segment's sub-protocols in order.
First, a roundlessBlock that runs lay.
Its public check planOk requires orderOk on order, orderAfterOk on orderAfter, and Block.hasNoClaimsAndNothingAfter of batch and of every sub-protocol of close.
Then those of hear, and batch applied to the function that gathers the claims (claimsInBy).
Then a roundlessBlock that runs runBehind, and those of close.
Last, a roundlessBlock that runs clear.
the file's variables
Lists a chain's sub-protocols in order: first, those of front, those of each segment of links as listed by Link.blocksInOrder, those of back, and last. Each sub-protocol outside a segment has Block.hasNoClaimsAndNothingAfter added to its public check planOk, so it fails that check if it has a claim function or an after function.
the file's variables
The prime 2^64 − 2^32 + 1 as a 64-bit word.
the file's variables
Checks that every 64-bit word that encodes a field element in a view (in prover messages, sampled elements and opened columns) is below the prime 2^64 − 2^32 + 1.
the file's variables
Runs a list of sub-protocols in order.
If no sub-protocol is left, the result is the final state and the remaining round values and columns.
Each sub-protocol takes from the front of the list one round value for each round it declares.
It rejects if too few remain.
Block.step then runs it on those values and the list of columns.
The first rejection is the result.
The columns that it used are dropped from the front of the list of columns.
the file's variables
Appends one empty round (no message items, no challenge, no digest) to a view.
the file's variables
Runs one chain on its view from an initial state, using foldBlocks. It rejects if the chain has no sub-protocols, if a sub-protocol rejects, if too few rounds remain for a sub-protocol, or if a round or opened column is left over.
The declared rounds of the three chains of a file: a triple with one list of Fmt.DeclaredRound for each chain.
For each chain in order, the list of oracle messages that it sends, in the order of sending. The type does not fix the number of chains; the protocol has three. Lean lists are indexed from 0, so index 0 is chain 1.
One opening of a Merkle tree: the chain that sent the tree, the tree's number on that chain, the shape that the opening round declares, and the logarithm of that round's range of positions.
All openings of Merkle trees in the three chains, in order. Queries to committed tables are not among them.
The declared oracle message for an opening's tree, if the list of oracle messages contains one for the chain that sent the tree and the tree's number on that chain.
Evaluates a condition on the tenants of an opened tree; returns true if no oracle message is declared for that tree.
Clause: every oracle message has at least one tenant, and its tenants' main and mask words add up to the symbol's width.
Clause: every tenant has field degree 1 or 3, the number of its main words is a multiple of that degree, and the number of its mask words is a multiple of 3.
Clause: for every tree that is opened, an oracle message is declared.
Clause: no opened tree is deeper than the logarithm of the range from which the opening round samples positions.
Clause: in every opened tree, all tenants with an out-of-domain sample have the same list of groups.
Clause: if an opened tree has a tenant without an out-of-domain sample, each of its tenants with one belongs to at most one group.
Clause: a tree that has a tenant without an out-of-domain sample is opened at most once in the whole file.
The number of tenants with an out-of-domain sample among the given oracle messages.
A check on one chain. It processes the rounds in order and maintains due, the number of sample answers that the next round must declare (answered initializes it to 0).
After the last round, due must be 0, and no remaining oracle message may have a tenant with an out-of-domain sample.
k is the number of tenants with an out-of-domain sample among the oracle messages that the round sends.
The round's answers must equal due.
If k ≥ 1, the round must be of kind seeds and have drawNZ ≠ 0, where drawNZ counts the sampled field elements that must be nonzero.
In every case, due for the next round is k · drawNZ, which is 0 if k = 0.
Clause: answeredIn holds on each of the three chains, so the tenants' flags and the schedule's numbers of sample answers agree.
Clause: oracle messages are declared for exactly three chains, and each chain has as many as there are Merkle roots in its schedule entries.
True if the oracle message with the given chain and number has a tenant with an out-of-domain sample; false if no oracle message is declared for that chain and number.
Clause: a condition on every opening of a tree in the three chains.
A chain may open a tree that it sends itself (.own) no earlier than the round that sends it, and only in a later round if the tree's oracle message has a tenant with an out-of-domain sample.
Only the third chain may open a tree of another chain (.taken), and that tree must be one that the first or second chain sends.
For one chain: in every round the opened trees are declared in strictly increasing order of the pair (sending chain, number on that chain).
Clause: inOrderIn holds on each of the three chains, so no round opens the same tree twice.
The eleven clauses on Merkle trees, their tenants and their openings, each with its name.
True exactly when all eleven clauses in clauses hold for the declared rounds D and the oracle messages T.
the file's variables
The declared rounds of the three chains, obtained by concatenating the rounds of each chain's sub-protocols in order.
the file's variables
The table of all sub-protocols of the three chains in order: name, address and number of rounds.
the file's variables
Public check on one sub-protocol: it lists one oracle message for each Merkle root of each round, each symbol's number of words is the sum of its tenants' numbers of words, and each tenant has field degree 1 or 3.
the file's variables
For one chain, every opening in the file of a tree that this chain sends: the tree's number in the chain, and the depth and width that the opening declares.
the file's variables
The tree number (Shape.tree) of the third chain's first own tree: the number of Merkle roots that the first chain sends, plus 1, regardless of what the second chain sends.
the file's variables
Public check on the tree numbers in the declared shapes.
If a chain opens its own tree number n, Shape.tree must be n, or lastChainFirstTreeNumber + n on the third chain.
Only the third chain may open a tree of another chain, which must be the first or the second; Shape.tree must be the tree's number on the chain that sends it.
the file's variables
Every sub-protocol of a list passes its own public check planOk and the check shaped.
the file's variables
For a chain's sub-protocols, the logarithmic length and symbol width of every oracle message they send, in the order of sending.
the file's variables
The number of the round that sends a chain's n-th oracle message, if there is one, found by counting the Merkle roots in the schedule entries; both numbers start from 0. This is the same function as BookPlan.roundOfRoot.
the file's variables
True if a round's challenge has at least one field element, position or matrix entry.
the file's variables
A check on the sub-protocols of one chain. Here c is the chain's index (counted from 0) and from' is the number of the chain's rounds before the first sub-protocol in the list.
Each pair in a sub-protocol's before names a chain and a message number on it.
On this chain, the limit is the round of the sub-protocol's first challenge (drawsAny) or, if it has no challenge, the round after its last one; on another chain, it is that chain's number of rounds.
The message must be sent on the chain that the pair names.
That chain's number must be from 1 to c + 1, so it is this chain or a lower-numbered one. On this chain the message must be sent no later than the limit.
If the message has a tenant with an out-of-domain sample, some later round of the message's chain must have answers ≠ 0; if that chain is this one, that round must also be within the limit.
the file's variables
The oracle messages that a chain's sub-protocols send, in the order of sending.
the file's variables
Public check on order: beforeAt holds on each of the three chains, for the rounds that the sub-protocols declare and the oracle messages that they list.
the file's variables
The three chains' oracle messages, chain by chain, in the form that the checks of BookPlan take.
the file's variables
Public check on Merkle trees: the eleven clauses of BookPlan.allClausesHold, on who may share a tree, when and how often a tree may be opened, and which prover messages carry out-of-domain sample answers.
the file's variables
Public check: each sub-protocol's address gives the chain in whose list it appears, and no two sub-protocols of the file have the same chain, segment and number.
the file's variables
A check on one declared round.
The round samples positions exactly when it queries a committed table or opens another Merkle tree.
It never does both, and the numbers of the committed tables are strictly increasing.
Their shares run from position 0 without a gap up to the number of sampled positions.
Each share has at least one position. Each committed table's shape is marked as a committed table's tree, with tree number 0 and depth at most the round's logN, and its width W is from 1 to 2^24 − 1.
Each other tree's shape is not marked as a committed table's tree, and its width W is at least 1 and at most 2^24 − 1.
the file's variables
Public check: readsFit holds at every round of the three chains.
the file's variables
Public check: the last sub-protocol of the first chain declares at least one round.
the file's variables
Public check: the logarithmic length and symbol width declared where an oracle message is sent equal the depth and width declared at each of its openings, and every oracle message is opened at least once.
the file's variables
The conjunction of these public checks: fileOk; every sub-protocol's own checks and its test shaped; the sub-protocols' rounds equal the declared rounds plans; every queried committed table has depth tableDepth; labelsOk, placesOk, beforeOk, treeSharingOk, readsOk and sentFit.
the file's variables
planOkCore and sealLast: the public checks that run performs before reading the instance or a view.
the file's variables
Public check: the addresses and numbers of rounds of all sub-protocols, in order, equal the table wanted. It is not part of planOk; of the three IOPs, it is called for the offline IOP, by Key.keyDataAndDecisionOfDescription.
the file's variables
For each sub-protocol in a list: its address, whether one of its rounds samples a challenge, and its list before.
the file's variables
Public check: for each row of owed, some sub-protocol at the row's address samples a challenge and lists all the row's oracle messages in before. Not part of planOk; called only by Key.keyDataAndDecisionOfDescription, for the offline IOP.
the file's variables
A chain that does nothing: two sub-protocols with no rounds that leave the state unchanged.
the file's variables
A one-chain written IOP viewed as a three-chain one whose second and third chains do nothing. It is used to apply the three-chain public checks; no decision is run on it.
the file's variables
The declared rounds of the one chain, obtained by concatenating the rounds of its sub-protocols in order.
the file's variables
Public check: every committed table that a round queries has a number below tables, the file's number of committed tables.
the file's variables
The list of names and values of the public checks of a one-chain written IOP, used to produce an error message.
the file's variables
The public checks of a one-chain written IOP: FileDescription.planOkCore applied to asFile, and storedOk.
the file's variables
none if planOk holds; otherwise an error message naming the first sub-protocol that fails its own public check or shaped, or else the first failing clause of BookPlan.clauses, if any.
the file's variables
The verifier's decision for three chains, in order: public checks, instance check, field-range checks, chain 1 on its view with an empty round appended, chain 2, chain 3 started from both final states, final check.
the file's variables
Applies runCore to the fields of a written IOP F, an instance x and three views. Returns the three chains' final states or the reason for rejection.
the file's variables
The verifier's decision for a written IOP F: it accepts an instance and three views if and only if runEnd returns final states.
the file's variables
A written IOP for instances Xi, viewed as one for instances Xi' along a map from Xi' to Xi. Only the instance check, the public part of the instance and the final check change.
the file's variables
none if planOk holds; otherwise an error message that names the first failing sub-protocol or, if there is none, the first failing check of planClauses.
the file's variables
The verifier's decision for one chain, in order: public checks, instance check, field-range check on the view, the chain by chainAt, final check. Returns the chain's final state or the reason for rejection.
the file's variables
The verifier's decision for a one-chain written IOP: it accepts an instance and one view if and only if runEnd returns a final state.
The written offline IOP, built from public parameters: a structure of three chains of sub-protocols with their initial verifier states, the declared rounds, the public checks, the check on the instance, and the final check.
The offline IOP's first chain: two sub-protocols that send oracle messages; a segment per lookup; the lookups' constraints imposed on one group; that group's proximity test; a batching of pending claims; optionally a third sub-protocol that sends oracle messages; the chain's last sub-protocol.
The offline IOP's third chain is the general third chain (card lastChainWithOwnTest) for the offline IOP's public parameters, with a proximity test at address ⟨3, –, 2⟩.
The written online IOP. It takes the second hash function and the bytes of the three public files as arguments and returns the structure of three chains or an error message.
The written online IOP as a function of its parts. It computes the public parameters from the three public files and the argument o, which represents the second hash function, then assembles the written IOP from given lists of sub-protocols and two given later chains; either step may return an error message.
Takes the public parameters and the given sub-protocols. Returns an error message if baseOf returns one or, if anything is inconsistent or missing, an error message that lists it. Otherwise returns the result of onlineDescriptionAfterTests: the assembled written online IOP or a further error message.
The last step of the assembly. It arranges the given sub-protocols into the first chain, adds the two later chains and forms the written IOP's structure; it returns an error message if no usable sub-protocol is supplied at an address, if chainBy returns an error, or if a later chain is missing.
The fifteen lists of sub-protocols from which the online IOP's first chain is assembled, as a function of the public parameters. They cover the sub-protocols of no kind and of every kind except the committed-table claim reduction and the two-table comparison steps.
The online IOP's third chain in full: its state type, its start function (which computes the initial state from the two earlier chains' final states, or rejects) and its final check. Its own public check is constantly true. It returns nothing if the proximity tests' parameters cannot be computed.
An enumeration of the three sorts of model part that a segment of the first chain treats: layers, attention and head.
Maps a segment's sort to the kind of the sub-protocol that is specific to it: layer-segment sumchecks for layers, attention-segment sumchecks for attention, output-head sumchecks for the head.
The kinds of a segment's sub-protocols before its batching, in order.
first in the head's segment: the next-token message
code switch between segments (in the first segment: oracle message with out-of-domain sample), product-tree lookup argument, the kind specific to the segment's sort, oracle message with out-of-domain sample, sampling step of the approximate range proof, oracle message with out-of-domain sample, product-tree lookup argument
last in the head's segment: the output-head committed-table sumcheck
The kinds of the sub-protocols after the last segment, in order, without the chain's last sub-protocol: code switch between segments, proximity test with linear constraints, committed-table claim merge (only if the flag is true), oracle message with out-of-domain sample.
The kinds of the three sub-protocols that close a segment, in order: segment claim batching, segment-closing row fold, segment claim batching. The first and third sub-protocols have no rounds. The three come after the segment's batching and the sub-protocol without a kind that follows it.
The structure Blocks collects the parts from which the first chain is built.
the sub-protocol at each address, if there is one, block
the batching at each address, if there is one, batch
the steps on the verifier state at the start of a segment, lay, and at its end, clear; each returns a new state or an error
a segment's checks after each of its lists of claims, each
a segment's checks on the state after its batching, tests
a comparison of two states, same
the chain's first sub-protocol, first
the chain's last sub-protocol, last
the file's variables
Builds segment l of a given sort from the sub-protocols at the addresses determined by the lists of kinds, and fixes the order in which their claims are batched. Returns nothing if one of these sub-protocols is missing.
the file's variables
Builds the first chain from the list of the segments' sorts: the first sub-protocol, the segments, the sub-protocols after them, and the last sub-protocol. Returns nothing if the head is not the last segment, if it also occurs earlier in the list, or if a sub-protocol is missing.
the file's variables
The first chain as used: the chain of the card firstChainWithoutReplyGuard, with a check added after every step except the decision of the next-token message's sub-protocol. The check rejects a step if the given comparison of the states before and after it fails.
The test on the committed table, as eight sub-protocols in order, at addresses ⟨2, –, 1⟩ to ⟨2, –, 8⟩.
number 1: the verifier samples a point
number 2: the prover sends an oracle message whose tenants are the table's rows folded at part of that point, and a mask
number 3: each out-of-domain answer of the table gives a linear constraint on the folded tenant
number 4: the verifier samples positions, at which the table is opened
number 5: the prover sends one or two further oracle messages
number 6: the tenants of these messages are assigned to groups
number 7: the verifier samples a second point
number 8: it splits the linear constraint that equates the values of the two tenants at the two points into one constraint for each group, and has no round when there is only one group
The third chain consists of the second part of the test on the committed table, a check of the declared source of each oracle message taken from another chain, the given proximity test, and the chain's last sub-protocol.
The link IOP's five sub-protocols before its proximity test:
masksAhead is truecolumnsFirst of them and the copy at the next columnsFurtherThe written link IOP (one chain), built from public parameters, declared rounds and a Boolean used as its public check fileOk. Instance: each committed table's out-of-domain seeds and answers. Its final check always accepts.
The link IOP's decision linkDecisionAtParameterFile maps the bytes of a parameter file to a function of the two out-of-domain samples and a view.
the file's first lines are read
they are compared with recordLines, the first lines of the full-size parameter file
linkAt is applied; it returns no error only if the public checks pass
if linkAt returns no error, the function runs the written link IOP; otherwise it rejects every input
if the first lines differ from recordLines or cannot be read, the function rejects every input
the file's variables
Oracle message with out-of-domain sample. In the first round the prover sends oracle messages and the verifier samples out-of-domain seeds. In the second round the prover sends the answers. Each answer becomes a linear constraint on the sampled tenant that it answers for.
the file's variables
Oracle message with out-of-domain sample, inside a segment. It checks that the state is at this segment and step and expects these messages, then runs the rounds and decision of sendOwn. The messages' tenants join the segment's group, and the listed arrays are marked as committed.
the file's variables
Oracle message with out-of-domain sample at the start of the first segment: it opens that segment's group, then runs the rounds and decision of sendOwn on the chain's first oracle messages.
Code switch between segments: in its first round the prover sends oracle messages and the verifier samples out-of-domain seeds. In its second round the prover sends the answers and the verifier samples positions, at which the oracle messages of this chain listed in read are opened. The opened values yield linear constraints on the tenants of the messages sent in the first round.
Product-tree lookup argument, in the offline IOP's form. At a sampled point, masked sumchecks along product trees relate the product over the looked-up values to that over the table's rows, with multiplicities given in bits. The claims on the parts' keys are left to the caller.
Product-tree lookup argument, as used in the online IOP: the same sequence of rounds as in card lookupKind, with one part of looked-up values, a sampled shift and 32-bit multiplicities. It outputs two lists of claims.
the file's variables
Layer-segment sumchecks, the rounds specific to a segment of layers: sampled points, batching challenges and masked sumchecks. No oracle message is sent or opened. It outputs two lists of linear claims and has a check after the batching.
Attention-segment sumchecks, the rounds specific to an attention segment: prover scalars, sampled points, batching challenges and masked sumchecks. No oracle message is sent or opened. The lists of claims that it outputs are given by the parameter claims.
the file's variables
Output-head sumchecks, the rounds specific to the output head: sampled points, batching challenges and masked sumchecks. No oracle message is sent or opened. It outputs three lists of linear claims.
the file's variables
Output-head sumchecks as used: the sub-protocol of card Head.kind with a fourth list of linear claims, named join, inserted after the first.
Next-token message: one round, in which the prover sends one field element, the next token, and the verifier samples nothing. Its public check is that the vocabulary size is at least 2. It rejects if an element was stored before or the element is not a base-field value below the vocabulary size.
Draw of the approximate range proof, the test that committed values are small: one round, in which the prover sends nothing and the verifier samples matrices with entries −1, 0 or 1. They are stored after three checks on the state (the list of parts is closed, no count of rows is owed, no matrix has been sampled yet) and checks of their sizes.
Draw of the approximate range proof, as used: the sub-protocol of the card approximateRangeProofDrawKind, together with one list of claims (K8.equations) and two steps after the segment's batching (K8.lsTail, K8.tests).
the file's variables
Segment claim batching: one round, in which the verifier samples one field element. Every claim output by the segment's sub-protocols is added to one equation, weighted by a power of that element.
Segment-closing row fold, 2 + k rounds. One sampled element batches all linear constraints on the segment's group; a masked sumcheck of 1 + k rounds leaves one constraint on its rows folded at its challenges.
Output-head committed-table sumcheck, lk + 4 rounds, in the head's segment: a batching challenge and a masked sumcheck on the head's single claim on the committed table. It outputs one linear claim.
the file's variables
Proximity test with linear constraints, taking its parts as an argument. Rounds: a batching round; for each stage except the last, a fold (1 + k rounds) and a code switch (2); a base case (2).
guardedProximityTestParts defines the parts that proximityTestKind takes as its argument, with further checks that cause rejection if they fail: (f) and (p) in the first part, (c), (k) and (g) in the batching, and (z) in every part that is given rounds. In the batching, one element is sampled. A fold is a masked sumcheck. In a code switch, the prover sends a new oracle message and earlier ones are opened at sampled positions. In the base case, the last message is sent in the clear in masked form and tested at sampled positions.
the file's variables
Committed-table claim merge, 2 + kCol rounds. One sampled element batches the two or more pending claims on the committed table; a masked sumcheck reduces them to one. No oracle message is sent or opened.
batchLinearConstraintsSecondPart is the second part of the committed-table claim reduction and has no rounds. It first makes three checks and rejects if one fails (their names in Lean: "the two ends are at hand"; "the shape does not split the row (Dot)"; "no root is received yet, and the first own tree's number counts just one tree more"). It then adopts the oracle message named in the second chain's final state, adds it to the group named in this chain's state, and adds a linear constraint on that message and another tenant to the same group. Each of these steps can also reject. Its public check is the conjunction of lengthsOk, linOk and plainArm.
the file's variables
A sub-protocol without rounds and of no kind: nothing is sent, sampled or opened, and its decision is the given update of the verifier state, which may reject.
A chain's last sub-protocol. If the chain is sealed, it has one round, named SEAL, in which nothing is sent or read; otherwise it has none. Its public check is nothingOwedOnPlan on the rounds declared by the sub-protocols before it. It accepts if the given conditions on the verifier state hold.
The type of a function that can replace the byte format's second hash function: it maps a number and a byte string to a byte string.
The data that determine the argument system. These fields are functions of the public files: C (types, relation, encoding), the three IOPs F, the provers P, a hash-oracle algorithm readMore (also a function of the files' digest), the compiler data T (also a function of that digest and of the output of readMore), an extractor, the honest commit and prove, and the parser parse. The fields shown and the honest sample are not. There are also four types: More, Shown, Rand and Form.
A configuration, without the conditions it must satisfy: types of indices, instances and cells; two relations Ryes, Rno on them; hold and enc, which encode an index with pads and randomness as n symbols; seeds, answers, a collision predicate and a decoder.
Builds a Description from parts L and a hash-oracle algorithm more. If L.live rejects the public files, empty round data are used. A proof is submitted as bytes; if decoding fails, L.f₀ is used instead.
The parts from which a Description is built, most of them functions of the public files: the relation, the index encoding, the round data of the offline and online IOPs, three verifier decisions, the provers, the extractor, the honest committer and prover, a test live, the planner's values G and Gd, the further fields it, N, hStar, d₀ and f₀, and two proofs, hf₀ and hlive.
the file's variables
Relation data on a decoded table, for instances in X: a type of matrices, the table's matrix, a range predicate, a relation Rel between matrix and instance, and a proof that the matrix depends only on entries below D.cut.
How an index is encoded: hold maps a matrix and pads to a message, enc encodes a message with randomness into 2^a symbols, and smp returns a message's answers to a seed.
The planner's values: parameters of the offline and online IOPs' chains, a function block of the instance, a sample rec₀, an instance–sample pair z₀, the batch depth depthReq, and a map early on instances.
For every choice of public files Z, the parts at Z: dataAtFilesFromRounds applied to the values of filesParametersOrDefault, keyRoundsOrEmpty and proofRoundsOrEmpty.
The parts L evaluated at one choice of public files, for given planner's values G and given round data that satisfy roundsDataFit.
L.G at the public files if L.live accepts them, otherwise L.Gd.
The offline IOP's round data L.DK if L.live accepts the public files, otherwise the empty round data emptyRoundsData.
The online IOP's round data L.DP if L.live accepts the public files, otherwise the empty round data emptyRoundsData.
Round data made from three empty lists of rounds, at table depth 0.
A check on the round data of the offline and online IOPs: in every round except the first chain's sealing round, the challenge kind's number and the number of proof-of-work bits are below 256 (kindsAndWorkBelow256), and KF DK DP + 2 < 2^49.
In every round of a file's three chains except the first chain's sealing round, the challenge kind's number and the number of proof-of-work bits are below 256.
The parts at one fixed choice of public files: DescriptionData's fields without honest, f₀, live and Gd, a number sR, and proofs of the three conditions of roundsDataFit.
the file's variables
The parts at one fixed choice of public files, in the form that descriptionOfFieldsWithReading takes. The link IOP's round data and its queries to the committed tables are the constants dsF and xsF, not fields.
the file's variables
The compiler's further data as a function of a digest c and a list of digests m, both converted to bytes and passed to inputFieldsAtReadingsAsBytes. In the verifier, c is the public files' digest and m is the output of readMore.
the file's variables
The compiler's further data for a 32-byte string c and a list of byte strings: tAt (not printed) applied to the parts' fields, c, and three values taken from the list.
the file's variables
descriptionWithDecoderAndReading with submitted proofs of type FormBytes (a list of tokens and five byte strings) and decoder decodeD.
the file's variables
descriptionOfFieldsWithReading applied to the parts (S Z).toDescriptionFields, to the honest algorithms Hn with the parser that committerAndProverWithParser builds from the decoder dec and the fallback f₀, and to the argument more as the hash-oracle algorithm readMore.
the file's variables
The honest algorithms Hn and the parser parserWithDecoder, in the form that descriptionOfFieldsWithReading takes.
the file's variables
The parser ignores the prompt and the output. It queries the hash oracle once for the public files' digest c, decodes the submitted proof given c, uses f₀ if decoding fails, and returns the typed proof.
The honest committer and prover for a proof type Form: commit and prove, the committer's randomness Rand with its sampler, and a function shown from the weights to a type Shown.
the file's variables
Defines every field of Description from parts fr Z indexed by the public files Z, the honest algorithms and parser H, and a hash-oracle algorithm more. The three IOPs are threeProtocolsAtFullSize at fr Z.
The parts that descriptionOfFieldsWithReading takes, for one choice of public files: relation, index encoding, the three IOPs' round data and decisions, provers, extractor, and the compiler's further data inputFieldsAtReadings.
The honest committer and prover, the type Form of submitted proofs, and the parser from Form to typed proofs, over a family of parts fr.
The relation and the encoding for DecR.configurationOfStoredTable: Ryes and Rno both say that the matrix M is in range and A.Rel M x holds; Cells is trivial; encoding, pads and sampler come from E.
the file's variables
The data that DecR.configurationOfStoredTable takes in addition to D and A: the two relations and the type Cells of their third argument, the encoding and its randomness, the pads, the message hold that contains an index with given pads, the sampler, a function trace into Cells, and a value cells0.
the file's variables
A committed table's configuration: index type A.Mat, words of 2^a symbols; seeds, answers, collision predicate and decoder from D; relations and encoding from R. held returns a message's matrix exactly when that matrix is in range.
the file's variables
The three IOPs at the full parameter size: filesAt over the field of size 2^64 − 2^32 + 1, with N = 2^depthReq, late = none, and checks silK, silP on the challenge-free rounds.
the file's variables
filesOf applied to the fields of DecR.configurationOfStoredTable A R: index type A.Mat, tables of 2^a symbols, the seeds and answers of the out-of-domain sample, and the relation and encoding from R.
the file's variables
Constructs a value of Files. The offline and online IOPs are reductionOfWholeFile applied to their round data (table depth set to a), checks and decisions, converted by toInteractiveOracleProof. The link IOP and its round marking come from eL.
Three public-coin IOPs over a configuration C. The offline IOP has an out-of-domain sample as its instance and the encoded index as its oracle. The link IOP has two of each. The online IOP has an element of type C.X together with a sample as its instance, and one encoded index as its oracle. The structure also contains N, the round markings, early and late.
the file's variables
Combines the three IOPs, the provers, and the configuration's encoder, sampler and index decoder into a value of Iop.HolographicProtocol, which the compiler takes as input. Here offline and link are the offline and link IOPs, and onlineBatch is the online IOP with its round marking.
the file's variables
A file's three chains as one interactive oracle reduction to the trivial statement, with a challenge-free round before each chain. It accepts if and only if all proof-of-work bits are 0 and fullOf, carriesOf, silent and run accept.
the file's variables
Views an interactive oracle reduction to the trivial statement as an IOP with the same rounds and queries. The IOP accepts if and only if the reduction returns an output.
The part of linkProtocolWithWireAtFullSize that filesOf takes, at K = 0: the link IOP, its round marking, and the two maps between oracle symbols and bit strings.
The link IOP's data for filesOf: the IOP, with instance type R × R over two oracle strings of 2^a symbols; its round marking; and two maps between oracle symbols and bit strings.
The link IOP at the full parameter size with its encoding data, built by linkProtocolWithWireOfRoundData from round data ds, table queries xs and decision dec, with K 256-bit digests for a verifier message.
The link IOP linkProtocolOfRoundData, the round marking allLo in which no round is shared, the two maps between oracle symbols and bit strings, the number K, and encoding data wL for the compiler.
the file's variables
The link IOP over two committed tables: linkSkeletonOfRoundData at round data ds, table depth a, table queries xs and decision dec, after the generic conversions .up and .loc (not printed).
the file's variables
The link IOP before the conversions .up and .loc: rounds, queries and flags of skeletonOverBothExternalStrings. It accepts exactly when all proof-of-work bits are 0, everyOpeningHasItsDraws and symbolsCarryTheirPositions hold, and dec x accepts the view.
An IOP over two committed tables, with a trivial instance, before two conversions. It accepts if and only if all proof-of-work bits are 0, each table query has its full share of the sampled positions (everyOpeningHasItsDraws), each symbol queried in a table has its position as its first component (symbolsCarryTheirPositions), and dec accepts.
True if every table query's round exists and its share contains count sampled positions.
True if every queried table position is below 2^a and the symbol read there has that position as its first component.
This protocol's parts at o: flashProveDataNoExtractorAtHash o with its extractor field set to theExtractorAt o.
This protocol's parts at o, field by field, with an extractor that returns nothing. Its provers send fixed messages; its honest committer and prover return fixed values.
This protocol's relation data, of type Claims: claimsReqAt (not printed) applied to full-size constants and to the table that ppAtFiles reads from the parameter and scale files, or a fixed reference table if reading fails.
This protocol's index encoding, of type Coding: codingCells (not printed) applied to the same constants and table as theClaims.
This protocol's provers: Files.fixedMessageProvers, which send every round's fixed default message.
The constant committer and the constant prover, fixedCommitterAndProver. They supply fields of the protocol's record that the types require but that neither compile nor the verifier reads. The six theorems take their honest provers and settings from honestProversAndSettings.
A constant committer and prover with trivial types: commit returns the all-false commitment and prove an empty list of tokens with five empty byte strings; neither makes a query.
The offline IOP's decision as used in the protocol: theKeyRunAt, except that it rejects everything if protocolDataWellFormedAt rejects the public files.
The online IOP's decision as used in the protocol: theProofRunAt, except that it rejects everything if protocolDataWellFormedAt rejects the public files.
The link IOP's decision as used in the protocol: linkDecisionAtFiles, except that it rejects everything if protocolDataWellFormedAt rejects the public files.
A three-view decision guarded by a Boolean: it accepts exactly when live is true and run accepts.
The one-view decision that accepts exactly when live is true and dec accepts.
The test on the public files: the planner's values and the round data of the offline and online IOPs can all be computed, and dataWellFormedAtFullSizeDepth accepts them.
The offline and online IOPs' round data have the full-size committed table's depth, and dataWellFormedApartFromDepth holds.
sizeNumbersFitAtPlan holds at KF and the bound 2^20 (eight numeric conditions on all three IOPs' round data and two depths of G, sizeNumbersFitAtFullSize), and none of the six lists of rounds is empty.
the file's variables
sizeNumbersFitAtFullSize at K = KF DK DP, the bound v, two depths taken from G, the offline and online IOPs' round data, and the link IOP's constants dsFull and frD.xs.
A conjunction of eight numeric conditions on the three IOPs' round data, the bounds K and v, and two depths. The functions that it calls are not printed.
None of the six lists of rounds (three chains of the offline IOP, three of the online IOP) is empty.
Given o and the public files, returns the planner's values of type FilesParameters, or an error. The planner runs with the constant fixedConfigurationDigest in place of the public files' digest.
The value of filesParametersOrRefusalAt, or a fixed default if it returns an error.
The offline IOP's verifier decision, a function from a committed table's out-of-domain sample and three views to a Boolean: the second component of keyDataAndDecisionOrRefusalAt, or, if that returns an error, the decision that rejects everything.
The offline IOP's round data: the first component of keyDataAndDecisionOrRefusalAt, or, where that returns an error, the round data of three empty chains.
Given o and the public files, returns the offline IOP's round data and verifier decision, or an error. publicOfO reads and checks the files, applying o; keyDataAndDecisionAtFixedDigest builds the written IOP and runs its public checks.
keyDataAndDecisionAtDigest at the constant fixedDigest: the offline IOP's round data and decision from the parsed public files and the layout file, or an error.
The digest used to build the written offline IOP: the constant fixedConfigurationDigest.
A constant: 32 bytes of value 1. When the written offline and online IOPs and the planner's values are built, the planner receives it in place of the public files' digest.
A reader who applies the tests in Judging the assumptions on the public files and on hash values encounters this constant. The protocol as Lean describes it is written with this constant in place of the digest; the true digest enters through the coding of the queries, the query for the out-of-domain seed and the commitment's code, as found by reading the Lean code, and no theorem says that every challenge depends on it (lean/GAPS.md, 5).
Runs the planner madeAt on the parsed public files, the layout file and a digest, then keyDataAndDecisionOfPlannerAnswer on its result.
Builds the written offline IOP from the planner's result and computes its round data and decision with keyDataAndDecisionOfDescription; returns an error if either step fails or if one of the further public checks lawsAsk fails.
The written offline IOP descriptionFromSource X N P, whose three arguments are computed from the planner's result, or an error if one of them cannot be computed.
Returns the round data F.data of the written offline IOP F and its decision F.run applied to the instance made from an out-of-domain sample, or an error if F.planWord reports a failure or if wantedOk, owedOk or F.data fails.
The type of the makers' result for the offline IOP: an error message, or round data with a decision.
The type of the offline IOP's decision: from an out-of-domain sample and three views to a Boolean.
The offline IOP's instance as the written IOP takes it, computed from a committed table's out-of-domain sample.
the file's variables
The round data of a written IOP, computed from its declared rounds F.roundsDeclaredByBlocks and its table depth; an error if the conversion or its checks fail.
The online IOP's verifier decision, a function from a request, a committed table's out-of-domain sample and three views to a Boolean: the second component of proofDataAndDecisionOrRefusalAt, or, if that returns an error, the decision that rejects everything.
The online IOP's round data: the first component of proofDataAndDecisionOrRefusalAt, or, where that returns an error, the round data of three empty chains.
Given o and the public files, returns the online IOP's round data and verifier decision, or an error. It builds the written online IOP and fails unless that IOP's public checks pass.
Builds the written online IOP from o and the public files with ProofFile.onlineDescription, then computes its round data and decision with proofDataAndDecisionOfDescription; returns an error if either fails.
Returns the round data F.data and the decision proofDecisionOfDescription F of the written online IOP F, or an error if F.planWord reports a failure, F.data fails, or one of the further public checks lawsAsk fails.
The online IOP's decision: F.run applied to the instance that instanceAsPlainRecord constructs from a request and an out-of-domain sample.
The online IOP's instance as the written IOP takes it, computed from a request and a committed table's out-of-domain sample.
The link IOP's verifier decision on two out-of-domain samples and one view. It reads only the parameter file: if the file's first 32 lines equal fixed full-size lines, it is the written IOP's decision; otherwise it rejects everything.
linkAt P plan returns the written link IOP F at parameters P, built by linkDescriptionAt with linkDeclaredRounds P as its declared rounds and linkRoundsMatchPlan P plan as its public check, together with its round data and its table queries. It returns an error if F.planWord reports a failed public check or if the round data cannot be formed.
The declared rounds of the link IOP's chain at parameters P.
Public check: the schedule entries of the link IOP's declared rounds equal the rounds of the given schedule.
VerifierAndGoals.storedLines has no card on this page; it is in the Lean file Ladder/Stored.lean:237.
(1) blake2bHash is the function that leanVerifier uses in place of the random oracle. It is not plain BLAKE2b; it is computed as follows:
Fmt.formatHash (a number, a tree, an index, a start, bytes), and the output is 32 bytes of BLAKE2b of that call, with bytes 0 to 15 of the start as salt and bytes 16 to 31 as personalization;(2) secondHashFunction is the fixed function in the protocol's description: BLAKE2b's compression function with a number and the input's length in 32-bit words (rounded down) in the high word of the counter. In the statements, (1) is sampled at random and (2) is fixed.
The concrete hash function that replaces the random oracle when a proof is checked. It writes the bit string as bytes, applies Fmt.oracle to them, and returns 256 bits of the result (hashOf, the next card). Fmt.oracle first parses the bytes as a call of Fmt.formatHash (oParse), then applies BLAKE2b.
The hash function on bit strings obtained from a function O from bytes to bytes: the input is written as bytes, O is applied, and the first 256 bits of the result are returned, padded with zeros if the result is shorter (gOf, OnBytes/TypedOracleCompiler/Run/PageRunFast.lean:46).
the digest's length in bytes dlen; a salt and a personalization; a message
Run.Blake2b.blake2bSaltedPlain applied to them
a byte string
parse it as a half (0 or 1) and one call of Fmt.formatHash: a number, a tree, an index, a start and bytes (oParse)
it is not such a call: Fmt.formatHash of the whole string, with number 177, tree 0, index 0 and an all-zero start (oOut)
it is one, and its half is 0 or its number is 162 (oUsed):
the digest of Fmt.formatHash for that call (next card);
its bytes 0 to 31 if the half is 0, otherwise bytes 32 to 63
else: as in the case where it is not such a call
three numbers: number, tree, index; two byte strings: start, bytes
blake2b, the library's unkeyed BLAKE2b, with a 64-byte digest if the number is 162 and a 32-byte digest otherwise (dlen);
salt: bytes 0 to 15 of the start, which is truncated or padded with zeros to 32 bytes;
personalization: its bytes 16 to 31;
message: the label, then the bytes
the arguments of Fmt.formatHash (the card above)
Fmt.HF: the definition of Fmt.formatHash, with blake2bF in place of blake2b
formatHashFastForm and Fmt.formatHash are the same function
a number num; a byte string w
n: the number of whole words of 32 bits in w
full: the number of blocks of 128 bytes before the last block
the high word of the counter, in every call: num + 2^32 · n, modulo 2^64
for each of the full blocks in turn:
apply BLAKE2b's compression function (Run.Blake2b.compress) to that block; the counter's low word is the number of bytes up to the block's end
starting from the first state of BLAKE2b with no key and 64 bytes of output
the compression function once more,
with the last-block flag set and 4 · n as the low word of the counter,
on the last block; the eight chaining words of the resulting state
a number num; a byte string w
the first 32 bytes of secondHashFunctionState num w (the card above)
a byte string w
if its length is not a multiple of 4 bytes or is less than 32 bytes: nothing
otherwise, it is hashed level by level (secondHashFunctionTreeLevels), at least once, until 32 bytes remain; nothing if this takes more than 16 levels
The BLAKE2b chaining value, one field per word.
One BLAKE2b message block as sixteen words.
BLAKE2b's work vector of sixteen words.
The four words that BLAKE2b's function G changes.
BLAKE2b's eight initial constants.
The 64-bit word w rotated right by c bits.
The mixing function: additions, exclusive-ors and rotations by 32, 24, 16 and 63 bits, on four words of the work vector and two message words.
One round: eight calls of G, on the four columns and then the four diagonals of the work vector, with sixteen message words in the order that the caller gives.
The hashing state: the chaining value, a two-word counter of the bytes processed, and two flag words. The first flag word marks the last block; the second is 0 in every state that the definitions of Hash.lean and Salted.lean produce from init0.
The compression function: the work vector from the state and the constants, twelve rounds, each with the message words in the order of its row of the schedule, and the new chaining value.
Byte i as a 64-bit word, or 0 past the end.
The 64-bit little-endian word at offset k; missing bytes are read as 0.
The 128 bytes at an offset as sixteen words, zero-padded.
The state with a number added to its two-word counter, with carry.
The state with the next block marked as the last.
The state whose chaining value is the initialization vector and whose other words are all 0.
The state after the eight words of the parameter block are XORed into the initialization vector.
The first word of the parameter block: output length, key length, fanout 1, depth 1.
The first state, for an output length, a salt and a personalization.
The state after a number of blocks, none of them the last, are compressed: the counter is increased by 128 before each block.
The state after the last block is compressed: the counter is increased by the block's length, and the block is marked as the last.
The state after a whole message of inlen bytes.
The state after a whole message, starting from the first state.
Appends the eight little-endian bytes of a word to an array.
The state's eight words as 64 little-endian bytes.
The digest: the first outlen bytes of the state's 64 bytes.
BLAKE2b of a byte string with a salt, a personalization and no key. The result is the empty array if the output length is 0 or greater than 64.
This appendix presents the integer model, from the definitions named in CanServe and requestOutcome (modelNextToken, RequestForm, requestResult) down to arithmetic.
The cards. A card names the definitions that it uses. Each of these, except those of Lean's own library, has its own card in this appendix (the five packed arrays of numbers are named but not printed). The small auxiliary definitions (such as entry, tabulate, sumOver, roundShift, clamp) are in the last folded section.
Range conditions. A range condition is a bound outside which the model is undefined (allConditionsHold).
The files. The Lean code is in IntegerModel/Model.lean (725 lines), VerifiableInference/ModelWeights.lean and VerifiableInference/RequestResult.lean, with one definition from IntegerModel/Window.lean; the first card is from VerifiableInference/Statements.lean.
The comments in the Lean code. A short comment at the end of a Lean line, such as -- Vx or -- sigma, gives the symbol for that value in docs/model.md ("The integer model"); "section 7" in two comments refers to a section of that file. The numbers 1 to 8 in the comments of the range conditions enumerate these conditions. The definitions can be read without these comments.
A Token is a natural number.
The type imposes no upper bound; RequestForm requires each token of a request to be less than settings.vocabulary.
settings, weights at these settings (ModelWeights),
a prompt and a claimed output
the model is run on one window of 1,024 tokens: the prompt, the claimed output, then zeros (zeroFilledWindow)
if the model has a value on this window (modelNextToken returns some token):
the choices of this run (trace, its field choices, one for each of the 1,024 positions)
the result is some list of these choices, starting at position prompt.length - 1 (0 for an empty prompt): as many as the claimed output has tokens, or fewer if the window ends first
if the model has no value on this window (modelNextToken returns none), the result is none: failure
RequestForm is not tested here.settings, a prompt and an output
settings.vocabularysettings.positions (the number 1,025 is a literal).zeroFilledWindow), so the window does not contain the 1,025th token.zeroFilledWindow prompt output is the prompt, then the output, then zeros, truncated to exactly 1,024 tokens: (prompt ++ output ++ List.replicate 1024 0).take 1024.
settings, weights at these settings (ModelWeights), a list of tokens
the output of the integer model (IntegerTransformer.model) on these settings, the library's lookup tables (lookupTables), these weights and these tokens: the next token, or nothing
the settings s; five lookup tables (cosine, sine, exponential, SiLU, sigmoid); weights; the tokens so far
if the arguments fit together (wellFormed), and there are from 1 to s.positions tokens, each below s.vocabulary (isPrompt):
all values of the model, at every position (trace);
if these values satisfy the range conditions (allConditionsHold): the choice at the last position
in the other two cases: nothing
the settings s; tokens, as numbers
there is at least one token, there are at most s.positions,
and each is below s.vocabulary
An IntegerVector, or vector, is an array of unbounded integers (Int).
A Matrix is an array of vectors, which are its rows.
the settings of the model:
the largest number of tokens (isPrompt)
the number of layers (trace)
the number of entries of a row of the residual stream (attention, feedForward)
the number of query heads; the number of key and value heads; the number of entries of one head (attendHead)
the hidden units of a feed-forward block; those of one expert; the number of routed experts (feedForward, routedExpert)
the number of tokens: a token is a number below it (isPrompt)
an exponent: in a layer whose rotary is false every cosine is 2 to this power (projections)
the offset, the exponent and the shift of the final normalization (trace, rmsNorm)
for each layer, its settings (LayerSettings, next card)
the type has a default value
the settings of one layer:
the exponent, the shift and the offset of the normalization before attention (attention, rmsNorm)
the shifts of queries, keys and values (projections)
whether this layer reads the cosine and sine tables (projections)
the shift of a score's distance to the largest score (attendHead)
the shift after the output matrix (attention)
the exponent, the shift and the offset of the normalization before the feed-forward block (feedForward)
the shifts after the gate, up and down matrices (feedForward)
the shifts after the router's matrix and the chosen expert's gate and up matrices (routedExpert)
the type has a default value
s.queryWidth is queryHeads * headDim, the number of entries of all query heads together.
s.keyValueWidth is keyValueHeads * headDim, the number of entries of all key heads together, and of all value heads together.
s.isMixture l tests whether layer l is a mixture-of-experts layer: the number of routed experts is positive and l is odd.
the weights:
the embedding matrix: a row for each token (trace)
for each layer, its matrices (LayerWeights, next card)
the matrix that gives the logits (trace)
the type has a default value
the weights of one layer:
the matrices for queries, keys and values (projections)
the output matrix (attention)
the gate, up and down matrices (GatedWeights) of the block that every layer has (feedForward)
the router's matrix (routedExpert)
the gate, up and down matrices of each routed expert (routedExpert, feedForward)
the type has a default value
A GatedWeights consists of the three weight matrices of one gated feed-forward block: gate, up and down.
A Tables consists of the five lookup tables that the model reads:
the cosine table
the sine table
the exponential table of the softmax
the SiLU table
the sigmoid table
A KeyedTable is a lookup table whose keys are consecutive integers starting at lowestKey, which may be negative; entries[0] belongs to the key lowestKey.
table.read key is the entry of table at key, or 0 if table has no entry at key.
A Trace contains the intermediate values of the model on given input tokens, from the embedded tokens to the logits and their argmax at each position.
the four arguments of model: settings s, lookup tables, weights, tokens
for each token, its row of the embedding matrix
the s.layers layers, each applied to the output of the one below it (firstLayers, layer)
the output of the last layer (the embedded tokens, if there is no layer)
the final normalization of each of its rows (rmsNorm)
the logits: each normalized row times the matrix weights.head
at each position, the least token with the largest logit (firstArgmax)
all of these, in one structure
the settings; the lookup tables; all weights; the embedded tokens; a number
that many layers, with all their values:
for 0: none
for l + 1: the first l layers,
followed by layer l (layer),
applied to the output of the last of them, or to the embedded tokens if there are none (streamAbove)
streamAbove embedded below is the residual stream that leaves the last layer of the array below, or embedded if below is empty.
A Layer contains the values of one layer at all positions:
the residual stream that enters the layer
the Attention
one FeedForward for each position
the residual stream that leaves the layer
the settings s; the lookup tables; all weights; the number l of the layer; the residual stream x, one row for each position
the values of the layer at all positions (Layer):
attention (attention), with the settings and the weights of layer l, on x
on each row of its output, the feed-forward block (feedForward);
with routed experts if s.isMixture l: there are experts, and l is odd
x, both results, and the layer's output: the outputs of the feed-forward block, row by row
A Norm contains the values of one normalization of one vector:
the sum of squares
the integer square root of that sum plus the offset
the scaled reciprocal of the root
the quotient (the result before clamping)
the result out
an exponent bits, a shift, an offset eps; a vector x of integers
the sum of the squares of x's entries
the integer square root (integerSquareRoot) of that sum plus eps (of 0 if that is negative)
2 to the power bits, plus half of root, divided by root
each entry of x times reciprocal, divided by 2 to the power shift and rounded (roundShift)
each of these clamped to the interval from −2,047 to 2,047 (clamp, activationBound)
all five, in one structure (Norm)
An Attention contains the values of one layer's attention at all positions; out is the residual stream after attention.
the settings s; the layer's settings p; the lookup tables; the layer's weights w; the residual stream x: one row for each position
the values below, in one structure (Attention)
the normalization of each row (rmsNorm), with the layer's exponent, shift and offset
at each position t: queries, keys and values from the normalized row (projections)
at each position, for each query head: its attention (attendHead)
at each position: the heads' results concatenated, s.queryWidth entries
each such row times the output matrix, each entry divided by 2 to the power p.outputShift and rounded
at each position: the row of x plus that row (addVectors)
all six
A Projections contains the queries, keys and values of one position in one layer, and the intermediate values from which they are computed.
the settings s; the layer's settings p; the lookup tables
the layer's weights w; a position t; a vector a (in attention: the normalized row at t)
the values below, in one structure (Projections)
the cosines: if p.rotary, row t of the cosine table; else s.headDim / 2 entries, each 2 to the power s.rotaryScale
the sines: if p.rotary, row t of the sine table; else as many zeros
a times the query matrix (product): s.queryWidth entries
a times the key matrix: s.keyValueWidth entries
both rotated by these cosines and sines, pair by pair within each head (rotate)
each entry divided by 2 to the power p.queryShift (for keys: p.keyShift) and rounded (roundShift)
each entry clamped to the interval from −2,047 to 2,047 (clamp): the queries and the keys
a times the value matrix, each entry divided by 2 to the power p.valueShift and rounded
each entry clamped in the same way: the values
all ten
rotate applies the rotary position embedding: in each head of headDim entries of A (headDim even) it maps the entries (a, b) at 2i and 2i + 1 to (c * a - s * b, s * a + c * b), with c = cosine[i] and s = sine[i].
A Head contains the values of one query head's attention at one position:
the scores
the largest score
the scores' scaled distances to it
the exponentials
their total
the weighted sum of the values
the result out
the settings s; the layer's settings p; the lookup tables
the queries, keys and values of all positions; a position i; a query head h
the values below, in one structure (Head)
dh: the number of entries of one head
g: h divided by the number of query heads for each key and value head
for each position j from 0 to i: the inner product of head h's query at i and head g's key at j
the largest of these scores (maxUpTo)
for each score: top minus the score, divided by 2 to the power p.softmaxShift
for each distance, its exponential: the entry of the exponential table at that distance, or 0 if the distance is not less than the table's size
the sum of these exponentials
for each entry c of a head: the sum over j of j's exponential times entry c of head g's value at j
each of these sums, doubled, plus total, divided by twice total
all seven
A FeedForward contains the values of one layer's feed-forward block at one position; out is the row that leaves the layer.
the settings s; the layer's settings p; the lookup tables; the layer's weights w
whether the layer has routed experts, mixture; a row x of the residual stream
the values of the block at one position (FeedForward):
the normalization of x (rmsNorm), with the layer's exponent, shift and offset for it; m is its result
with routed experts: the s.expertHidden hidden units of the shared block, evaluated on m;
the router and the expert that it chooses (routedExpert), on m;
for each of the s.width entries: the down projection of the shared block (downSum),
plus that of the chosen expert; the sum divided by 2^p.downShift and rounded
these values; the block's output is x plus addition, entry by entry (addVectors)
without routed experts: the s.hidden hidden units of the single block, evaluated on m;
for each entry: its down projection, divided by 2^p.downShift and rounded
these values, with empty vectors for the router (noRoute); the output is x plus addition
A HiddenUnits contains, for each hidden unit of one gated feed-forward block:
the gate value
its balanced low byte
its high part (gate value - low byte) / 256 before clamping
its high part after clamping
the key into the SiLU table
the activation
the up value
downSum units down k is entry k of a block's down projection before the rounding shift: the sum over the hidden units j of activation[j] * up[j] * down[j][k].
A Routed contains the router's values at one position:
the logits before clamping
their values with the three low bits dropped (logit / 8, rounded down)
these bits (logit % 8)
the clamped logits
the chosen expert
its scale
the scaled input
the chosen expert's hidden units
the settings s; those of the layer p; the lookup tables; the layer's weights w; a vector m
the router's values, and the hidden units of one expert (Routed):
m times the matrix w.router, one entry for each expert, each divided by 2^p.routerShift and rounded
each entry divided by 8, rounded down;
and its remainder, from 0 to 7
the logits: the quotient, clamped to the interval from −2,047 to 2,047, times 8, plus the remainder
the least expert with the largest logit (firstArgmax)
the entry of the sigmoid table at that logit
each entry of m times scale, divided by 2^16 and rounded
the hidden units (hiddenUnits) of the chosen expert's block, s.expertHidden of them, with the shifts p.routedGateShift and p.routedUpShift, on input
all eight, in one structure
noRoute is the Routed value of a dense layer: every vector is empty, and chosen and scale are 0.
the settings s; all values of the model (Trace)
at every position t,
in every layer l:
the conditions on attention hold (attentionOk): those on its normalization hold, and each entry of the queries, keys and values before clamping is in the range −32,768 to 32,767;
the conditions on the feed-forward block hold (feedForwardOk): those on its normalization, on the shared and the routed hidden units, and on the router's quotients;
and the conditions on a normalization hold at the final normalization (normOk)
attentionOk p a t tests the range conditions of one layer's attention at position t: normOk of the normalization, and fits16 of the queries, keys and values before clamping.
feedForwardOk p ff tests the range conditions of a feed-forward block at one position: normOk, unitsOk applied to the shared and to the routed hidden units, and fits16 applied to the wide router logits (before clamping) with the three low bits dropped.
normOk eps n tests the range conditions of one normalization: the sum of squares plus eps is below 2^78, and the quotient passes fits16.
unitsOk units tests the range conditions of one gated block: the high part of every gate value, before clamping, lies in the range from -16,384 to 16,383, and the up values pass fits16.
fits16 v tests whether every entry of v is a signed 16-bit number, from -32,768 to 32,767.
settings
the arrays of weights (Weights) that pass the test weightsAreValid at these settings
weightsAreValid settings weights tests wellFormed (applied to settings, lookupTables and weights) and weightsInRange.
the settings s; the lookup tables; all weights
the numbers of key-value heads and query heads are positive, and the first divides the second
the width of a head is positive and even; the vocabulary is not empty
there are no experts, or s.hidden is twice s.expertHidden
the final normalization's offset and its shift are at least 1
the lookup tables for cosine and sine have s.positions rows, each of half a head's width
the table for the exponential is not empty, its first entry is positive, and no entry is negative
the table for SiLU has all keys from −32,768 to 32,767, and the table for the sigmoid has all keys from −16,384 to 16,383
the embedding matrix has s.vocabulary rows of s.width entries, and the matrix weights.head has s.width rows of s.vocabulary entries
there are settings and weights for exactly s.layers layers
in each layer, the matrices that the layer reads have the sizes given by the settings, and the two offsets and the shifts passed to roundShift are at least 1 (layerWellFormed; softmaxShift is not tested)
the settings s; the layer's settings p; the layer's weights w; whether the layer has routed experts, mixture
the query, key, value and output matrices have the sizes that s gives
the layer's two offsets are at least 1
every shift passed to roundShift is at least 1 (the shifts of the router and the routed experts are treated below)
the router and the routed experts are tested only if mixture is true; then the matrices of the shared block, the router and each of the s.experts routed experts have the sizes given by s,
and their three shifts are at least 1
otherwise the matrices of the shared block have the sizes that s gives
softmaxShift is not tested here; layerSettingsInRange in VerifiableInference/ModelWeights.lean requires 4 ≤ softmaxShift ≤ 12.
hasSize rows columns W tests whether W has rows rows of columns entries each.
w.hasSizes d h tests whether gate and up have d rows and h columns, and down has h rows and d columns.
table.covers low high tests, for low ≤ high, whether table has an entry at every key from low to high.
settings; weights
every embedding entry is in the range from -2,155,905,152 to 2,139,062,143 (four signed bytes in base 256)
every entry of head is in the range from -4,096 to 4,095
layerWeightsInRange holds for each of the 48 layers
layerWeightsInRange mixture layer tests whether every weight of the layer is in the range from -4,096 to 4,095; in a dense layer the router matrix and the array of routed experts must be empty.
gatedWithin block tests whether every entry of the block's three matrices is a signed 13-bit number, from -4,096 to 4,095.
entriesWithin low high matrix tests whether every entry of matrix is in the range from low to high.
lookupTables is the Tables value made of the five tables on the next cards, with lowest key -32,768 for SiLU and -16,384 for the sigmoid.
cosineTable has 1,024 rows, one for each position, each with 64 entries, one for each pair of entries of a head. Entry pair of row position is entry 64 * position + pair of the packed array Inst.Model.Data.cos (packedEntry, 14 bits), minus 4,096, clamped to the interval from -4,096 to 4,096.
sineTable has the same size and is read in the same way from the packed array Inst.Model.Data.sin.
exponentialTable, the exponential table of the softmax, has 2,307 entries. Entry distance is entry distance of the packed array Inst.Model.Data.exp (packedEntry, 13 bits), clamped to 1 .. 4,096.
Intended content: 4,096 times exp (-distance / 256), rounded to the nearest integer, from 4,096 down to 1.
siluTable has 65,536 entries; entry index corresponds to the key index - 32768. The key is first clamped to -16,384 .. 16,383. The entry is then the entry of the packed array Inst.Model.Data.silu at the clamped key plus 16,384 (packedEntry, 13 bits), minus 4,095, clamped to -4,095 .. 4,095. Below and above these keys the table is constant.
sigmoidTable has 32,768 entries. Entry index is 16 times the smaller of 4,096 and entry index of the packed array Inst.Model.Data.sigm (packedEntry, 13 bits).
packedEntry packed bits index is entry index of an array of natural numbers, each of which packs 1,024 entries of bits bits, lowest bits first; beyond the array it is 0.
v.entry k is entry k of the array v, counted from 0, or the element type's default value (0 for a number) if k is outside the array.
tabulate n f is the array of n entries whose entry i is f i.
sumOver n f is the sum f 0 + f 1 + ... + f (n - 1), which is 0 for n = 0.
maxUpTo f i is the largest of the i + 1 values f 0, ..., f i.
firstArgmax f n is the argmax of f over the indices below n, with ties going to the lowest index; it is 0 for n = 0.
roundShift a k, the rounding shift of a by k, is a / 2^k rounded to the nearest integer, ties upward, for k ≥ 1; it is a + 1 for k = 0.
clamp a b is a clamped to the interval from -b to b, that is, min (max a (-b)) b.
activationBound is 2,047 = 2^11 - 1, the bound to which normalized rows, queries, keys and values are clamped.
balancedLowByte a, the balanced low byte of a, is the integer from -128 to 127 that is congruent to a modulo 256.
integerSquareRoot a is the integer square root of the natural number a, the largest r with r * r ≤ a, computed by recursion on a / 4, rounded down.
addVectors x y is the entrywise sum of the vectors x and y, with as many entries as x.
product x W outputs is the vector-matrix product of x and W, with outputs entries: entry j is the sum over k of x[k] * W[k][j].
All 1,558 embedded declarations, searchable by name or file.