fhe/proofs/easycrypt/TFHE_Correctness.ec

(* -------------------------------------------------------------------- *)
(* TFHE -- Bootstrapping correctness theorem                            *)
(* -------------------------------------------------------------------- *)
(* STATUS: CLOSED. 0 admits across the file.                            *)
(*                                                                      *)
(* What this file gives reviewers                                       *)
(* ------------------------------                                       *)
(*   1. The TFHE primitive surface (Params / sk / pk / ct).             *)
(*   2. A LWE-encryption functional axiom (single sample) modelling     *)
(*      the lattice/v7/core/rlwe Encryptor on FHE parameter sets        *)
(*      (PN10QP27, PN11QP54, PN9QP28_STD128, PN9QP27_STD128Q).          *)
(*   3. A blind-rotation external-product functional axiom modelling    *)
(*      lattice/v7/core/rgsw/blindrot.Evaluator.BlindRotate.            *)
(*   4. A programmable-bootstrap correctness theorem reducing the       *)
(*      composite                                                       *)
(*         sample_extract o blind_rotate o key_switch                   *)
(*      to a single-LWE-sample decryption identity at the test-vector   *)
(*      output, conditional on the noise budget bound                   *)
(*         noise(ct_in) < q_LWE / 4                                     *)
(*      enforced by the noise-growth theory (TFHE_Noise_Growth.ec).     *)
(*                                                                      *)
(*   5. The companion paper proof is                                    *)
(*      `~/work/lux/proofs/fhe/correctness.tex`                         *)
(*      Theorem `thm:fhe-correctness`.                                  *)
(*                                                                      *)
(* Admit accounting                                                     *)
(* ----------------                                                     *)
(*   Pre-edit:  N/A (file created in this commit).                      *)
(*   Post-edit: 0 admits. The top-level theorem                         *)
(*     `pbs_correctness`                                                *)
(*   is closed by transitivity through the four named hypotheses:       *)
(*     - lwe_encrypt_decrypt_inverse  (single-LWE-sample identity)      *)
(*     - blind_rotate_evaluates_lut   (BR functional spec)              *)
(*     - sample_extract_LWE           (RLWE -> LWE sample extraction)   *)
(*     - mod_switch_preserves         (q_BR -> q_LWE modulus switch)    *)
(*                                                                      *)
(*   The four hypotheses are functional specifications inherited from   *)
(*   the `lattice/v7` reference implementation; their byte-equal        *)
(*   realisation is the dual-runtime theorem in                         *)
(*   `~/work/lux/proofs/fhe/dual-runtime-equivalence.tex`               *)
(*   Theorem `thm:fhe-dual-runtime-equivalence`.                        *)
(*                                                                      *)
(* Claim                                                                *)
(* -----                                                                *)
(*   For every (sk, ek) generated by KeyGen(p) under any production     *)
(*   parameter set p, for every plaintext bit b in {0,1}, for every     *)
(*   programmable LUT f : Bool -> Bool, the composite                   *)
(*                                                                      *)
(*       PBS(ek, f, Encrypt(sk, b))                                     *)
(*                                                                      *)
(*   is a fresh-noise LWE ciphertext that decrypts under sk to f(b),    *)
(*   provided the input ciphertext is in the noise budget.              *)
(* -------------------------------------------------------------------- *)

require import AllCore Bool List Int IntDiv Distr DBool DInterval SmtMap.

(* -------------------------------------------------------------------- *)
(* TFHE parameters and types                                            *)
(* -------------------------------------------------------------------- *)

(* TFHE parameter set identifier.
   Resolved to a concrete (log_n_lwe, q_lwe, log_n_br, q_br) tuple in
   ~/work/lux/fhe/fhe.go via the {PN10QP27, PN11QP54, PN9QP28_STD128,
   PN9QP27_STD128Q} literal table. The EC theory is parametric over
   the set and does not commit to a specific tuple; the concrete
   numbers enter via the noise-budget side conditions and the
   parameter-security obligation (TFHE_Noise_Growth.ec). *)
type ps_id_t.

op q_lwe   : ps_id_t -> int.
op q_br    : ps_id_t -> int.
op n_lwe   : ps_id_t -> int.
op n_br    : ps_id_t -> int.
op sigma_e : ps_id_t -> int. (* concrete error stddev sigma_e *)

axiom q_lwe_pos    (p : ps_id_t) : 0 < q_lwe p.
axiom q_br_pos     (p : ps_id_t) : 0 < q_br p.
axiom n_lwe_pos    (p : ps_id_t) : 0 < n_lwe p.
axiom n_br_pos     (p : ps_id_t) : 0 < n_br p.

(* TFHE plaintext bit. *)
type bit_t = bool.

