Cost accounting for Fiat-Shamir with aborts

Exact per-query-class cost accounting for fsAbortSignLoop and FiatShamirWithAbort.sign/verify. Each lemma characterises the weighted query cost or the number of hash queries made by one signing/verification invocation; the expected-value versions live in FiatShamir.WithAbort.ExpectedCost.

theorem FiatShamirWithAbort.signAttempt_run_formula_withUnitCost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) : WriterT.run (HasQuery.withUnitCost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => fsAbortSignAttempt ids M pk sk msg) runtime) = (fun (attempt : Commit × Option Resp) => (attempt, Multiplicative.ofAdd 1)) <$> HasQuery.inRuntime (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] => fsAbortSignAttempt ids M pk sk msg) runtime

theorem FiatShamirWithAbort.signAttempt_usesCostAsQueryCost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → ω) : HasQuery.UsesCostAs (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => fsAbortSignAttempt ids M pk sk msg) runtime costFn fun (attempt : Commit × Option Resp) => costFn (msg, attempt.1)

A single signing attempt has query cost determined by its output: the returned commitment w' is exactly the random-oracle query point.

theorem FiatShamirWithAbort.signAttempt_expectedQueryCost_eq_outputExpectation {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {ω : Type} [AddMonoid ω] [HasEvalSPMF m] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → ω) (val : ω → ENNReal) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ω m)] => fsAbortSignAttempt ids M pk sk msg) runtime costFn val = ∑' (attempt : Commit × Option Resp), Pr[= attempt | HasQuery.inRuntime (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) m] => fsAbortSignAttempt ids M pk sk msg) runtime] * val (costFn (msg, attempt.1))

The expected weighted query cost of one signing attempt is the expectation of the queried commitment cost over the attempt output distribution.

theorem FiatShamirWithAbort.fsAbortSignLoop_usesWeightedQueryCostAtMost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSet m] {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → κ) (w : κ) (hcost : ∀ (t : M × Commit), costFn t ≤ w) (n : ℕ) : HasQuery.UsesCostAtMost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT κ m)] => fsAbortSignLoop ids M pk sk msg n) runtime costFn (n • w)

The retry loop makes weighted query cost at most n • w when each query costs at most w.

theorem FiatShamirWithAbort.sign_usesWeightedQueryCostAtMost {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSet m] (hr : GenerableRelation Stmt Wit rel) {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → κ) (w : κ) (hcost : ∀ (t : M × Commit), costFn t ≤ w) (maxAttempts : ℕ) : HasQuery.UsesCostAtMost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT κ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime costFn (maxAttempts • w)

Signing makes weighted query cost at most maxAttempts • w when each query costs at most w.

theorem FiatShamirWithAbort.sign_usesAtMostMaxAttemptsQueries {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSet m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.UsesAtMostQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime maxAttempts

Unit-cost specialization: signing makes at most maxAttempts random-oracle queries.

theorem FiatShamirWithAbort.sign_expectedQueries_eq_sum_reachedAttemptProbabilities {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSPMF m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime = ∑ i ∈ Finset.range maxAttempts, probEvent (HasQuery.queryCountDist (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime) fun (q : ℕ) => i < q

Tail-sum formula for the expected number of signing queries in Fiat-Shamir with aborts.

The random variable on the right is the unit-cost query count of the signer. The event i < q means that the signer performed at least i + 1 random-oracle queries, equivalently that the (i + 1)-st signing attempt was reached. Since the signer performs at most maxAttempts iterations, the infinite tail sum truncates to Finset.range maxAttempts.

theorem FiatShamirWithAbort.sign_expectedQueryCost_le {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSPMF m] (hr : GenerableRelation Stmt Wit rel) {κ : Type} [AddCommMonoid κ] [PartialOrder κ] [IsOrderedAddMonoid κ] [CanonicallyOrderedAdd κ] (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (costFn : M × Commit → κ) (w : κ) (val : κ → ENNReal) (hcost : ∀ (t : M × Commit), costFn t ≤ w) (hval : Monotone val) (maxAttempts : ℕ) : HasQuery.expectedQueryCost (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT κ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime costFn val ≤ val (maxAttempts • w)

Expected weighted query cost of signing is bounded by the worst-case maxAttempts • w budget whenever every query costs at most w.

theorem FiatShamirWithAbort.sign_expectedQueries_le {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (ids : IdenSchemeWithAbort Stmt Wit Commit PrvState Chal Resp rel) (M : Type) {m : Type → Type u} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] [HasEvalSPMF m] (hr : GenerableRelation Stmt Wit rel) (runtime : QueryRuntime (OracleSpec.ofFn fun (x : M × Commit) => Chal) m) (pk : Stmt) (sk : Wit) (msg : M) (maxAttempts : ℕ) : HasQuery.expectedQueries (fun [HasQuery (OracleSpec.ofFn fun (x : M × Commit) => Chal) (AddWriterT ℕ m)] => (FiatShamirWithAbort ids hr M maxAttempts).sign pk sk msg) runtime ≤ ↑maxAttempts

Unit-cost specialization: the expected number of signing queries is at most maxAttempts.