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.

Non-asymptotic version

Simplified version without the asymptotic security parameter framework. The full asymptotic version (below, commented) 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)
• gen_sound (x : X) (w : W) : (x, w) ∈ support self.gen → r x w = true

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.