ReplayAudit.hs

-- @generated by keiro-dsl 0.21.0.0 (language keiro-dsl 4) from context workspace-proof replay-audit assembly; do not edit.
--
-- Deployment contract:
--   * replay-neutral diff: no data audit is required;
--   * affected diff: run AuditTargeted with the emitted affected set
--     against a production copy under the candidate binary;
--   * one-time runtime cutover: run AuditFull;
--   * any non-zero audit exit blocks deployment.
module Proof.WorkspaceProof.Generated.ReplayAudit (auditTargets) where

import Proof.WorkspaceProof.Alpha.Generated.EventStream qualified as Alpha
import Proof.WorkspaceProof.Assignment.Generated.EventStream qualified as Assignment
import Proof.WorkspaceProof.Beta.Generated.EventStream qualified as Beta
import Keiro.ReplayAudit (AuditTarget (..), SomeAuditTarget (..), streamInCategory)
import Keiro.Stream qualified as Stream

auditTargets :: [SomeAuditTarget]
auditTargets =
  [ SomeAuditTarget
      AuditTarget
        { eventStream = Alpha.alphaEventStream
        , category = Stream.categoryText Alpha.alphaCategory
        , mkStream = streamInCategory (Stream.categoryText Alpha.alphaCategory)
        }
  , SomeAuditTarget
      AuditTarget
        { eventStream = Assignment.assignmentEventStream
        , category = Stream.categoryText Assignment.assignmentCategory
        , mkStream = streamInCategory (Stream.categoryText Assignment.assignmentCategory)
        }
  , SomeAuditTarget
      AuditTarget
        { eventStream = Beta.betaEventStream
        , category = Stream.categoryText Beta.betaCategory
        , mkStream = streamInCategory (Stream.categoryText Beta.betaCategory)
        }
  ]