Deterministic environment fragments for kernel replay assurance.
Summary
Functions
Returns deterministic environment cases used by kernel differential assurance.
Builds a transparent definition chain ending in a theorem over the normalized endpoint.
Returns malformed deterministic environments expected to be rejected.
Builds definitions whose values contain lets that normalize to the previous declaration.
Builds a definition chain with theorem declarations at every step.
Builds a small universe-polymorphic identity chain.
Functions
@spec cases(keyword()) :: [Theoria.Kernel.EnvironmentCorpus.Case.t()]
Returns deterministic environment cases used by kernel differential assurance.
@spec definition_chain(pos_integer()) :: Theoria.Kernel.EnvironmentCorpus.Case.t()
Builds a transparent definition chain ending in a theorem over the normalized endpoint.
@spec invalid_cases(keyword()) :: [Theoria.Kernel.EnvironmentCorpus.InvalidCase.t()]
Returns malformed deterministic environments expected to be rejected.
@spec let_chain(pos_integer()) :: Theoria.Kernel.EnvironmentCorpus.Case.t()
Builds definitions whose values contain lets that normalize to the previous declaration.
@spec theorem_chain(pos_integer()) :: Theoria.Kernel.EnvironmentCorpus.Case.t()
Builds a definition chain with theorem declarations at every step.
@spec universe_polymorphic_chain(pos_integer()) :: Theoria.Kernel.EnvironmentCorpus.Case.t()
Builds a small universe-polymorphic identity chain.