Executable binary field blocks

A bounded scan splits an explicitly supplied number of fixed-width blocks. Short inputs produce short or empty final blocks and long suffixes are ignored; the program is total on all inputs. Canonical-width inputs split and flatten exactly. Combined conversion interprets the flat CL vector in the constructed self-dual basis and returns the field arithmetic's canonical Shoup rows.

def MIPRE.Introspection.BinaryBlock.splitBlocks : ℕ → ℕ → Cost.BitStr → List Cost.BitStr

Equations

• MIPRE.Introspection.BinaryBlock.splitBlocks 0 x✝¹ x✝ = []
• MIPRE.Introspection.BinaryBlock.splitBlocks n.succ x✝¹ x✝ = List.take x✝¹ x✝ :: MIPRE.Introspection.BinaryBlock.splitBlocks n x✝¹ (List.drop x✝¹ x✝)

theorem MIPRE.Introspection.BinaryBlock.splitBlocks_length (n k : ℕ) (v : Cost.BitStr) : (splitBlocks n k v).length = n

noncomputable def MIPRE.Introspection.BinaryBlock.splitStep : Cost.PolyTimeFun ((Cost.BitStr × List Cost.BitStr) × Cost.Unary) (Cost.BitStr × List Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.BinaryBlock.splitStep_apply (v : Cost.BitStr) (vs : List Cost.BitStr) (k : Cost.Unary) : splitStep.toFun ((v, vs), k) = (List.drop (List.length k) v, List.take (List.length k) v :: vs)

theorem MIPRE.Introspection.BinaryBlock.splitStep_fold (n : ℕ) (k : Cost.Unary) (v : Cost.BitStr) (vs : List Cost.BitStr) : (List.foldl splitStep.step (v, vs) (List.replicate n k)).2 = (splitBlocks n (List.length k) v).reverse ++ vs

noncomputable def MIPRE.Introspection.BinaryBlock.splitBlocksProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) (List Cost.BitStr)

Inputs are number of blocks, block width, and flat bits, in that order.

Equations

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

theorem MIPRE.Introspection.BinaryBlock.splitBlocksProg_apply (n k : Cost.Unary) (v : Cost.BitStr) : splitBlocksProg.toFun (n, k, v) = splitBlocks (List.length n) (List.length k) v

noncomputable def MIPRE.Introspection.BinaryBlock.flattenProg : Cost.PolyTimeFun (List Cost.BitStr) Cost.BitStr

Concatenation is an actual ambient program with a polynomial bound.

Equations

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

theorem MIPRE.Introspection.BinaryBlock.flattenProg_apply (vs : List Cost.BitStr) : flattenProg.toFun vs = vs.flatten

theorem MIPRE.Introspection.BinaryBlock.splitBlocks_flatten (k : ℕ) (vs : List Cost.BitStr) (hv : ∀ v ∈ vs, List.length v = k) : splitBlocks vs.length k vs.flatten = vs

noncomputable def MIPRE.Introspection.BinaryBlock.decodeBlocksProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) (List Cost.BitStr)

Read a flat self-dual vector as canonical Shoup field rows.

Equations

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

noncomputable def MIPRE.Introspection.BinaryBlock.encodeBlocksProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) Cost.BitStr

Write canonical Shoup rows as the flat self-dual CL vector.

Equations

• MIPRE.Introspection.BinaryBlock.encodeBlocksProg = MIPRE.Introspection.BinaryBlock.flattenProg.comp MIPRE.Introspection.BasisProgram.toSelfDualRowsProg

theorem MIPRE.Introspection.BinaryBlock.decodeBlocksProg_apply (n k : Cost.Unary) (v : Cost.BitStr) : decodeBlocksProg.toFun (n, k, v) = BasisProgram.fromSelfDualRowsProg.toFun (k, splitBlocks (List.length n) (List.length k) v)

theorem MIPRE.Introspection.BinaryBlock.encodeBlocksProg_apply (k : Cost.Unary) (vs : List Cost.BitStr) : encodeBlocksProg.toFun (k, vs) = (BasisProgram.toSelfDualRowsProg.toFun (k, vs)).flatten

theorem MIPRE.Introspection.BinaryBlock.encodeBlocksProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {n : ℕ} (u : Fin n → (SAT.shoupBinField k hk).carrier) : encodeBlocksProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits u) = (List.ofFn fun (i : Fin n) => LowDegree.BinaryLinear.vectorBits ((SAT.shoupSelfDualNormalBasis k hk hodd).equivFun (u i))).flatten

theorem MIPRE.Introspection.BinaryBlock.decodeBlocksProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {n : ℕ} (u : Fin n → (SAT.shoupBinField k hk).carrier) : decodeBlocksProg.toFun (Cost.unary n, Cost.unary k, (List.ofFn fun (i : Fin n) => LowDegree.BinaryLinear.vectorBits ((SAT.shoupSelfDualNormalBasis k hk hodd).equivFun (u i))).flatten) = (SAT.shoupBinField k hk).vecBits u