Hard Relations

This file defines a typeclass HardRelation X W r for relations r : X → W → Prop that are "hard" in the sense that given x : X no polynomial adversary can find w : W such that r x w holds.

In the actual implementation all of these are indexed by some security parameter.

Implementation notes

This is a simplified version without the asymptotic security parameter framework. A full asymptotic version needs OracleAlg to be redesigned.

structure GenerableRelation (X W : Type) (r : X → W → Bool) : Type

A relation r is generable if there is an efficient algorithm gen that produces instance-witness pairs satisfying the relation.

• gen : ProbComp (X × W)

  An efficient algorithm producing instance-witness pairs.

• gen_sound (x : X) (w : W) : (x, w) ∈ support self.gen → r x w = true

  Every pair in the support of gen satisfies the relation r.

def hardRelationExp {X W : Type} {r : X → W → Bool} (hr : GenerableRelation X W r) (adversary : X → ProbComp W) : ProbComp Bool

Experiment for checking whether an adversary can find a witness for a generated instance.