Running the input's calculator and processor on a clamped description and a clock #
The linear-constraints processor of the tailored introspection verifier (issue #281, P3e) needs,
at index m = 2^n, the input's answer lengths T.lenOf m q κ (to split the input's answers in
the padded layout) and its constraints T.consOf m qx qy aR bR (the source check). Its own
description must have size ≤ C (λ + 1)^C whatever the input, so the input's programs cannot be
embedded as they are. This module does what MIPRE.Introspection.seven does for normal form
verifiers:
clamp, on((S, L, P), λ), replaces every program of size aboveλbyProg.nil(SourceDescriptionCompiler.clampProgram, applied three times), keepingλ. It is the identity on the programs of aλ-bounded verifier (clamp_bounded), and its output has size at most19 (λ + 1)whatever the input (clamp_size).runLen UandrunLp Utake a unary clock, a program description as data, and the arguments, and run the program through the clocked universal machineU(ClockedQuery.run, asClockedSourceChecksdoes):runLenreads the output as a length (its spine, asLenIsdoes, and0on a timeout, aslenOfdoes whenlendiverges),runLpas a constraint list (bitsListD, asLpIsdoes, and the rejecting list[rejectConstraint 0]on a timeout, a timeout being a rejection).lenRun UandlpRun Uread the program from the clamped metadata((S, L, P), λ), as the decision kernel ofsevenreads its source decider fromDecisionPreparation.Metadata.
Correctness (runLen_eq, runLp_eq, lenRun_clamp, lpRun_clamp): for a λ-bounded T,
m ≥ 2, and a clock of length at least the running-time bound IsBounded gives,
m^λ (|args| + 1)^λ, the runs compute T.lenOf m q κ and T.consOf m qx qy aR bR exactly.
At m = 2^n, n ≥ 1, with questions and readable answers of length at most (2^n)^λ, the
clock ansBound 5 λ n = 2^{(λn + 1)^5} that seven computes suffices (len_clock_le,
lp_clock_le; lenRun_seven, lpRun_seven), and any clock at least as long
(ansBound_mono).
A λ-bounded tailored verifier has λ ≥ 2: every program has size at least 2.
The stored description of the input: its three programs and the parameter λ.
Equations
Instances For
The arguments of the answer-length calculator: (m, q, κ).
Equations
Instances For
The arguments of the linear-constraints processor: (m, qx, qy, aR, bR).
Equations
Instances For
Clamping the description #
Clamp the three programs independently to size λ, keeping λ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Otherwise each program is kept or replaced by Prog.nil: nothing else enters.
The clamped answer-length calculator.
Equations
Instances For
The clamped linear-constraints processor.
Equations
Instances For
The clocked runs #
Run a stored program on encoded arguments, for at most the clock's length.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An in-budget run is read back with its success tag.
A clocked result read as a length: the spine of the result, 0 on a timeout.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A clocked result read as a constraint list: bitsListD of the result, and the rejecting
list on a timeout.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The clocked answer-length calculator, on (clock, L, (m, q, κ)).
Equations
Instances For
The clocked linear-constraints processor, on (clock, P, (m, qx, qy, aR, bR)).
Equations
Instances For
On a timeout, the length read is 0 and the constraint list rejects.
Correctness for a bounded input #
The clocked calculator computes lenOf for a λ-bounded input at an index m ≥ 2,
when the clock covers the input's running-time bound m^λ (|(q, κ)| + 1)^λ.
A bounded input's calculator halts at every question of an index m ≥ 2.
The clocked processor computes consOf for a λ-bounded input at an index m ≥ 2,
when the clock covers the input's running-time bound m^λ (|(qx, qy, aR, bR)| + 1)^λ.
Reading the program from the clamped description #
The calculator run, its program read from the description ((S, L, P), λ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The processor run, its program read from the description ((S, L, P), λ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
lenOf from the clamped description, for a λ-bounded input.
consOf from the clamped description, for a λ-bounded input.
The clock at m = 2^n #
The introspection clock grows with its exponent and its parameter.
The processor's running-time bound at 2^n, on questions and readable answers of length at
most (2^n)^λ, is within seven's clock 2^{(λn + 1)^5}.
The calculator's running-time bound at 2^n, on a question of length at most (2^n)^λ, is
within the same clock.
lenOf at 2^n with seven's clock, or any longer one.
consOf at 2^n with seven's clock, or any longer one.