Succinct MCSP -- definitions

SuccinctMCSP replaces a complete truth table by a finite list of sampled input/output constraints. The list may repeat an input, so contradictory constraints are represented rather than ruled out by syntax. An instance is accepted exactly when one circuit within its threshold matches every sample.

The codec is total and canonical. Each typed sample is framed separately, the sample count is explicit, and decoding rejects wrong-width inputs, non-singleton outputs, missing samples, trailing samples, noncanonical natural fields, and malformed pairing.

Positive arities use Basis.andOr2. Since the circuit type has no zero-input member, a zero-arity witness is an explicitly chosen constant bit of size zero. Thus contradictory zero-arity samples are rejected while every consistent list is accepted at every natural threshold.

structure Complexity.SuccinctMCSP.Sample (arity : ℕ) : Type

One typed input/output constraint for an arity-input Boolean function.

• input : BitString arity

  Input on which the candidate circuit is constrained.

• output : Bool

  Required output on input.

def Complexity.SuccinctMCSP.Sample.ofFunction {arity : ℕ} (f : BitString arity → Bool) (input : BitString arity) : Sample arity

Package one evaluation of a Boolean function as a sample.

Equations

• Complexity.SuccinctMCSP.Sample.ofFunction f input = { input := input, output := f input }

def Complexity.SuccinctMCSP.Sample.MatchesFunction {arity : ℕ} (sample : Sample arity) (f : BitString arity → Bool) : Prop

A sample is satisfied when the function has its required output.

Equations

• sample.MatchesFunction f = (f sample.input = sample.output)

def Complexity.SuccinctMCSP.Sample.encode {arity : ℕ} (sample : Sample arity) : List Bool

Canonically encode a sample as a framed input and singleton output.

Equations

• sample.encode = Complexity.pair sample.input.toList [sample.output]

def Complexity.SuccinctMCSP.Sample.decode? (arity : ℕ) (bits : List Bool) : Option (Sample arity)

Decode exactly one sample at the supplied arity.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SuccinctMCSP.encodeSamples {arity : ℕ} : List (Sample arity) → List Bool

Canonically encode a list of samples as a right-nested sequence of pairs.

Equations

• Complexity.SuccinctMCSP.encodeSamples [] = []
• Complexity.SuccinctMCSP.encodeSamples (sample :: samples) = Complexity.pair sample.encode (Complexity.SuccinctMCSP.encodeSamples samples)

def Complexity.SuccinctMCSP.decodeSamples? (arity count : ℕ) : List Bool → Option (List (Sample arity))

Decode exactly count right-nested samples and reject all trailing data.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SuccinctMCSP.decodeSamples? arity 0 [] = some []
• Complexity.SuccinctMCSP.decodeSamples? arity 0 (head :: tail) = none

structure Complexity.SuccinctMCSP.Instance : Type

A sampled circuit-minimization instance. Repeated inputs are permitted.

• arity : ℕ

  Number of input bits in every sample.

• samples : List (Sample self.arity)

  Finite list of constraints; repetitions and contradictions are retained.

• threshold : ℕ

  Maximum allowed circuit size.

def Complexity.SuccinctMCSP.Instance.ofInputs {arity : ℕ} (threshold : ℕ) (f : BitString arity → Bool) (inputs : List (BitString arity)) : Instance

Build the sampled constraints induced by a function on a chosen input list.

Equations

• Complexity.SuccinctMCSP.Instance.ofInputs threshold f inputs = { arity := arity, samples := List.map (Complexity.SuccinctMCSP.Sample.ofFunction f) inputs, threshold := threshold }

def Complexity.SuccinctMCSP.Instance.SamplesFunction (inst : Instance) (f : BitString inst.arity → Bool) : Prop

Every sample in the instance is satisfied by the supplied function.

Equations

• inst.SamplesFunction f = ∀ sample ∈ inst.samples, sample.MatchesFunction f

def Complexity.SuccinctMCSP.Instance.encode (inst : Instance) : List Bool

Canonically encode arity, threshold, count, and the framed sample payload.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SuccinctMCSP.Instance.decode? (bits : List Bool) : Option Instance

Decode exactly one canonical sampled instance.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SuccinctMCSP.Instance.HasCircuitAtMost (inst : Instance) : Prop

A direct typed witness formulation of sampled circuit minimization.

At positive arity the witness is a fan-in-two circuit matching every listed constraint. At arity zero the witness is an explicit constant output bit of size zero.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SuccinctMCSP : Set (List Bool)

Total succinct MCSP over canonical sampled-instance codes.

Malformed strings are no-instances.

Equations

• Complexity.SuccinctMCSP = {bits : List Bool | match Complexity.SuccinctMCSP.Instance.decode? bits with | some inst => inst.HasCircuitAtMost | none => False}