structure Hash : Type

ハッシュ値を表す型

AMATELUSプロトコルでは、SHA3-512を使用するため、 実装では64バイト（512ビット）の固定長配列となる。

• value : List UInt8

instance instReprHash : Repr Hash

Equations

• instReprHash = { reprPrec := reprHash✝ }

instance instDecidableEqHash : DecidableEq Hash

Equations

• instDecidableEqHash = decEqHash✝

structure PublicKey : Type

公開鍵を表す型

AMATELUSプロトコル Version 0では、Ed25519を使用するため、 実装では32バイト固定長となる。

• bytes : List UInt8

instance instReprPublicKey : Repr PublicKey

Equations

• instReprPublicKey = { reprPrec := reprPublicKey✝ }

instance instDecidableEqPublicKey : DecidableEq PublicKey

Equations

• instDecidableEqPublicKey = decEqPublicKey✝

structure SecretKey : Type

秘密鍵を表す型

AMATELUSプロトコル Version 0では、Ed25519を使用するため、 実装では32バイト固定長となる。

• bytes : List UInt8

instance instReprSecretKey : Repr SecretKey

Equations

• instReprSecretKey = { reprPrec := reprSecretKey✝ }

instance instDecidableEqSecretKey : DecidableEq SecretKey

Equations

• instDecidableEqSecretKey = decEqSecretKey✝

structure Signature : Type

デジタル署名を表す型

AMATELUSプロトコル Version 0では、Ed25519を使用するため、 実装では64バイト固定長となる。

• bytes : List UInt8

instance instReprSignature : Repr Signature

Equations

• instReprSignature = { reprPrec := reprSignature✝ }

instance instDecidableEqSignature : DecidableEq Signature

Equations

• instDecidableEqSignature = decEqSignature✝

structure PublicInput : Type

公開入力を表す型

ZKPの検証者が知っている情報。 例: "age >= 20"という主張における20

• data : List UInt8

structure Witness : Type

秘密入力（witness）を表す型

ZKPの証明者のみが知っている情報。 例: "age >= 20"という主張における実際の年齢25

• data : List UInt8

structure Proof : Type

ZKP証明を表す型

証明データ（π）のバイト列表現。

• bytes : List UInt8

def Relation : Type

関係式を表す型

ZKPで証明される関係式 R(x, w)。 x: 公開入力、w: 秘密入力（witness） 例: R(20, 25) = (25 >= 20) = true

Equations

• Relation = (PublicInput → Witness → Bool)