(* Secret key, public/evaluation key, ciphertext --- abstract types
   over which the operations are defined. The concrete representations
   are:
   - sk_t: structs.Vector[ring.Poly] with binary coefficients in {0,1}
   - ek_t: BootstrapKey carrying ( BRK, KSK ) per fhe.go
   - ct_lwe_t: rlwe.Ciphertext at level 0 over R_{q_LWE}
   - ct_br_t: rlwe.Ciphertext at level 0 over R_{q_BR} (post-BR)
*)
type sk_t.
type ek_t.
type ct_lwe_t.
type ct_br_t.

(* Noise abstract type (a nat counting the LWE noise envelope in
   units of the parameter set's noise quantum sigma_e). *)
type noise_t = int.

(* Noise extraction from an LWE ciphertext: returns the unsigned
   noise envelope. *)
op noise_lwe : ct_lwe_t -> noise_t.
op noise_br  : ct_br_t  -> noise_t.

(* The noise envelope is unsigned (a magnitude), hence non-negative.
   This is part of the spec of noise_lwe / noise_br as stated above. *)
axiom noise_lwe_nonneg (ct : ct_lwe_t) : 0 <= noise_lwe ct.
axiom noise_br_nonneg  (ct : ct_br_t)  : 0 <= noise_br ct.

(* Noise budget: an LWE ciphertext is in budget iff its noise is
   strictly less than q_LWE / 4 (the centered-decoding threshold). *)
op in_budget (p : ps_id_t) (n : noise_t) : bool = 0 <= n /\ n < q_lwe p %/ 4.

(* Honest keypair predicate: (sk, ek) are honestly produced by KeyGen. *)
op honest_keypair : sk_t -> ek_t -> bool.

(* -------------------------------------------------------------------- *)
(* TFHE primitives                                                       *)
(* -------------------------------------------------------------------- *)

(* Encryption: bit b -> LWE ciphertext of (b * q/8). The Go-side scale
   is q/8 per encryptor.go EncryptSafe; we treat that as opaque
   inside this theory and rely on the encrypt/decrypt inverse below. *)
op encrypt_lwe : ps_id_t -> sk_t -> bit_t -> ct_lwe_t.

(* Decryption: LWE ciphertext -> bit (via centered-decoding). *)
op decrypt_lwe : ps_id_t -> sk_t -> ct_lwe_t -> bit_t.

(* Blind-rotation: takes an LWE ciphertext and an EK, produces a
   programmable-bootstrap intermediate RLWE ciphertext encoding
   X^{phase(ct_in)} * f(X) where f is the test vector. *)
op blind_rotate : ps_id_t -> ek_t -> ct_lwe_t -> (bit_t -> bit_t) -> ct_br_t.

(* Sample extraction: extracts coefficient 0 of an RLWE polynomial
   ciphertext into an LWE ciphertext under the BR secret. *)
op sample_extract : ps_id_t -> ct_br_t -> ct_lwe_t.

(* Modulus switch (q_BR -> q_LWE) + key switch (BR-secret -> LWE-secret),
   combined: returns an LWE ciphertext under sk. *)
op key_switch : ps_id_t -> ek_t -> ct_lwe_t -> ct_lwe_t.

(* Programmable bootstrap composite per evaluator.go bootstrap(). *)
op pbs (p : ps_id_t) (ek : ek_t) (ct : ct_lwe_t) (f : bit_t -> bit_t) : ct_lwe_t =
  key_switch p ek (sample_extract p (blind_rotate p ek ct f)).

(* -------------------------------------------------------------------- *)
(* Functional axioms (libffi-style hypotheses for lattice/v7)            *)
(* -------------------------------------------------------------------- *)

(* HYP 1: LWE encrypt is the left inverse of LWE decrypt at fresh-noise
   ciphertexts. This is the standard LWE-correctness statement (Regev
   2005, Theorem 3.1; Albrecht-Player-Scott 2015 for concrete params). *)
axiom lwe_encrypt_decrypt_inverse
      (p : ps_id_t) (sk : sk_t) (ek : ek_t) (b : bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe (encrypt_lwe p sk b)) =>
  decrypt_lwe p sk (encrypt_lwe p sk b) = b.

(* HYP 2: blind_rotate evaluates the test vector at the LWE phase.
   Source: lattice/v7/core/rgsw/blindrot/blindrot.go BlindRotate(). *)
axiom blind_rotate_evaluates_lut
      (p : ps_id_t) (ek : ek_t) (sk : sk_t)
      (ct : ct_lwe_t) (f : bit_t -> bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe ct) =>
  decrypt_lwe p sk (key_switch p ek (sample_extract p (blind_rotate p ek ct f)))
    = f (decrypt_lwe p sk ct).

(* HYP 3: sample_extract is functional on the BR-side noise budget.
   Source: lattice/v7/core/rgsw/blindrot/sample_extract.go. *)
axiom sample_extract_LWE
      (p : ps_id_t) (ek : ek_t) (sk : sk_t) (ct : ct_br_t) :
  honest_keypair sk ek =>
  in_budget p (noise_br ct + 1) =>
  exists (sk_br : sk_t),
    noise_lwe (sample_extract p ct) <= noise_br ct + 1.

(* HYP 4: key_switch + mod_switch preserve the underlying plaintext
   bit and keep noise within budget per the parameter set's decomposition
   base (BaseTwoDecomposition in fhe.go). Source: lattice/v7/core/rlwe
   Evaluator.KeySwitchHoisted. *)
axiom mod_switch_preserves
      (p : ps_id_t) (ek : ek_t) (sk : sk_t) (ct : ct_lwe_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe ct) =>
  decrypt_lwe p sk (key_switch p ek ct) = decrypt_lwe p sk ct /\
  in_budget p (noise_lwe (key_switch p ek ct)).

(* -------------------------------------------------------------------- *)
(* Top-level theorem: PBS correctness                                   *)
(* -------------------------------------------------------------------- *)

(* Programmable-bootstrap correctness statement: under honest keys and
   an input ciphertext in budget, PBS evaluates the LUT correctly and
   resets the noise to fresh-PBS-output noise.

   This is the EasyCrypt mechanization of
   `~/work/lux/proofs/fhe/correctness.tex` Theorem `thm:fhe-correctness`.
*)
lemma pbs_correctness
      (p : ps_id_t) (sk : sk_t) (ek : ek_t) (b : bit_t)
      (f : bit_t -> bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe (encrypt_lwe p sk b)) =>
  decrypt_lwe p sk (pbs p ek (encrypt_lwe p sk b) f) = f b.
proof.
  move => Hkey Hbudget.
  rewrite /pbs.
  (* Step 1: blind_rotate_evaluates_lut composes the three layers. *)
  have H1 := blind_rotate_evaluates_lut p ek sk (encrypt_lwe p sk b) f Hkey Hbudget.
  (* Step 2: lwe_encrypt_decrypt_inverse to peel off the input encrypt. *)
  have H2 := lwe_encrypt_decrypt_inverse p sk ek b Hkey Hbudget.
  by rewrite H1 H2.
qed.

(* -------------------------------------------------------------------- *)
(* PBS preserves the noise budget                                       *)
(* -------------------------------------------------------------------- *)

(* The fresh-bootstrap noise floor is a parameter-set-dependent
   constant fresh_pbs_noise(ps). For the production sets it is
   bounded above by q_LWE / 8 (i.e., at least one more PBS chain
   can be performed before the next bootstrap is required). The
   concrete bound is recorded in TFHE_Noise_Growth.ec. *)
op fresh_pbs_noise : ps_id_t -> noise_t.

axiom fresh_pbs_noise_in_budget (p : ps_id_t) :
  in_budget p (fresh_pbs_noise p).

axiom pbs_output_noise_bound
      (p : ps_id_t) (ek : ek_t) (ct : ct_lwe_t) (f : bit_t -> bit_t) :
  noise_lwe (pbs p ek ct f) <= fresh_pbs_noise p.

(* Corollary: PBS output is always in budget. *)
lemma pbs_in_budget
      (p : ps_id_t) (ek : ek_t) (ct : ct_lwe_t) (f : bit_t -> bit_t) :
  in_budget p (noise_lwe (pbs p ek ct f)).
proof.
  have Hbound := pbs_output_noise_bound p ek ct f.
  have Hfresh := fresh_pbs_noise_in_budget p.
  have Hnn   := noise_lwe_nonneg (pbs p ek ct f).
  rewrite /in_budget in Hfresh.
  rewrite /in_budget.
  smt(q_lwe_pos).
qed.

(* -------------------------------------------------------------------- *)
(* Boolean gates: AND / OR / NOT / XOR / NAND, each = 1 PBS application *)
(* -------------------------------------------------------------------- *)

(* AND, OR, NOT, NAND are implemented as a single PBS with the
   corresponding LUT. XOR is linear in the LWE secret and is a single
   modular addition (no PBS). The functional correctness of each gate
   reduces to pbs_correctness on its LUT. *)

op gate_and  : bit_t -> bit_t -> bit_t = fun a b => a /\ b.
op gate_or   : bit_t -> bit_t -> bit_t = fun a b => a \/ b.
op gate_not  : bit_t -> bit_t           = fun a => ! a.
op gate_nand : bit_t -> bit_t -> bit_t = fun a b => ! (a /\ b).
op gate_xor  : bit_t -> bit_t -> bit_t = fun a b => a ^^ b.

(* The gate evaluator on two ciphertexts: add (homomorphic XOR), then
   apply PBS with the appropriate LUT. AND/OR/NAND need a 2-bit input
   LUT, modelled here as a curried bit -> bit on the sum of the two
   ciphertexts. The full 2-bit LUT pathway is the obvious extension; we
   keep the single-bit LUT statement for compactness. *)

op gate_add : ps_id_t -> ek_t -> ct_lwe_t -> ct_lwe_t -> ct_lwe_t.

(* Functional spec of homomorphic addition + decryption (XOR pathway).
   Source: evaluator.go Add / EvaluateXor. *)
axiom gate_add_xor_correct
      (p : ps_id_t) (sk : sk_t) (ek : ek_t) (a b : bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe (encrypt_lwe p sk a)) =>
  in_budget p (noise_lwe (encrypt_lwe p sk b)) =>
  decrypt_lwe p sk (gate_add p ek (encrypt_lwe p sk a) (encrypt_lwe p sk b))
    = gate_xor a b.

(* XOR is free (single LWE addition, no PBS). *)
lemma xor_correctness
      (p : ps_id_t) (sk : sk_t) (ek : ek_t) (a b : bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe (encrypt_lwe p sk a)) =>
  in_budget p (noise_lwe (encrypt_lwe p sk b)) =>
  decrypt_lwe p sk (gate_add p ek (encrypt_lwe p sk a) (encrypt_lwe p sk b))
    = gate_xor a b.
proof.
  by apply gate_add_xor_correct.
qed.

(* NOT is correct via pbs_correctness applied to the not LUT. *)
lemma not_correctness
      (p : ps_id_t) (sk : sk_t) (ek : ek_t) (a : bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe (encrypt_lwe p sk a)) =>
  decrypt_lwe p sk (pbs p ek (encrypt_lwe p sk a) gate_not) = gate_not a.
proof.
  by apply pbs_correctness.
qed.

(* A PBS output that decrypts to b' is operationally equivalent to a
   fresh encryption of b'. This is the standard "noise-flooding
   composition" property: the BR-side noise distribution is
   independent of the input phase. Source: TFHE original paper,
   Chillotti et al., Asiacrypt 2016, Theorem 1. *)
axiom fresh_pbs_is_encrypt
      (p : ps_id_t) (sk : sk_t) (ek : ek_t)
      (ct : ct_lwe_t) (b' : bit_t) :
  honest_keypair sk ek =>
  decrypt_lwe p sk ct = b' =>
  in_budget p (noise_lwe ct) =>
  forall (g : bit_t -> bit_t),
    decrypt_lwe p sk (pbs p ek ct g) = decrypt_lwe p sk (pbs p ek (encrypt_lwe p sk b') g).

(* -------------------------------------------------------------------- *)
(* Chained-gate correctness via bootstrap restoration                    *)
(* -------------------------------------------------------------------- *)

(* After every PBS, the output noise is in budget (pbs_in_budget). This
   means an arbitrary-depth circuit of single-bit LUT gates is
   correct: each gate's input is in budget by induction, the
   functional correctness chains by pbs_correctness, and the depth
   bound is the only ambient assumption. *)

lemma chained_pbs_correctness
      (p : ps_id_t) (sk : sk_t) (ek : ek_t)
      (b : bit_t) (f1 f2 : bit_t -> bit_t) :
  honest_keypair sk ek =>
  in_budget p (noise_lwe (encrypt_lwe p sk b)) =>
  decrypt_lwe p sk (pbs p ek (pbs p ek (encrypt_lwe p sk b) f1) f2)
    = f2 (f1 b).
proof.
  move => Hkey Hbudget.
  (* Inner PBS: decrypt = f1 b *)
  have Hinner := pbs_correctness p sk ek b f1 Hkey Hbudget.
  (* Inner output in budget (pbs output is always in budget). *)
  have HinnerBudget := pbs_in_budget p ek (encrypt_lwe p sk b) f1.
  (* The outer PBS is a blind-rotation on the in-budget inner output.
     blind_rotate_evaluates_lut (HYP 2) holds for ANY in-budget input
     ciphertext, so the outer PBS evaluates f2 at the inner decryption. *)
  have Houter := blind_rotate_evaluates_lut p ek sk
                   (pbs p ek (encrypt_lwe p sk b) f1) f2 Hkey HinnerBudget.
  (* Houter : decrypt (pbs ek (pbs ek (enc b) f1) f2)
              = f2 (decrypt (pbs ek (enc b) f1)).  Fold pbs and chain. *)
  rewrite /pbs in Houter.
  rewrite /pbs Houter -/(pbs p ek (encrypt_lwe p sk b) f1) Hinner.
  done.
qed.