Documentation

Complexitylib.Circuits.OracleInlining.Adaptive.Internal

Fixed-round adaptive oracle circuit programs -- proof internals #

source
theorem Complexity.AdaptiveOracleProgram.inlineHistory_eval_internal {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

Internal correctness of every compiled history prefix.

source
theorem Complexity.AdaptiveOracleProgram.inlineHistory_size_internal {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

Internal exact size of every compiled history prefix.

source
theorem Complexity.AdaptiveOracleProgram.inline_eval_internal {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

Internal semantic correctness of the fully inlined circuit.

source
theorem Complexity.AdaptiveOracleProgram.inline_size_internal {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

Internal exact size of the fully inlined circuit.