Concrete depth fit for GSW decryption

The complete raw-input decryptor and its two-copy NAND augmentation each compile to at most DepthParameters.depthBudget layers, for every security parameter. This is an arithmetic budget result; it does not assume or establish LWE hardness or circular security.

Main results

• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.layers_le_depthBudget: the actual decryptor's layer count fits the existing GSW parameter family.
• Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.layers_augment_le_depthBudget: the actual augmented circuit's layer count fits the same family.

theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.layers_le_depthBudget (security : ℕ) : (Circuits.Boolean.Layered.compile (inputWidth (Parameters.dimension security) (DepthParameters.width security)) (circuit (Parameters.dimension security) (DepthParameters.width security)).code).1.length ≤ DepthParameters.depthBudget security

Two microlevels per De Morgan level of the complete raw decryptor fit the budget.

theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.depth_augment_le (n w : ℕ) : (augmentNand (circuit n w)).depth ≤ 30 + 18 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 n

The NAND extension adds at most two De Morgan levels to the complete raw decryptor.

theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.layers_augment_le_depthBudget (security : ℕ) : (Circuits.Boolean.Layered.compile (inputWidth (Parameters.dimension security) (DepthParameters.width security) + inputWidth (Parameters.dimension security) (DepthParameters.width security)) (augmentNand (circuit (Parameters.dimension security) (DepthParameters.width security))).code).1.length ≤ DepthParameters.depthBudget security

Two microlevels per De Morgan level, including the actual NAND augmentation, fit the budget.