Documentation

Complexitylib.Circuits.OracleInlining.Adaptive

Fixed-round adaptive oracle circuit programs #

This module compiles every query of a fixed-round adaptive oracle program into one ordinary circuit. Correct oracle circuits give exact semantic preservation, and the size recurrence records every query, oracle, and retained-history cost.

source
theorem Complexity.AdaptiveOracleProgram.inlineHistory_eval {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) {oracle : BooleanOracle} (himplementation : implementation.Implements oracle) (input : BitString inputWidth) (completed : ℕ) (hcompleted : completed ≤ rounds) :
(program.inlineHistory implementation completed hcompleted).snd.eval input = program.history oracle input completed hcompleted

Inlining correct oracle circuits produces the exact semantic history after every prefix of the adaptive computation.

source
theorem Complexity.AdaptiveOracleProgram.inlineHistory_size {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) (completed : ℕ) (hcompleted : completed ≤ rounds) :
(program.inlineHistory implementation completed hcompleted).snd.size = program.inlineHistorySize implementation completed hcompleted

The compiled history circuit has exactly the recursively accounted size.

source
theorem Complexity.AdaptiveOracleProgram.inline_eval {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) {oracle : BooleanOracle} (himplementation : implementation.Implements oracle) (input : BitString inputWidth) :
(program.inline implementation).snd.eval input = program.eval oracle input

Inlining correct oracle circuits preserves the complete adaptive program's output on every input.

source
theorem Complexity.AdaptiveOracleProgram.inline_size {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (implementation : program.OracleCircuitImplementation) :
(program.inline implementation).snd.size = program.inlineHistorySize implementation rounds ⋯ + program.final.size

The fully inlined circuit has the exact history-prefix cost plus the final output circuit's size.