RandomSystems.lean

/-
Copyright (c) 2024-2026 Trail of Bits. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
import RandomSystems.PartialFunction
import RandomSystems.System.DiscreteSystem
import RandomSystems.Converter.Converter
import RandomSystems.Converter.Cascade
import RandomSystems.Converter.Attachment
import RandomSystems.System.ProbabilisticSystem
import RandomSystems.System.Environment
import RandomSystems.System.ClassDistance
import RandomSystems.System.Behaviour
import RandomSystems.System.MultiDistance
import RandomSystems.System.Attainment
import RandomSystems.System.SingleQuery
import RandomSystems.System.BehaviourAttainment
import RandomSystems.System.Example216
import RandomSystems.System.Relabel
import RandomSystems.System.Phi
import RandomSystems.System.ConnectPhi
import RandomSystems.System.Parallel
import RandomSystems.System.Par
import RandomSystems.System.FullyDefined
import RandomSystems.System.Absorb
import RandomSystems.System.FilterPhi
import RandomSystems.System.MetricFullyDefined
import RandomSystems.System.ConnectFullyDefined
import RandomSystems.System.AttachEngineFully
import RandomSystems.System.BlockReplies
import RandomSystems.System.StarFullyDefined
import RandomSystems.System.ParFace
import RandomSystems.System.Connect
import RandomSystems.System.Game
import RandomSystems.System.Winnability
import RandomSystems.Converter.ConverterImpl
import RandomSystems.Converter.Sigma
import RandomSystems.Technique.ConditionalEquivalence
import RandomSystems.Technique.BlindWinning
import RandomSystems.Notation
import RandomSystems.Technique.Completeness
import RandomSystems.Technique.HCoefficient
import RandomSystems.System.RandomObjects
import RandomSystems.Interface.Interface
import RandomSystems.System.ProbabilisticConverter
import RandomSystems.Game.GameRelaxation
import RandomSystems.Converter.CascadeRealization
import RandomSystems.Converter.CombineRealization
import RandomSystems.Converter.CascadeLaw

/-!
# Random systems

Maurer's random-systems layer: the deterministic discrete system, the
converter, and the machinery built on them.  It depends on `Probability` and
not on the abstract-cryptography layer; the instances connecting the two are
given where the objects are defined.

Modules not listed here are placeholders awaiting migration.
-/