SSA.Projects.FullyHomomorphicEncryption.Syntax

source

def mkTy {q : ℕ} {n : ℕ} [Fact (q > 1)] {φ : ℕ} :

MLIR.AST.MLIRType φ → MLIR.AST.ExceptM (FHE q n) (FHE q n).Ty

Equations

mkTy (MLIR.AST.MLIRType.undefined "R") = pure Ty.polynomialLike
mkTy (MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless a) = pure Ty.integer
mkTy MLIR.AST.MLIRType.index = pure Ty.index
mkTy x = throw MLIR.AST.TransformError.unsupportedType

Instances For

source

instance instTransformTy {q : ℕ} {n : ℕ} [Fact (q > 1)] :

MLIR.AST.TransformTy (FHE q n) 0

Equations

instTransformTy = { mkTy := mkTy }

source

def cstInt {q : ℕ} {n : ℕ} [Fact (q > 1)] {Γ : Ctxt (FHE q n).Ty} (z : ℤ) :

Expr (FHE q n) Γ EffectKind.pure Ty.integer

Equations

cstInt z = Expr.mk (Op.const_int z) ⋯ ⋯ HVector.nil HVector.nil

Instances For

source

def cstIdx {q : ℕ} {n : ℕ} [Fact (q > 1)] {Γ : Ctxt (FHE q n).Ty} (i : ℕ) :

Expr (FHE q n) Γ EffectKind.pure Ty.index

Equations

cstIdx i = Expr.mk (Op.const_idx i) ⋯ ⋯ HVector.nil HVector.nil

Instances For

source

def add {q : ℕ} {n : ℕ} [Fact (q > 1)] {Γ : Ctxt (Ty q n)} (e₁ : Γ.Var Ty.polynomialLike) (e₂ : Γ.Var Ty.polynomialLike) :

Expr (FHE q n) Γ EffectKind.pure Ty.polynomialLike

Equations

add e₁ e₂ = Expr.mk Op.add ⋯ ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

Instances For

source

def mul {q : ℕ} {n : ℕ} [Fact (q > 1)] {Γ : Ctxt (Ty q n)} (e₁ : Γ.Var Ty.polynomialLike) (e₂ : Γ.Var Ty.polynomialLike) :

Expr (FHE q n) Γ EffectKind.pure Ty.polynomialLike

Equations

mul e₁ e₂ = Expr.mk Op.mul ⋯ ⋯ (e₁::ₕ(e₂::ₕHVector.nil)) HVector.nil

Instances For

source

def mon {q : ℕ} {n : ℕ} [Fact (q > 1)] {Γ : Ctxt (Ty q n)} (a : Γ.Var Ty.integer) (i : Γ.Var Ty.index) :

Expr (FHE q n) Γ EffectKind.pure Ty.polynomialLike

Equations

mon a i = Expr.mk Op.monomial ⋯ ⋯ (a::ₕ(i::ₕHVector.nil)) HVector.nil

Instances For

source

def ROfZComputable_impl {q : ℕ} {n : ℕ} (z : ℤ) :

R q n

Equations

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

Instances For

source

@[irreducible, implemented_by ROfZComputable_impl]

def ROfZComputable_stuck_term (q : ℕ) (n : ℕ) (z : ℤ) :

R q n

Equations

ROfZComputable_stuck_term q n z = ↑z

Instances For

source

@[simp]

theorem ROfZComputable_def (q : ℕ) (n : ℕ) (z : ℤ) :

ROfZComputable_stuck_term q n z = ↑z

source

def cstComputable {q : ℕ} {n : ℕ} [Fact (q > 1)] {Γ : Ctxt (FHE q n).Ty} (z : ℤ) :

Expr (FHE q n) Γ EffectKind.pure Ty.polynomialLike

Equations

cstComputable z = Expr.mk (Op.const (ROfZComputable_stuck_term q n z)) ⋯ ⋯ HVector.nil HVector.nil

Instances For

source

def mkExpr {q : ℕ} {n : ℕ} [Fact (q > 1)] (Γ : Ctxt (FHE q n).Ty) (opStx : MLIR.AST.Op 0) :

MLIR.AST.ReaderM (FHE q n) ((eff : EffectKind) × (ty : (FHE q n).Ty) × Expr (FHE q n) Γ eff ty)

Equations

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

Instances For

source

instance instTransformExprFHEOfNatNat {q : ℕ} {n : ℕ} [Fact (q > 1)] :

MLIR.AST.TransformExpr (FHE q n) 0

Equations

instTransformExprFHEOfNatNat = { mkExpr := mkExpr }

source

def mkReturn {q : ℕ} {n : ℕ} [Fact (q > 1)] (Γ : Ctxt (FHE q n).Ty) (opStx : MLIR.AST.Op 0) :

MLIR.AST.ReaderM (FHE q n) ((eff : EffectKind) × (ty : (FHE q n).Ty) × Com (FHE q n) Γ eff ty)

Equations

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

Instances For

source

instance instTransformReturnFHEOfNatNat {q : ℕ} {n : ℕ} [Fact (q > 1)] :

MLIR.AST.TransformReturn (FHE q n) 0

Equations

instTransformReturnFHEOfNatNat = { mkReturn := mkReturn }

source

def «term[poly_,_,_|_]» :

Lean.ParserDescr

Equations

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

Instances For