// Copyright 2026 John Wilger

#[cfg(test)]
mod tests {
    use std::error::Error;

    use crate::core::digest::{
        WorkflowArtifactDigestInput, artifact_digest, slice_artifact_digest,
    };
    use crate::core::effect::FileContents;
    use crate::core::emit::quint::{emit_slice_module, emit_workflow_module};
    use crate::core::types::{
        CommandErrorName, CommandName, ModelDescription, ModelName, OutcomeLabelName,
        PayloadContractName, SliceKindName, TransitionTriggerName, WorkflowCommandErrorRecord,
        WorkflowCommandErrorRecords, WorkflowEntryLifecycleEvidenceText,
        WorkflowEntryLifecycleStateName, WorkflowEntryLifecycleStateRecord,
        WorkflowEntryLifecycleStateRecords, WorkflowModuleData, WorkflowOutcomeRecord,
        WorkflowOutcomeRecords, WorkflowOwnedDefinitionKind, WorkflowOwnedDefinitionName,
        WorkflowOwnedDefinitionRecord, WorkflowOwnedDefinitionRecords, WorkflowSliceDetail,
        WorkflowSliceDetails, WorkflowSlug, WorkflowStepRelationshipName,
        WorkflowTransitionEndpoint, WorkflowTransitionEvidenceRecords, WorkflowTransitionKind,
        WorkflowTransitionRecord, WorkflowTransitionRecords,
    };
    use crate::io::dto::{
        parse_model_description, parse_model_name, parse_quint_module_name, parse_slice_slug,
        parse_workflow_slug,
    };

    struct WorkflowFixtureData {
        name: ModelName,
        description: ModelDescription,
        slug: WorkflowSlug,
        slice_details: Vec<WorkflowSliceDetail>,
        transitions: Vec<WorkflowTransitionRecord>,
        outcomes: WorkflowOutcomeRecords,
        command_errors: WorkflowCommandErrorRecords,
        owned_definitions: WorkflowOwnedDefinitionRecords,
        entry_lifecycle_states: WorkflowEntryLifecycleStateRecords,
    }

    fn build_workflow_fixture_data() -> Result<WorkflowFixtureData, Box<dyn Error>> {
        let workflow_name = parse_model_name("Open ticket")?;
        let workflow_description = parse_model_description("Actor opens a repair ticket.")?;
        let workflow_slug = parse_workflow_slug("open-ticket")?;
        let workflow_slice_details = vec![
            WorkflowSliceDetail::new_with_relationship(
                parse_slice_slug("capture-ticket")?,
                parse_model_name("Capture ticket")?,
                SliceKindName::try_new("state_view")?,
                parse_model_description("Actor enters repair ticket details.")?,
                WorkflowStepRelationshipName::Entry,
            ),
            WorkflowSliceDetail::new_with_relationship(
                parse_slice_slug("review-ticket")?,
                parse_model_name("Review ticket")?,
                SliceKindName::try_new("state_view")?,
                parse_model_description("Actor reviews repair ticket details.")?,
                WorkflowStepRelationshipName::Main,
            ),
        ];
        let workflow_transitions = vec![WorkflowTransitionRecord::new_with_payload_contract(
            WorkflowTransitionEndpoint::try_new("capture-ticket".to_owned())?,
            WorkflowTransitionEndpoint::try_new("review-ticket".to_owned())?,
            WorkflowTransitionKind::try_new("external_trigger")?,
            TransitionTriggerName::try_new("callback_received".to_owned())?,
            PayloadContractName::try_new("CallbackReceivedPayload".to_owned())?,
        )];
        let workflow_outcomes = WorkflowOutcomeRecords::from_records([WorkflowOutcomeRecord::new(
            WorkflowTransitionEndpoint::try_new("capture-ticket".to_owned())?,
            OutcomeLabelName::try_new("ticket_captured".to_owned())?,
            true,
        )]);
        let workflow_command_errors =
            WorkflowCommandErrorRecords::from_records([WorkflowCommandErrorRecord::new(
                WorkflowTransitionEndpoint::try_new("capture-ticket".to_owned())?,
                CommandName::try_new("CaptureTicket".to_owned())?,
                CommandErrorName::try_new("DuplicateTicket".to_owned())?,
            )]);
        let workflow_owned_definitions =
            WorkflowOwnedDefinitionRecords::from_records([WorkflowOwnedDefinitionRecord::new(
                WorkflowTransitionEndpoint::try_new("capture-ticket".to_owned())?,
                WorkflowOwnedDefinitionKind::try_new("external_payload")?,
                WorkflowOwnedDefinitionName::try_new("CallbackReceivedPayload".to_owned())?,
            )]);
        let workflow_entry_lifecycle_states = WorkflowEntryLifecycleStateRecords::from_records([
            WorkflowEntryLifecycleStateRecord::new(
                WorkflowEntryLifecycleStateName::FreshUninitialized,
                WorkflowTransitionEndpoint::try_new("capture-ticket".to_owned())?,
                WorkflowEntryLifecycleEvidenceText::try_new(
                    "capture-ticket view distinguishes first arrival before initialization"
                        .to_owned(),
                )?,
            ),
        ]);
        Ok(WorkflowFixtureData {
            name: workflow_name,
            description: workflow_description,
            slug: workflow_slug,
            slice_details: workflow_slice_details,
            transitions: workflow_transitions,
            outcomes: workflow_outcomes,
            command_errors: workflow_command_errors,
            owned_definitions: workflow_owned_definitions,
            entry_lifecycle_states: workflow_entry_lifecycle_states,
        })
    }

    fn build_workflow_fixture_module() -> Result<FileContents, Box<dyn Error>> {
        let WorkflowFixtureData {
            name: workflow_name,
            description: workflow_description,
            slug: workflow_slug,
            slice_details: workflow_slice_details,
            transitions: workflow_transitions,
            outcomes: workflow_outcomes,
            command_errors: workflow_command_errors,
            owned_definitions: workflow_owned_definitions,
            entry_lifecycle_states: workflow_entry_lifecycle_states,
        } = build_workflow_fixture_data()?;
        let module = emit_workflow_module(
            &parse_quint_module_name("OpenTicket")?,
            &WorkflowModuleData::new(
                workflow_name.clone(),
                workflow_description.clone(),
                workflow_slug.clone(),
                artifact_digest(&WorkflowArtifactDigestInput {
                    workflow_name,
                    workflow_slug,
                    workflow_description,
                    workflow_slice_details: WorkflowSliceDetails::from_details(
                        workflow_slice_details.clone(),
                    ),
                    workflow_transitions: WorkflowTransitionRecords::from_records(
                        workflow_transitions.clone(),
                    ),
                    workflow_outcomes: workflow_outcomes.clone(),
                    workflow_command_errors: workflow_command_errors.clone(),
                    workflow_owned_definitions: workflow_owned_definitions.clone(),
                    workflow_transition_evidences: WorkflowTransitionEvidenceRecords::default(),
                    workflow_requires_entry_lifecycle_coverage: false,
                    workflow_entry_lifecycle_states: workflow_entry_lifecycle_states.clone(),
                }),
            )
            .with_slice_details(WorkflowSliceDetails::from_details(workflow_slice_details))
            .with_transitions(WorkflowTransitionRecords::from_records(
                workflow_transitions,
            ))
            .with_outcomes(workflow_outcomes)
            .with_command_errors(workflow_command_errors)
            .with_owned_definitions(workflow_owned_definitions)
            .with_entry_lifecycle_states(workflow_entry_lifecycle_states),
        );
        Ok(module)
    }

    #[test]
    fn quint_workflow_module_represents_business_workflow_fields() -> Result<(), Box<dyn Error>> {
        let module = build_workflow_fixture_module()?;
        let quint = module.as_ref();

        assert_workflow_header_and_digest(quint);
        assert_workflow_scalar_values(quint);
        assert_workflow_type_declarations(quint);
        assert_workflow_value_declarations(quint);
        assert_workflow_identity_and_structure(quint);
        assert_workflow_step_relationship_invariants(quint);
        assert_workflow_reachability_invariants(quint);
        assert_workflow_lifecycle_invariants(quint);
        assert_workflow_transition_resolution_invariants(quint);
        assert_workflow_outcome_and_error_invariants(quint);
        assert_workflow_owned_definition_invariants(quint);
        assert_workflow_command_transition_invariants(quint);
        assert_workflow_event_transition_invariants(quint);
        assert_workflow_navigation_invariants(quint);
        assert_workflow_external_trigger_invariants(quint);
        assert_workflow_model_state(quint);

        Ok(())
    }

    fn assert_workflow_header_and_digest(quint: &str) {
        assert!(quint.contains("module OpenTicket"));
        assert!(
            quint.contains(
                "// EMC-DIGEST: workflow:name=Open ticket;slug=open-ticket;description=Actor opens a repair ticket.;slices=capture-ticket|Capture ticket|state_view|Actor enters repair ticket details.|entry,review-ticket|Review ticket|state_view|Actor reviews repair ticket details.|main;transitions=capture-ticket->review-ticket:external_trigger:callback_received::CallbackReceivedPayload"
            )
        );
    }

    fn assert_workflow_scalar_values(quint: &str) {
        assert!(quint.contains("val workflowName = \"Open ticket\""));
        assert!(quint.contains("val workflowSlug = \"open-ticket\""));
        assert!(quint.contains("val workflowDescription = \"Actor opens a repair ticket.\""));
    }

    fn assert_workflow_type_declarations(quint: &str) {
        assert!(quint.contains(
            "type WorkflowSliceDetail = { slug: str, name: str, kind: SliceKindName, description: str }"
        ));
        assert!(quint.contains(
            "type WorkflowTransitionKind = Command | Event | Navigation | ExternalTrigger | Outcome | WorkflowExitCommand | WorkflowExitEvent | WorkflowExitNavigation | WorkflowExitExternalTrigger | WorkflowExitOutcome"
        ));
        assert!(quint.contains(
            "type WorkflowOwnedDefinitionKind = OwnedCommand | OwnedEvent | OwnedView | OwnedControl | OwnedReadModel | OwnedOutcome | OwnedError | OwnedAutomation | OwnedTranslation | OwnedExternalPayload"
        ));
        assert!(quint.contains(
            "type WorkflowTransition = { source: str, target: str, kind: WorkflowTransitionKind, trigger: str, sourceControl: str, targetView: str, rationale: str, payloadContract: str }"
        ));
        assert!(quint.contains(
            "type WorkflowOutcome = { sourceSlice: str, label: str, externallyRelevant: bool }"
        ));
        assert!(quint.contains(
            "type WorkflowCommandError = { sourceSlice: str, commandName: str, errorName: str }"
        ));
        assert!(quint.contains(
            "type WorkflowOwnedDefinition = { sourceSlice: str, definitionKind: WorkflowOwnedDefinitionKind, definitionName: str, definitionStream: str, sourceProvenance: str, eventParticipation: str, viewRole: str }"
        ));
        assert!(quint.contains(
            "type WorkflowEntryLifecycleStateName = FreshUninitialized | InitializedUnauthenticated | InitializedAuthenticated | PartiallyConfigured | FullyConfigured"
        ));
        assert!(quint.contains(
            "type WorkflowEntryLifecycleState = { state: WorkflowEntryLifecycleStateName, step: str, evidence: str }"
        ));
        assert!(quint.contains("type WorkflowSlice = { slug: str }"));
    }

    fn assert_workflow_value_declarations(quint: &str) {
        assert!(
            quint
                .contains("val workflowSlices: List[WorkflowSlice] = [{ slug: \"capture-ticket\" },{ slug: \"review-ticket\" }]")
        );
        assert!(
            quint.contains(
                "val workflowSliceSlugs: List[str] = workflowSlices.foldl([], (slugs, workflowSlice) => slugs.append(workflowSlice.slug))"
            )
        );
        assert!(
            quint.contains(
                "val workflowSliceDetails: List[WorkflowSliceDetail] = [{ slug: \"capture-ticket\", name: \"Capture ticket\", kind: SliceStateView, description: \"Actor enters repair ticket details.\" },{ slug: \"review-ticket\", name: \"Review ticket\", kind: SliceStateView, description: \"Actor reviews repair ticket details.\" }]"
            )
        );
        assert!(
            quint.contains(
                "val workflowTransitions: List[WorkflowTransition] = [{ source: \"capture-ticket\", target: \"review-ticket\", kind: ExternalTrigger, trigger: \"callback_received\", sourceControl: \"\", targetView: \"\", rationale: \"\", payloadContract: \"CallbackReceivedPayload\" }]"
            )
        );
        assert!(quint.contains(
            "val workflowOutcomes: List[WorkflowOutcome] = [{ sourceSlice: \"capture-ticket\", label: \"ticket_captured\", externallyRelevant: true }]"
        ));
        assert!(quint.contains(
            "val workflowCommandErrors: List[WorkflowCommandError] = [{ sourceSlice: \"capture-ticket\", commandName: \"CaptureTicket\", errorName: \"DuplicateTicket\" }]"
        ));
        assert!(quint.contains("val workflowOwnedDefinitions: List[WorkflowOwnedDefinition] = [{ sourceSlice: \"capture-ticket\", definitionKind: OwnedExternalPayload, definitionName: \"CallbackReceivedPayload\", definitionStream: \"\", sourceProvenance: \"\", eventParticipation: \"\", viewRole: \"\" }]"));
        assert!(quint.contains("val workflowRequiresEntryLifecycleCoverage = false"));
        assert!(
            quint.contains(
                "val workflowEntryLifecycleStates: List[WorkflowEntryLifecycleState] = [{ state: FreshUninitialized, step: \"capture-ticket\", evidence: \"capture-ticket view distinguishes first arrival before initialization\" }]"
            )
        );
    }

    fn assert_workflow_identity_and_structure(quint: &str) {
        assert!(quint.contains("val workflowIdentityStable"));
        assert!(quint.contains("val workflowSlicesHaveDetails ="));
        assert!(quint.contains("val workflowSliceDetailsComplete = workflowSlicesHaveDetails"));
        assert!(quint.contains(
            "val workflowTransitionsStructured = workflowTransitions.select(transition => transition.source != \"\" and transition.target != \"\" and transition.trigger != \"\").length() == workflowTransitions.length()"
        ));
        assert!(
            quint.contains("val workflowExitTargets: List[str] = []"),
            "Quint workflow artifacts must explicitly model workflow-exit targets for transition target resolution"
        );
        assert!(
            quint.contains("val requiredEntryLifecycleStates: List[WorkflowEntryLifecycleStateName] = [FreshUninitialized,InitializedUnauthenticated,InitializedAuthenticated,PartiallyConfigured,FullyConfigured]"),
            "Quint workflow artifacts must encode the required application-entry lifecycle states"
        );
    }

    fn assert_workflow_step_relationship_invariants(quint: &str) {
        assert!(
            quint.contains(
                "type WorkflowStepRelationshipName = StepEntry | StepMain | StepBranch | StepAlternate | StepAsyncLifecycle | StepSupporting"
            ),
            "Quint workflow artifacts must model workflow step relationships as a closed domain type"
        );
        assert!(
            quint.contains(
                "type WorkflowStepRelationship = { step: str, relationship: WorkflowStepRelationshipName }"
            ),
            "Quint workflow artifacts must represent workflow step relationships separately from rendering concerns"
        );
        assert!(
            quint.contains("val workflowStepRelationships: List[WorkflowStepRelationship] ="),
            "Quint workflow artifacts must emit workflow step relationships"
        );
        assert!(
            quint.contains(
                "val workflowStepRelationships: List[WorkflowStepRelationship] = [{ step: \"capture-ticket\", relationship: StepEntry },{ step: \"review-ticket\", relationship: StepMain }]"
            ),
            "Quint workflow artifacts must emit concrete workflow step relationships"
        );
        assert!(
            quint.contains("val workflowStepRelationshipsAreAllowed = workflowStepRelationships.select(step => workflowStepRelationshipIsAllowed(step)).length() == workflowStepRelationships.length()"),
            "Quint workflow artifacts must expose allowed step relationships as an invariant"
        );
        assert!(
            quint.contains("val workflowStepSlugsAreUnique = workflowSliceSlugs.select(step => workflowSliceSlugs.select(other => other == step).length() == 1).length() == workflowSliceSlugs.length()"),
            "Quint workflow artifacts must verify workflow step slugs are unique"
        );
        assert!(
            quint.contains("val workflowHasExactlyOneEntryStep = workflowStepRelationships.select(step => step.relationship == StepEntry).length() == 1"),
            "Quint workflow artifacts must verify the composition has exactly one entry step"
        );
        assert!(
            quint.contains("val workflowMainStepsHaveIncomingReachability = workflowStepRelationships.select(step => workflowMainStepHasIncomingTransition(step)).length() == workflowStepRelationships.length()"),
            "Quint workflow artifacts must verify main workflow steps have incoming reachability"
        );
    }

    fn assert_workflow_reachability_invariants(quint: &str) {
        assert!(
            quint.contains("def workflowReachableStepsAfterFuel(fuel, reachable) ="),
            "Quint workflow artifacts must compute workflow reachability from the entry step"
        );
        assert!(
            quint.contains("val workflowReachableStepsFromEntry = workflowReachableStepsAfterFuel(2, workflowEntrySteps)"),
            "Quint workflow artifacts must bound reachability traversal by the emitted workflow size"
        );
        assert!(
            quint.contains("def workflowStepIsReachableFromEntry(step) = step.relationship == StepSupporting or step.relationship == StepAsyncLifecycle or workflowReachableStepsFromEntry.select(reachableStep => reachableStep == step.step).length() > 0"),
            "Quint workflow artifacts must exempt supporting and async lifecycle steps from required entry reachability"
        );
        assert!(
            quint.contains("val workflowNonSupportingStepsReachableFromEntry = workflowStepRelationships.select(step => workflowStepIsReachableFromEntry(step)).length() == workflowStepRelationships.length()"),
            "Quint workflow artifacts must expose non-supporting workflow reachability as an invariant"
        );
        assert!(
            quint.contains("def workflowBranchOrAlternateStepHasTriggerOrRationale(step) = (step.relationship != StepBranch and step.relationship != StepAlternate) or workflowTransitions.select(transition => transition.target == step.step and (transition.trigger != \"\" or transition.rationale != \"\")).length() > 0"),
            "Quint workflow artifacts must define branch and alternate step trigger/rationale obligations"
        );
        assert!(
            quint.contains("val workflowBranchAndAlternateStepsHaveTriggerOrRationale = workflowStepRelationships.select(step => workflowBranchOrAlternateStepHasTriggerOrRationale(step)).length() == workflowStepRelationships.length()"),
            "Quint workflow artifacts must verify branch and alternate steps explain why they are reached"
        );
    }

    fn assert_workflow_lifecycle_invariants(quint: &str) {
        assert!(
            quint.contains("def workflowEntryLifecycleStateCovered(state) = workflowEntryLifecycleStates.select(coverage => coverage.state == state and workflowSliceSlugs.select(step => step == coverage.step).length() > 0 and coverage.evidence != \"\").length() > 0"),
            "Quint workflow artifacts must check lifecycle coverage with the closed lifecycle-state type"
        );
        assert!(
            quint.contains("val workflowEntryLifecycleStatesCoverRequiredStates = not(workflowRequiresEntryLifecycleCoverage) or requiredEntryLifecycleStates.select(state => workflowEntryLifecycleStateCovered(state)).length() == requiredEntryLifecycleStates.length()"),
            "Quint workflow artifacts must expose application-entry lifecycle coverage as an invariant"
        );
    }

    fn assert_workflow_transition_resolution_invariants(quint: &str) {
        assert!(
            quint.contains(
                "val workflowTransitionSourcesResolve = workflowTransitions.select(transition => workflowSliceSlugs.select(step => step == transition.source).length() > 0).length() == workflowTransitions.length()"
            ),
            "Quint workflow artifacts must verify transition sources are composed workflow steps"
        );
        assert!(
            quint.contains(
                "val workflowTransitionTargetsResolve = workflowTransitions.select(transition => workflowSliceSlugs.select(step => step == transition.target).length() > 0 or workflowExitTargets.select(exitTarget => exitTarget == transition.target).length() > 0).length() == workflowTransitions.length()"
            ),
            "Quint workflow artifacts must verify transition targets are composed steps or explicit workflow exits"
        );
        assert!(
            quint.contains(
                "def workflowTransitionKindIsModeled(transition) = transition.kind == Navigation or transition.kind == Command or transition.kind == Event or transition.kind == ExternalTrigger or transition.kind == Outcome or transition.kind == WorkflowExitNavigation or transition.kind == WorkflowExitCommand or transition.kind == WorkflowExitEvent or transition.kind == WorkflowExitExternalTrigger or transition.kind == WorkflowExitOutcome"
            ),
            "Quint workflow artifacts must model the legal workflow transition kinds, including explicit workflow exits"
        );
        assert!(
            quint.contains(
                "def workflowTransitionExitHasRationale(transition) = workflowExitTargets.select(exitTarget => exitTarget == transition.target).length() == 0 or transition.rationale != \"\""
            ),
            "Quint workflow artifacts must require workflow exits to explain why the exit is reached"
        );
        assert!(
            quint.contains(
                "val workflowTransitionsHaveModeledKinds = workflowTransitions.select(transition => workflowTransitionKindIsModeled(transition)).length() == workflowTransitions.length()"
            ),
            "Quint workflow artifacts must expose transition-kind legality as an invariant"
        );
        assert!(
            quint.contains(
                "val workflowExitsNameTargetsAndRationale = workflowTransitions.select(transition => workflowTransitionExitHasRationale(transition)).length() == workflowTransitions.length()"
            ),
            "Quint workflow artifacts must expose workflow-exit rationale as an invariant"
        );
    }

    fn assert_workflow_outcome_and_error_invariants(quint: &str) {
        assert!(quint.contains(
            "def workflowOutcomeHandledByTransition(outcome) = not(outcome.externallyRelevant) or workflowTransitions.select(transition => transition.source == outcome.sourceSlice and transition.kind == Outcome and transition.trigger == outcome.label).length() > 0"
        ));
        assert!(quint.contains(
            "val workflowExternallyRelevantOutcomesHandled = workflowOutcomes.select(outcome => workflowOutcomeHandledByTransition(outcome)).length() == workflowOutcomes.length()"
        ));
        assert!(quint.contains(
            "def workflowOutcomeSourceResolves(outcome) = workflowSliceSlugs.select(step => step == outcome.sourceSlice).length() > 0"
        ));
        assert!(quint.contains(
            "val workflowOutcomesSourceResolve = workflowOutcomes.select(outcome => workflowOutcomeSourceResolves(outcome)).length() == workflowOutcomes.length()"
        ));
        assert!(quint.contains(
            "def workflowCommandErrorSourceResolves(error) = workflowSliceSlugs.select(step => step == error.sourceSlice).length() > 0"
        ));
        assert!(quint.contains(
            "val workflowCommandErrorsSourceResolve = workflowCommandErrors.select(error => workflowCommandErrorSourceResolves(error)).length() == workflowCommandErrors.length()"
        ));
        assert!(quint.contains(
            "val workflowTransitionsDoNotUseCommandErrorsAsOutcomes = workflowTransitions.select(transition => transition.kind != Outcome or workflowCommandErrors.select(error => error.sourceSlice == transition.source and error.errorName == transition.trigger).length() == 0).length() == workflowTransitions.length()"
        ));
    }

    fn assert_workflow_owned_definition_invariants(quint: &str) {
        assert!(quint.contains(
            "def workflowNonEventDefinitionOwnedOnce(definition) = definition.definitionKind == OwnedEvent or workflowOwnedDefinitions.select(other => other.definitionKind == definition.definitionKind and other.definitionName == definition.definitionName).length() == 1"
        ));
        assert!(quint.contains(
            "val workflowNonEventDefinitionsAreUniquelyOwned = workflowOwnedDefinitions.select(definition => workflowNonEventDefinitionOwnedOnce(definition)).length() == workflowOwnedDefinitions.length()"
        ));
        assert!(quint.contains(
            "def workflowEventDefinitionHasIdentity(definition) = definition.definitionKind != OwnedEvent or (definition.definitionStream != \"\" and definition.sourceProvenance != \"\")"
        ));
        assert!(quint.contains(
            "def workflowSharedEventDefinitionMatches(left, right) = left.definitionKind != OwnedEvent or right.definitionKind != OwnedEvent or left.definitionName != right.definitionName or (left.definitionStream == right.definitionStream and left.sourceProvenance == right.sourceProvenance)"
        ));
        assert!(quint.contains(
            "val workflowSharedEventDefinitionsHaveIdenticalIdentity = workflowOwnedDefinitions.select(definition => workflowEventDefinitionHasIdentity(definition)).length() == workflowOwnedDefinitions.length() and workflowOwnedDefinitions.select(definition => workflowOwnedDefinitions.select(other => workflowSharedEventDefinitionMatches(definition, other)).length() == workflowOwnedDefinitions.length()).length() == workflowOwnedDefinitions.length()"
        ));
        assert!(quint.contains(
            "val workflowOnlyEventsMayBeSharedAcrossSlices = workflowNonEventDefinitionsAreUniquelyOwned and workflowSharedEventDefinitionsHaveIdenticalIdentity"
        ));
        assert!(quint.contains(
            "def workflowOwnsDefinition(sourceSlice, definitionKind, definitionName) = workflowOwnedDefinitions.select(definition => definition.sourceSlice == sourceSlice and definition.definitionKind == definitionKind and definition.definitionName == definitionName).length() > 0"
        ));
    }

    fn assert_workflow_command_transition_invariants(quint: &str) {
        assert!(quint.contains(
            "def workflowCommandTransitionTargetsOwnedCommand(transition) = transition.kind != Command or workflowOwnsDefinition(transition.target, OwnedCommand, transition.trigger)"
        ));
        assert!(quint.contains(
            "val workflowCommandTransitionsTargetOwnedCommands = workflowTransitions.select(transition => workflowCommandTransitionTargetsOwnedCommand(transition)).length() == workflowTransitions.length()"
        ));
        assert!(quint.contains(
            "def workflowCommandTransitionSourceOwnsControl(transition) = transition.kind != Command or workflowOwnsDefinition(transition.source, OwnedControl, transition.trigger)"
        ));
        assert!(quint.contains(
            "val workflowCommandTransitionsSourceOwnedControls = workflowTransitions.select(transition => workflowCommandTransitionSourceOwnsControl(transition)).length() == workflowTransitions.length()"
        ));
        assert!(quint.contains(
            "val workflowCommandTransitionsResolveControlsAndCommands = workflowTransitions.select(transition => workflowCommandTransitionSourceOwnsControl(transition) and workflowCommandTransitionTargetsOwnedCommand(transition)).length() == workflowTransitions.length()"
        ));
        assert!(quint.contains(
            "def workflowSliceHasKind(sliceSlug, kind) = workflowSliceDetails.select(detail => detail.slug == sliceSlug and detail.kind == kind).length() > 0"
        ));
        assert!(quint.contains(
            "def workflowStateViewCommandTransitionTargetsStateChange(transition) = transition.kind != Command or not(workflowSliceHasKind(transition.source, SliceStateView)) or workflowSliceHasKind(transition.target, SliceStateChange)"
        ));
        assert!(quint.contains(
            "val workflowStateViewCommandTransitionsTargetStateChanges = workflowTransitions.select(transition => workflowStateViewCommandTransitionTargetsStateChange(transition)).length() == workflowTransitions.length()"
        ));
    }

    fn assert_workflow_event_transition_invariants(quint: &str) {
        assert!(quint.contains(
            "def workflowEventTransitionIsSharedByEndpoints(transition) = transition.kind != Event or (workflowOwnsDefinition(transition.source, OwnedEvent, transition.trigger) and workflowOwnsDefinition(transition.target, OwnedEvent, transition.trigger))"
        ));
        assert!(quint.contains(
            "val workflowEventTransitionsAreSharedByEndpointSlices = workflowTransitions.select(transition => workflowEventTransitionIsSharedByEndpoints(transition)).length() == workflowTransitions.length()"
        ));
        assert!(quint.contains(
            "def workflowEventDefinitionParticipates(sourceSlice, eventName) = workflowOwnedDefinitions.select(definition => definition.sourceSlice == sourceSlice and definition.definitionKind == OwnedEvent and definition.definitionName == eventName and workflowEventParticipationIsModeled(definition)).length() > 0"
        ));
        assert!(quint.contains(
            "val workflowEventTransitionsHaveParticipatingEndpointEvents = workflowTransitions.select(transition => workflowEventTransitionSourceParticipates(transition) and workflowEventTransitionTargetParticipates(transition)).length() == workflowTransitions.length()"
        ));
    }

    fn assert_workflow_navigation_invariants(quint: &str) {
        assert!(quint.contains(
            "def workflowNavigationTransitionSourceOwnsControl(transition) = transition.kind != Navigation or workflowOwnsDefinition(transition.source, OwnedControl, workflowNavigationSourceControl(transition))"
        ));
        assert!(quint.contains(
            "def workflowNavigationTransitionTargetsOwnedView(transition) = transition.kind != Navigation or workflowOwnsDefinition(transition.target, OwnedView, workflowNavigationTargetView(transition))"
        ));
        assert!(quint.contains(
            "val workflowNavigationTransitionsResolveControlsAndViews = workflowTransitions.select(transition => workflowNavigationTransitionSourceOwnsControl(transition) and workflowNavigationTransitionTargetsOwnedView(transition)).length() == workflowTransitions.length()"
        ));
        assert!(quint.contains(
            "def workflowOwnsEntryView(sourceSlice, viewName) = workflowOwnedDefinitions.select(definition => definition.sourceSlice == sourceSlice and definition.definitionKind == OwnedView and definition.definitionName == viewName and workflowViewRoleIsEntry(definition)).length() > 0"
        ));
        assert!(quint.contains(
            "def workflowNavigationTransitionTargetsEntryView(transition) = transition.kind != Navigation or workflowOwnsEntryView(transition.target, workflowNavigationTargetView(transition))"
        ));
        assert!(quint.contains(
            "val workflowNavigationTransitionsResolveToEntryViews = workflowTransitions.select(transition => workflowNavigationTransitionTargetsEntryView(transition)).length() == workflowTransitions.length()"
        ));
    }

    fn assert_workflow_external_trigger_invariants(quint: &str) {
        assert!(quint.contains(
            "def workflowExternalTriggerDeclaresPayloadContract(transition) = transition.kind != ExternalTrigger or (transition.payloadContract != \"\" and workflowOwnsDefinition(transition.source, OwnedExternalPayload, transition.payloadContract))"
        ));
        assert!(quint.contains(
            "val workflowExternalTriggersDeclarePayloadContracts = workflowTransitions.select(transition => workflowExternalTriggerDeclaresPayloadContract(transition)).length() == workflowTransitions.length()"
        ));
        assert!(quint.contains(
            "def workflowExternalTriggerPayloadContractHasProvenance(transition) = transition.kind != ExternalTrigger or workflowOwnedDefinitions.select(definition => definition.sourceSlice == transition.source and definition.definitionKind == OwnedExternalPayload and definition.definitionName == transition.payloadContract and definition.sourceProvenance != \"\").length() > 0"
        ));
        assert!(quint.contains(
            "val workflowExternalTriggerPayloadContractsHaveProvenance = workflowTransitions.select(transition => workflowExternalTriggerPayloadContractHasProvenance(transition)).length() == workflowTransitions.length()"
        ));
        assert!(
            !quint.contains("all { transition <- workflowTransitions }"),
            "Quint transition invariant must be a pure list expression, not an action all block"
        );
        assert!(
            !quint.contains("length(workflowTransitions) == length(workflowTransitions)"),
            "Quint transition invariant must not be a tautological length self-comparison"
        );
    }

    fn assert_workflow_model_state(quint: &str) {
        assert!(quint.contains("var modelState: int"));
        assert!(quint.contains("action init = modelState' = 0"));
        assert!(quint.contains("action step = modelState' = modelState"));
    }

    #[test]
    fn quint_slice_module_exposes_verification_entrypoints() -> Result<(), Box<dyn Error>> {
        let slice_name = parse_model_name("Capture ticket")?;
        let slice_description = parse_model_description("Actor enters repair ticket details.")?;
        let slice_slug = parse_slice_slug("capture-ticket")?;
        let slice_kind = SliceKindName::try_new("state_view")?;
        let module = emit_slice_module(
            &parse_quint_module_name("CaptureTicket")?,
            &slice_name,
            &slice_description,
            &slice_slug,
            slice_kind,
            &slice_artifact_digest(&slice_name, &slice_slug, slice_kind, &slice_description),
        );
        let quint = module.as_ref();

        assert_slice_header_and_digest(quint);
        assert_slice_type_declarations(quint);
        assert_slice_reference_types(quint);
        assert_slice_command_value_declarations(quint);
        assert_slice_event_value_declarations(quint);
        assert_slice_read_model_value_declarations(quint);
        assert_slice_view_value_declarations(quint);
        assert_slice_scenario_value_declarations(quint);
        assert_slice_scenario_invariants(quint);
        assert_slice_contract_scenario_invariants(quint);
        assert_slice_command_input_invariants(quint);
        assert_slice_command_input_source_invariants(quint);
        assert_slice_command_error_invariants(quint);
        assert_slice_automation_invariants(quint);
        assert_slice_translation_invariants(quint);
        assert_slice_board_element_invariants(quint);
        assert_slice_board_connection_invariants(quint);
        assert_slice_outcome_invariants(quint);
        assert_slice_event_invariants(quint);
        assert_slice_event_attribute_invariants(quint);
        assert_slice_read_model_field_invariants(quint);
        assert_slice_view_field_invariants(quint);
        assert_slice_view_provenance_invariants(quint);
        assert_slice_data_flow_invariants(quint);
        assert_slice_view_control_invariants(quint);
        assert_slice_kind_ownership_invariants(quint);
        assert_slice_coherence_invariants(quint);
        assert_slice_navigation_invariants(quint);
        assert_slice_identity_and_model_state(quint);

        Ok(())
    }

    fn assert_slice_header_and_digest(quint: &str) {
        assert!(quint.contains("module CaptureTicket"));
        assert!(
            quint.contains(
                "// EMC-DIGEST: slice:name=Capture ticket;slug=capture-ticket;kind=state_view;description=Actor enters repair ticket details."
            )
        );
    }

    fn assert_slice_type_declarations(quint: &str) {
        assert!(quint.contains(
            "type EventModelScenario = { name: str, givenSteps: List[str], whenSteps: List[str], thenSteps: List[str], readStreams: List[str], writtenStreams: List[str], contractKind: str, coveredDefinition: str, errorReferences: List[str] }"
        ));
        assert!(quint.contains(
            "type BitLevelDataFlow = { datum: str, sourceKind: str, source: str, transformationSemantics: str, target: str, bitEncoding: str }"
        ));
        assert!(quint.contains(
            "type CommandInputSourceKind = CommandInputActor | CommandInputSession | CommandInputGenerated | CommandInputExternalPayload | CommandInputEventStreamState | CommandInputInvocationArgument\n  type CommandInput = { name: str, sourceKind: CommandInputSourceKind, sourceDescription: str, provenanceChain: List[str], eventStreamSourceEvent: str, eventStreamSourceAttribute: str, externalPayloadSourceName: str, externalPayloadSourceField: str, generatedSourceName: str, generatedSourceField: str, sessionSourceName: str, sessionSourceField: str, invocationArgumentSourceName: str, invocationArgumentSourceField: str }"
        ));
        assert!(quint.contains(
            "type CommandErrorDefinition = { name: str, scenarioName: str, recoveryKind: str }"
        ));
        assert!(quint.contains(
            "type CommandDefinition = { name: str, inputs: List[CommandInput], emittedEvents: List[SliceEventReference], observedStreams: List[SliceStreamReference], errors: List[CommandErrorDefinition], singleton: bool, repeatBehavior: str }"
        ));
        assert!(quint.contains(
            "type OutcomeDefinition = { label: str, eventSet: List[str], externallyRelevant: bool }"
        ));
        assert!(quint.contains("type StreamDefinition = { name: str }"));
        assert!(quint.contains(
            "type EventAttribute = { name: str, sourceKind: str, sourceName: str, sourceField: str, generatedSourceKind: str, provenanceDescription: str }"
        ));
        assert!(
            quint.contains("type ExternalPayloadField = { name: str, provenanceDescription: str, bitEncoding: str }\n  type ExternalPayloadDefinition = { name: str, fields: List[ExternalPayloadField] }")
        );
        assert!(quint.contains(
            "type EventDefinition = { name: str, stream: str, attributes: List[EventAttribute], observed: bool, shared: bool }"
        ));
        assert!(quint.contains(
            "type ReadModelField = { name: str, sourceKind: str, sourceEvent: str, sourceAttribute: str, derivationRule: str, derivationSourceFields: List[str], absenceEvent: str, derivationScenarioName: str, absenceScenarioName: str, provenanceDescription: str }"
        ));
        assert!(
            quint
                .contains("type ReadModelDefinition = { name: str, fields: List[ReadModelField], transitive: bool, relationshipFields: List[str], transitiveRule: str, exampleScenarioName: str }")
        );
        assert!(quint.contains(
            "type ViewField = { name: str, sourceKind: str, sourceReadModel: str, sourceField: str, sketchToken: str, provenanceDescription: str, bitEncoding: str }"
        ));
        assert!(quint.contains(
            "type ControlInputProvision = { name: str, sourceKind: CommandInputSourceKind, sourceDescription: str, sketchToken: str, visibleToActor: bool, decisionField: bool }"
        ));
        assert!(quint.contains(
            "type NavigationTarget = { targetType: str, targetName: str, externalWorkflowName: str, externalSystemName: str, handoffContract: str }"
        ));
        assert!(quint.contains(
            "type ControlDefinition = { name: str, commandName: str, inputs: List[ControlInputProvision], handledErrors: List[str], recoveryBehavior: str, sketchToken: str, navigation: NavigationTarget }"
        ));
        assert!(quint.contains(
            "type ViewDefinition = { name: str, readModels: List[str], fields: List[ViewField], controls: List[ControlDefinition], sketchTokens: List[str], localStates: List[str], filters: List[str] }"
        ));
        assert!(quint.contains(
            "type AutomationDefinition = { name: str, triggerName: str, commandName: str, handledErrors: List[str], reactionDescription: str }"
        ));
        assert!(quint.contains(
            "type TranslationDefinition = { name: str, externalEventName: str, payloadContractName: str, commandName: str }"
        ));
        assert!(quint.contains(
            "type BoardElement = { name: str, kind: str, lane: str, declaredName: str, mainPath: bool }"
        ));
        assert!(quint.contains(
            "type BoardConnection = { source: str, sourceKind: str, target: str, targetKind: str }"
        ));
    }

    fn assert_slice_reference_types(quint: &str) {
        assert!(
            quint.contains("type SliceEventReference = { name: str }"),
            "Quint slice artifacts must represent referenced event names as typed records"
        );
        assert!(
            quint.contains("type SliceCommandReference = { name: str }"),
            "Quint slice artifacts must represent referenced command names as typed records"
        );
        assert!(
            quint.contains("type SliceReadModelReference = { name: str }"),
            "Quint slice artifacts must represent referenced read model names as typed records"
        );
        assert!(
            quint.contains("type SliceViewReference = { name: str }"),
            "Quint slice artifacts must represent referenced view names as typed records"
        );
    }

    fn assert_slice_command_value_declarations(quint: &str) {
        assert!(quint.contains("val sliceCommands: List[SliceCommandReference] = []"));
        assert!(quint.contains(
            "val sliceCommandNames: List[str] = sliceCommands.foldl([], (names, commandRef) => names.append(commandRef.name))"
        ));
        assert!(quint.contains("val sliceCommandDefinitions: List[CommandDefinition] = []"));
        assert!(quint.contains("val sliceAutomations: List[AutomationDefinition] = []"));
        assert!(quint.contains("val sliceTranslations: List[TranslationDefinition] = []"));
        assert!(
            quint.contains("val canonicalBoardLanes: List[str] = [\"ux\",\"actions\",\"events\"]")
        );
        assert!(quint.contains("val sliceBoardElements: List[BoardElement] = []"));
        assert!(quint.contains("val sliceBoardConnections: List[BoardConnection] = []"));
        assert!(quint.contains("val sliceReferencedCommands: List[SliceCommandReference] = []"));
        assert!(quint.contains(
            "val sliceReferencedCommandNames: List[str] = sliceReferencedCommands.foldl([], (names, commandRef) => names.append(commandRef.name))"
        ));
        assert!(quint.contains("val sliceOutcomeDefinitions: List[OutcomeDefinition] = []"));
        assert!(quint.contains(
            "val allowedCommandInputSourceKinds: List[CommandInputSourceKind] = [CommandInputActor,CommandInputSession,CommandInputGenerated,CommandInputExternalPayload,CommandInputEventStreamState,CommandInputInvocationArgument]"
        ));
        assert!(quint.contains(
            "val allowedRecoveryKinds: List[str] = [\"retry\",\"stay_on_screen\",\"navigation\",\"explicit_recovery_action\"]"
        ));
        assert!(quint.contains(
            "val allowedSingletonRepeatBehaviors: List[str] = [\"already_exists_error\",\"idempotent\"]"
        ));
    }

    fn assert_slice_event_value_declarations(quint: &str) {
        assert!(quint.contains("val sliceEvents: List[SliceEventReference] = []"));
        assert!(quint.contains(
            "val sliceEventNames: List[str] = sliceEvents.foldl([], (names, eventRef) => names.append(eventRef.name))"
        ));
        assert!(quint.contains("val sliceStreams: List[StreamDefinition] = []"));
        assert!(quint.contains("val sliceExternalPayloads: List[ExternalPayloadDefinition] = []"));
        assert!(quint.contains("val sliceEventDefinitions: List[EventDefinition] = []"));
        assert!(quint.contains(
            "val storedEventFactSourceKinds: List[str] = [\"command_input\",\"external_payload\",\"generated\",\"session\",\"derivation\"]"
        ));
        assert!(quint.contains(
            "val allowedEventAttributeSourceKinds: List[str] = storedEventFactSourceKinds"
        ));
    }

    fn assert_slice_read_model_value_declarations(quint: &str) {
        assert!(quint.contains("val sliceReadModels: List[SliceReadModelReference] = []"));
        assert!(quint.contains(
            "val sliceReadModelNames: List[str] = sliceReadModels.foldl([], (names, readModelRef) => names.append(readModelRef.name))"
        ));
        assert!(quint.contains("val sliceReadModelDefinitions: List[ReadModelDefinition] = []"));
        assert!(quint.contains(
            "val allowedReadModelFieldSourceKinds: List[str] = [\"event_attribute\",\"derivation\",\"absence_default\"]"
        ));
    }

    fn assert_slice_view_value_declarations(quint: &str) {
        assert!(quint.contains("val sliceViews: List[SliceViewReference] = []"));
        assert!(quint.contains(
            "val sliceViewNames: List[str] = sliceViews.foldl([], (names, viewRef) => names.append(viewRef.name))"
        ));
        assert!(quint.contains("val sliceViewDefinitions: List[ViewDefinition] = []"));
        assert!(quint.contains("val allowedViewFieldSourceKinds: List[str] = [\"read_model\"]"));
        assert!(quint.contains(
            "val allowedControlInputSourceKinds: List[CommandInputSourceKind] = [CommandInputActor,CommandInputSession,CommandInputGenerated,CommandInputExternalPayload,CommandInputEventStreamState,CommandInputInvocationArgument]"
        ));
        assert!(quint.contains(
            "val allowedNavigationTargetTypes: List[str] = [\"modeled_view\",\"local_view_state\",\"external_system\",\"external_workflow\"]"
        ));
    }

    fn assert_slice_scenario_value_declarations(quint: &str) {
        assert!(quint.contains("val sliceAcceptanceScenarios: List[EventModelScenario] = []"));
        assert!(quint.contains("val sliceContractScenarios: List[EventModelScenario] = []"));
        assert!(quint.contains("val sliceBitLevelDataFlows: List[BitLevelDataFlow] = []"));
        assert!(quint.contains(
            "val sliceAcceptanceScenariosHaveGwt = sliceAcceptanceScenarios.select(scenario => scenario.name != \"\" and scenario.givenSteps.length() > 0 and scenario.whenSteps.length() > 0 and scenario.thenSteps.length() > 0).length() == sliceAcceptanceScenarios.length()"
        ));
        assert!(quint.contains(
            "val sliceContractScenariosHaveGwt = sliceContractScenarios.select(scenario => scenario.name != \"\" and scenario.givenSteps.length() > 0 and scenario.whenSteps.length() > 0 and scenario.thenSteps.length() > 0).length() == sliceContractScenarios.length()"
        ));
        assert!(quint.contains(
            "val sliceScenariosHaveGwt = sliceAcceptanceScenariosHaveGwt and sliceContractScenariosHaveGwt"
        ));
        assert!(quint.contains(
            "val sliceScenarioNamesAreUnique = sliceAcceptanceScenarios.select(scenario => sliceAcceptanceScenarios.select(other => other.name == scenario.name).length() + sliceContractScenarios.select(other => other.name == scenario.name).length() == 1).length() == sliceAcceptanceScenarios.length() and sliceContractScenarios.select(scenario => sliceAcceptanceScenarios.select(other => other.name == scenario.name).length() + sliceContractScenarios.select(other => other.name == scenario.name).length() == 1).length() == sliceContractScenarios.length()"
        ));
        assert!(quint.contains(
            "def definitionNamesAreUnique(names) = names.select(name => names.select(other => other == name).length() == 1).length() == names.length()"
        ));
        assert!(quint.contains(
            "val sliceOwnedCommandNames: List[str] = sliceCommandDefinitions.foldl([], (names, command) => names.append(command.name))"
        ));
        assert!(quint.contains(
            "val sliceOwnedControlNames: List[str] = sliceViewDefinitions.foldl([], (names, view) => names.concat(view.controls.foldl([], (controlNames, control) => controlNames.append(control.name))))"
        ));
        assert!(quint.contains(
            "val sliceNamedDefinitionsAreUniquelyOwned = definitionNamesAreUnique(sliceCommandNames) and definitionNamesAreUnique(sliceOwnedCommandNames) and definitionNamesAreUnique(sliceEventNames) and definitionNamesAreUnique(sliceOwnedEventNames) and definitionNamesAreUnique(sliceOwnedStreamNames) and definitionNamesAreUnique(sliceOwnedExternalPayloadNames) and definitionNamesAreUnique(sliceReadModelNames) and definitionNamesAreUnique(sliceOwnedReadModelNames) and definitionNamesAreUnique(sliceViewNames) and definitionNamesAreUnique(sliceOwnedViewNames) and definitionNamesAreUnique(sliceOwnedAutomationNames) and definitionNamesAreUnique(sliceOwnedTranslationNames) and definitionNamesAreUnique(sliceOwnedControlNames)"
        ));
    }

    fn assert_slice_scenario_invariants(quint: &str) {
        assert!(quint.contains(
            "def scenarioStreamResolves(streamName) = sliceStreams.select(stream => stream.name == streamName).length() > 0"
        ));
        assert!(quint.contains(
            "def scenarioStreamsResolve(scenario) = scenario.readStreams.select(streamName => scenarioStreamResolves(streamName)).length() == scenario.readStreams.length() and scenario.writtenStreams.select(streamName => scenarioStreamResolves(streamName)).length() == scenario.writtenStreams.length()"
        ));
        assert!(quint.contains(
            "def stateChangeScenarioNamesStreams(scenario) = sliceKind != SliceStateChange or (scenario.readStreams.length() > 0 and scenario.writtenStreams.length() > 0)"
        ));
        assert!(quint.contains(
            "val sliceAcceptanceScenarioStreamsResolve = sliceAcceptanceScenarios.select(scenario => scenarioStreamsResolve(scenario)).length() == sliceAcceptanceScenarios.length()"
        ));
        assert!(quint.contains(
            "val sliceContractScenarioStreamsResolve = sliceContractScenarios.select(scenario => scenarioStreamsResolve(scenario)).length() == sliceContractScenarios.length()"
        ));
        assert!(quint.contains(
            "val sliceScenarioStreamsResolve = sliceAcceptanceScenarioStreamsResolve and sliceContractScenarioStreamsResolve"
        ));
        assert!(quint.contains(
            "val stateChangeAcceptanceScenariosNameStreams = sliceAcceptanceScenarios.select(scenario => stateChangeScenarioNamesStreams(scenario)).length() == sliceAcceptanceScenarios.length()"
        ));
        assert!(quint.contains(
            "val stateChangeContractScenariosNameStreams = sliceContractScenarios.select(scenario => stateChangeScenarioNamesStreams(scenario)).length() == sliceContractScenarios.length()"
        ));
        assert!(quint.contains(
            "val stateChangeScenariosNameStreams = stateChangeAcceptanceScenariosNameStreams and stateChangeContractScenariosNameStreams"
        ));
    }

    fn assert_slice_contract_scenario_invariants(quint: &str) {
        assert!(quint.contains(
            "val acceptanceScenariosAreUserFacing = sliceAcceptanceScenarios.select(scenario => scenario.contractKind == \"\" and scenario.coveredDefinition == \"\").length() == sliceAcceptanceScenarios.length()"
        ));
        assert!(quint.contains(
            "def scenarioCoversContract(contractKind, definitionName, scenario) = scenario.contractKind == contractKind and scenario.coveredDefinition == definitionName"
        ));
        assert!(quint.contains(
            "def readModelHasProjectorContract(readModel) = sliceContractScenarios.select(scenario => scenarioCoversContract(\"projector\", readModel.name, scenario)).length() > 0"
        ));
        assert!(quint.contains(
            "val stateViewReadModelsHaveProjectorContracts = sliceKind != SliceStateView or sliceReadModelDefinitions.select(readModel => readModelHasProjectorContract(readModel)).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "def contractScenarioTargetsKnownDefinition(scenario) = (scenario.contractKind == \"projector\" and (sliceReadModelNames.select(readModelName => readModelName == scenario.coveredDefinition).length() > 0 or sliceReadModelDefinitions.select(readModel => readModel.name == scenario.coveredDefinition).length() > 0)) or (scenario.contractKind == \"command\" and (sliceCommandNames.select(commandName => commandName == scenario.coveredDefinition).length() > 0 or sliceCommandDefinitions.select(command => command.name == scenario.coveredDefinition).length() > 0)) or (scenario.contractKind == \"automation\" and sliceAutomations.select(automation => automation.name == scenario.coveredDefinition).length() > 0) or (scenario.contractKind == \"translation\" and sliceTranslations.select(translation => translation.name == scenario.coveredDefinition).length() > 0) or (scenario.contractKind == \"derivation\" and scenario.coveredDefinition != \"\" and sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelField.sourceKind == \"derivation\" and readModelField.derivationScenarioName == scenario.name).length() > 0).length() > 0) or (scenario.contractKind == \"absence\" and scenario.coveredDefinition != \"\" and sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelField.sourceKind == \"absence_default\" and readModelField.absenceScenarioName == scenario.name).length() > 0).length() > 0) or (scenario.contractKind == \"transitive\" and sliceReadModelDefinitions.select(readModel => readModel.transitive and readModel.name == scenario.coveredDefinition and readModel.exampleScenarioName == scenario.name).length() > 0)"
        ));
        assert!(quint.contains(
            "val contractScenariosTargetKnownDefinitions = sliceContractScenarios.select(scenario => contractScenarioTargetsKnownDefinition(scenario)).length() == sliceContractScenarios.length()"
        ));
        assert!(quint.contains(
            "def commandHasContractScenario(command) = sliceContractScenarios.select(scenario => scenarioCoversContract(\"command\", command.name, scenario)).length() > 0"
        ));
        assert!(quint.contains(
            "def automationHasContractScenario(automation) = sliceContractScenarios.select(scenario => scenarioCoversContract(\"automation\", automation.name, scenario)).length() > 0"
        ));
        assert!(quint.contains(
            "def translationHasContractScenario(translation) = sliceContractScenarios.select(scenario => scenarioCoversContract(\"translation\", translation.name, scenario)).length() > 0"
        ));
        assert!(quint.contains(
            "def derivationFieldHasContractScenario(readModelField) = readModelField.sourceKind != \"derivation\" or sliceContractScenarios.select(scenario => scenario.contractKind == \"derivation\" and scenario.coveredDefinition != \"\" and scenario.name == readModelField.derivationScenarioName).length() > 0"
        ));
        assert!(quint.contains(
            "val contractScenariosCoverModeledContracts = sliceCommandDefinitions.select(command => commandHasContractScenario(command)).length() == sliceCommandDefinitions.length() and sliceAutomations.select(automation => automationHasContractScenario(automation)).length() == sliceAutomations.length() and sliceTranslations.select(translation => translationHasContractScenario(translation)).length() == sliceTranslations.length() and sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => derivationFieldHasContractScenario(readModelField)).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
    }

    fn assert_slice_command_input_invariants(quint: &str) {
        assert!(quint.contains(
            "val commandInputsHaveAllowedSources = sliceCommandDefinitions.select(command => command.inputs.select(input => allowedCommandInputSourceKinds.select(sourceKind => sourceKind == input.sourceKind).length() > 0).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "val commandInputsHaveProvenance = sliceCommandDefinitions.select(command => command.inputs.select(input => input.name != \"\" and input.sourceDescription != \"\" and input.provenanceChain.length() > 0).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def commandInputSessionInputHasDescription(input) = input.sourceKind != CommandInputSession or input.sourceDescription != \"\""
        ));
        assert!(quint.contains(
            "def commandHasIssuingControl(command) = sliceViewDefinitions.select(view => view.controls.select(control => control.commandName == command.name).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "def commandInputWithoutIssuingControlHasProvenance(command, input) = commandHasIssuingControl(command) or (input.name != \"\" and input.sourceDescription != \"\" and input.provenanceChain.length() > 0)"
        ));
        assert!(quint.contains(
            "val commandInputsWithoutIssuingControlsHaveProvenance = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputWithoutIssuingControlHasProvenance(command, input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "val commandSessionInputsHaveDescriptions = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputSessionInputHasDescription(input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def commandInputTracesToInvocationSource(input) = allowedCommandInputSourceKinds.select(sourceKind => sourceKind == input.sourceKind).length() > 0 and input.provenanceChain.length() > 0"
        ));
        assert!(quint.contains(
            "val commandInputsTraceToInvocationSources = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputTracesToInvocationSource(input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
    }

    fn assert_slice_command_input_source_invariants(quint: &str) {
        assert!(quint.contains(
            "def commandObservedStreamNames(command) = command.observedStreams.foldl([], (names, streamRef) => names.append(streamRef.name))"
        ));
        assert!(quint.contains(
            "def commandInputEventStreamSourceResolves(command, input) = input.sourceKind != CommandInputEventStreamState or (commandObservedStreamNames(command).length() > 0 and commandObservedStreamNames(command).select(streamName => scenarioStreamResolves(streamName)).length() == commandObservedStreamNames(command).length() and input.eventStreamSourceEvent != \"\" and input.eventStreamSourceAttribute != \"\" and sliceEventDefinitions.select(event => event.name == input.eventStreamSourceEvent and event.attributes.select(attribute => attribute.name == input.eventStreamSourceAttribute).length() > 0).length() > 0)"
        ));
        assert!(quint.contains(
            "val commandInputsSourcedFromEventStreamsResolve = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputEventStreamSourceResolves(command, input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def commandInputExternalPayloadSourceResolves(input) = input.sourceKind != CommandInputExternalPayload or (input.externalPayloadSourceName != \"\" and input.externalPayloadSourceField != \"\" and sliceExternalPayloads.select(payload => payload.name == input.externalPayloadSourceName and payload.fields.select(payloadField => payloadField.name == input.externalPayloadSourceField).length() > 0).length() > 0)"
        ));
        assert!(quint.contains(
            "val commandInputsSourcedFromExternalPayloadsResolve = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputExternalPayloadSourceResolves(input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def commandInputGeneratedSourceHasCoordinates(input) = input.sourceKind != CommandInputGenerated or (input.generatedSourceName != \"\" and input.generatedSourceField != \"\")"
        ));
        assert!(quint.contains(
            "val commandInputsSourcedFromGeneratedValuesHaveCoordinates = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputGeneratedSourceHasCoordinates(input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def commandInputInvocationArgumentSourceHasCoordinates(input) = input.sourceKind != CommandInputInvocationArgument or (input.invocationArgumentSourceName != \"\" and input.invocationArgumentSourceField != \"\")"
        ));
        assert!(quint.contains(
            "val commandInputsSourcedFromInvocationArgumentsHaveCoordinates = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputInvocationArgumentSourceHasCoordinates(input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def bitLevelFlowCoversTarget(target, datum) = sliceBitLevelDataFlows.select(flow => flow.target == target and flow.datum == datum and flow.sourceKind != \"\" and flow.source != \"\" and flow.transformationSemantics != \"\" and flow.bitEncoding != \"\").length() > 0"
        ));
        assert!(quint.contains(
            "def commandInputHasBitLevelFlow(command, input) = bitLevelFlowCoversTarget(command.name, input.name)"
        ));
    }

    fn assert_slice_command_error_invariants(quint: &str) {
        assert!(quint.contains(
            "val commandErrorsAreDeclared = sliceCommandDefinitions.select(command => command.errors.select(error => error.name != \"\" and error.scenarioName != \"\" and error.recoveryKind != \"\").length() == command.errors.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "val commandErrorsHaveAllowedRecovery = sliceCommandDefinitions.select(command => command.errors.select(error => allowedRecoveryKinds.select(recoveryKind => recoveryKind == error.recoveryKind).length() > 0).length() == command.errors.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def scenarioNameIsModeled(scenarioName) = sliceAcceptanceScenarios.select(scenario => scenario.name == scenarioName).length() > 0 or sliceContractScenarios.select(scenario => scenario.name == scenarioName).length() > 0"
        ));
        assert!(quint.contains(
            "def commandErrorHasScenarioCoverage(command, error) = sliceContractScenarios.select(scenario => scenario.name == error.scenarioName and scenario.contractKind == \"command\" and scenario.coveredDefinition == command.name and scenario.errorReferences.select(errorName => errorName == error.name).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val commandErrorsHaveScenarioCoverage = sliceCommandDefinitions.select(command => command.errors.select(error => commandErrorHasScenarioCoverage(command, error)).length() == command.errors.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "def scenarioErrorReferenceIsDeclared(scenario, errorName) = scenario.contractKind != \"command\" or sliceCommandDefinitions.select(command => command.name == scenario.coveredDefinition and command.errors.select(error => error.name == errorName).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "def scenarioErrorReferencesAreDeclaredForScenario(scenario) = scenario.errorReferences.select(errorName => scenarioErrorReferenceIsDeclared(scenario, errorName)).length() == scenario.errorReferences.length()"
        ));
        assert!(quint.contains(
            "val scenarioErrorReferencesAreDeclared = sliceContractScenarios.select(scenario => scenarioErrorReferencesAreDeclaredForScenario(scenario)).length() == sliceContractScenarios.length()"
        ));
        assert!(quint.contains(
            "def singletonCommandDeclaresRepeatBehavior(command) = not(command.singleton) or allowedSingletonRepeatBehaviors.select(repeatBehavior => repeatBehavior == command.repeatBehavior).length() > 0"
        ));
        assert!(quint.contains(
            "val singletonCommandsDeclareRepeatBehavior = sliceCommandDefinitions.select(command => singletonCommandDeclaresRepeatBehavior(command)).length() == sliceCommandDefinitions.length()"
        ));
    }

    fn assert_slice_automation_invariants(quint: &str) {
        assert!(quint.contains(
            "def automationHasTrigger(automation) = automation.name != \"\" and automation.triggerName != \"\" and automation.reactionDescription != \"\""
        ));
        assert!(quint.contains(
            "def automationIssuesKnownCommand(automation) = sliceCommandNames.select(commandName => commandName == automation.commandName).length() > 0 or sliceReferencedCommandNames.select(commandName => commandName == automation.commandName).length() > 0 or sliceCommandDefinitions.select(command => command.name == automation.commandName).length() > 0"
        ));
        assert!(quint.contains(
            "def automationHandlesCommandErrors(automation, command) = command.name != automation.commandName or command.errors.select(error => automation.handledErrors.select(handledError => handledError == error.name).length() > 0).length() == command.errors.length()"
        ));
        assert!(quint.contains(
            "val automationSlicesDeclareTriggers = sliceKind != SliceAutomation or (sliceAutomations.length() > 0 and sliceAutomations.select(automation => automationHasTrigger(automation)).length() == sliceAutomations.length())"
        ));
        assert!(quint.contains(
            "val automationSlicesRepresentOneReaction = sliceKind != SliceAutomation or sliceAutomations.length() == 1"
        ));
        assert!(quint.contains(
            "val automationsIssueKnownCommands = sliceAutomations.select(automation => automationIssuesKnownCommand(automation)).length() == sliceAutomations.length()"
        ));
        assert!(quint.contains(
            "val automationsHandleCommandErrors = sliceAutomations.select(automation => sliceCommandDefinitions.select(command => automationHandlesCommandErrors(automation, command)).length() == sliceCommandDefinitions.length()).length() == sliceAutomations.length()"
        ));
    }

    fn assert_slice_translation_invariants(quint: &str) {
        assert!(quint.contains(
            "def translationHasExternalContract(translation) = translation.name != \"\" and translation.externalEventName != \"\" and translation.payloadContractName != \"\" and sliceExternalPayloads.select(payload => payload.name == translation.payloadContractName).length() > 0"
        ));
        assert!(quint.contains(
            "def externalBoundaryHasPayloadContractAndFieldProvenance(translation) = translationHasExternalContract(translation) and sliceExternalPayloads.select(payload => payload.name == translation.payloadContractName and payload.fields.length() > 0 and payload.fields.select(payloadField => externalPayloadFieldHasProvenance(payloadField)).length() == payload.fields.length()).length() > 0"
        ));
        assert!(quint.contains(
            "val externalBoundariesHavePayloadContractsAndFieldProvenance = sliceTranslations.select(translation => externalBoundaryHasPayloadContractAndFieldProvenance(translation)).length() == sliceTranslations.length()"
        ));
        assert!(quint.contains(
            "def translationTargetsKnownCommand(translation) = sliceCommandNames.select(commandName => commandName == translation.commandName).length() > 0 or sliceReferencedCommandNames.select(commandName => commandName == translation.commandName).length() > 0 or sliceCommandDefinitions.select(command => command.name == translation.commandName).length() > 0"
        ));
        assert!(quint.contains(
            "def translationReferencesObservedExternalEvent(translation) = sliceEventDefinitions.select(event => event.name == translation.externalEventName and event.observed).length() > 0"
        ));
        assert!(quint.contains(
            "val translationSlicesDeclareExternalContracts = sliceKind != SliceTranslation or (sliceTranslations.length() > 0 and sliceTranslations.select(translation => translationHasExternalContract(translation)).length() == sliceTranslations.length())"
        ));
        assert!(quint.contains(
            "val translationsTargetKnownCommands = sliceTranslations.select(translation => translationTargetsKnownCommand(translation)).length() == sliceTranslations.length()"
        ));
        assert!(quint.contains(
            "val translationsReferenceObservedExternalEvents = sliceTranslations.select(translation => translationReferencesObservedExternalEvent(translation)).length() == sliceTranslations.length()"
        ));
    }

    fn assert_slice_board_element_invariants(quint: &str) {
        assert!(quint.contains(
            "def boardElementLaneMatchesKind(element) = (element.kind == \"view\" and element.lane == \"ux\") or (element.kind == \"automation\" and element.lane == \"ux\") or (element.kind == \"external_event\" and element.lane == \"ux\") or (element.kind == \"command\" and element.lane == \"actions\") or (element.kind == \"read_model\" and element.lane == \"actions\") or (element.kind == \"event\" and element.lane == \"events\")"
        ));
        assert!(quint.contains(
            "def boardElementReferencesDeclaration(element) = (element.kind == \"view\" and (sliceViewNames.select(viewName => viewName == element.declaredName).length() > 0 or sliceViewDefinitions.select(view => view.name == element.declaredName).length() > 0)) or (element.kind == \"automation\" and sliceAutomations.select(automation => automation.name == element.declaredName).length() > 0) or (element.kind == \"external_event\" and sliceEventDefinitions.select(event => event.name == element.declaredName and event.observed).length() > 0) or (element.kind == \"command\" and (sliceCommandNames.select(commandName => commandName == element.declaredName).length() > 0 or sliceReferencedCommandNames.select(commandName => commandName == element.declaredName).length() > 0 or sliceCommandDefinitions.select(command => command.name == element.declaredName).length() > 0)) or (element.kind == \"read_model\" and (sliceReadModelNames.select(readModelName => readModelName == element.declaredName).length() > 0 or sliceReadModelDefinitions.select(readModel => readModel.name == element.declaredName).length() > 0)) or (element.kind == \"event\" and (sliceEventNames.select(eventName => eventName == element.declaredName).length() > 0 or sliceEventDefinitions.select(event => event.name == element.declaredName and (event.observed or event.shared)).length() > 0))"
        ));
        assert!(quint.contains(
            "def automationBoardElementIsDeclaredAutomation(element) = element.kind != \"automation\" or sliceAutomations.select(automation => automation.name == element.declaredName).length() > 0"
        ));
        assert!(quint.contains(
            "val automationBoardElementsAreDeclaredAutomations = sliceBoardElements.select(element => automationBoardElementIsDeclaredAutomation(element)).length() == sliceBoardElements.length()"
        ));
        assert!(quint.contains(
            "def externalBoardElementIsObservedEvent(element) = element.kind != \"external_event\" or sliceEventDefinitions.select(event => event.name == element.declaredName and event.observed).length() > 0"
        ));
        assert!(quint.contains(
            "val externalBoardElementsAreObservedEvents = sliceBoardElements.select(element => externalBoardElementIsObservedEvent(element)).length() == sliceBoardElements.length()"
        ));
    }

    fn assert_slice_board_connection_invariants(quint: &str) {
        assert!(quint.contains(
            "def boardConnectionHasAllowedShape(connection) = (connection.sourceKind == \"view\" and connection.targetKind == \"command\") or (connection.sourceKind == \"automation\" and connection.targetKind == \"command\") or (connection.sourceKind == \"external_event\" and connection.targetKind == \"command\") or (connection.sourceKind == \"workflow_trigger\" and connection.targetKind == \"command\") or (connection.sourceKind == \"command\" and connection.targetKind == \"event\") or (connection.sourceKind == \"event\" and connection.targetKind == \"read_model\") or (connection.sourceKind == \"read_model\" and connection.targetKind == \"view\")"
        ));
        assert!(quint.contains(
            "def commandEventBoardEdgeMatchesEmission(connection) = connection.sourceKind != \"command\" or connection.targetKind != \"event\" or sliceCommandDefinitions.select(command => command.name == connection.source and commandEmittedEventNames(command).select(eventName => eventName == connection.target).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val commandEventBoardEdgesMatchEmissions = sliceBoardConnections.select(connection => commandEventBoardEdgeMatchesEmission(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "def eventReadModelBoardEdgeMatchesProjection(connection) = connection.sourceKind != \"event\" or connection.targetKind != \"read_model\" or sliceReadModelDefinitions.select(readModel => readModel.name == connection.target and readModel.fields.select(readModelField => readModelField.sourceEvent == connection.source).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val eventReadModelBoardEdgesMatchProjectionSources = sliceBoardConnections.select(connection => eventReadModelBoardEdgeMatchesProjection(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "def externalEventCommandBoardEdgeMatchesTranslation(connection) = connection.sourceKind != \"external_event\" or connection.targetKind != \"command\" or sliceTranslations.select(translation => translation.externalEventName == connection.source and translation.commandName == connection.target).length() > 0"
        ));
        assert!(quint.contains(
            "val externalEventTriggersMatchTranslations = sliceBoardConnections.select(connection => externalEventCommandBoardEdgeMatchesTranslation(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "def externalEventDoesNotUpdateReadModel(connection) = connection.sourceKind != \"event\" or connection.targetKind != \"read_model\" or sliceEventDefinitions.select(event => event.name == connection.source and event.observed).length() == 0"
        ));
        assert!(quint.contains(
            "val externalEventsDoNotUpdateReadModels = sliceBoardConnections.select(connection => externalEventDoesNotUpdateReadModel(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "def viewCommandBoardEdgeMatchesControl(connection) = connection.sourceKind != \"view\" or connection.targetKind != \"command\" or sliceViewDefinitions.select(view => view.name == connection.source and view.controls.select(control => control.commandName == connection.target).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val viewCommandBoardEdgesMatchControls = sliceBoardConnections.select(connection => viewCommandBoardEdgeMatchesControl(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "val boardLanesAreCanonical = canonicalBoardLanes == [\"ux\",\"actions\",\"events\"]"
        ));
        assert!(quint.contains(
            "val boardElementsUseCanonicalLanes = sliceBoardElements.select(element => canonicalBoardLanes.select(lane => lane == element.lane).length() > 0 and boardElementLaneMatchesKind(element)).length() == sliceBoardElements.length()"
        ));
        assert!(quint.contains(
            "val boardElementsReferenceDeclarations = sliceBoardElements.select(element => boardElementReferencesDeclaration(element)).length() == sliceBoardElements.length()"
        ));
        assert!(quint.contains(
            "val boardConnectionsHaveCausalSemantics = sliceBoardConnections.select(connection => boardConnectionHasAllowedShape(connection) and commandEventBoardEdgeMatchesEmission(connection) and eventReadModelBoardEdgeMatchesProjection(connection) and externalEventCommandBoardEdgeMatchesTranslation(connection) and externalEventDoesNotUpdateReadModel(connection) and viewCommandBoardEdgeMatchesControl(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "def readModelViewConnectionHasIncomingEventUpdate(connection) = connection.sourceKind != \"read_model\" or connection.targetKind != \"view\" or sliceBoardConnections.select(incoming => incoming.target == connection.source and incoming.targetKind == \"read_model\" and incoming.sourceKind == \"event\").length() > 0"
        ));
        assert!(quint.contains(
            "val readModelsFeedingViewsHaveIncomingEventUpdates = sliceBoardConnections.select(connection => readModelViewConnectionHasIncomingEventUpdate(connection)).length() == sliceBoardConnections.length()"
        ));
        assert!(quint.contains(
            "val commandsHaveIncomingTriggers = sliceBoardElements.select(element => element.kind != \"command\" or sliceBoardConnections.select(connection => connection.target == element.name and connection.targetKind == \"command\" and (connection.sourceKind == \"view\" or connection.sourceKind == \"automation\" or connection.sourceKind == \"external_event\" or connection.sourceKind == \"workflow_trigger\")).length() > 0).length() == sliceBoardElements.length()"
        ));
        assert!(quint.contains(
            "val mainPathBoardHasNoDisconnectedIslands = sliceBoardElements.select(element => not(element.mainPath) or sliceBoardConnections.select(connection => connection.source == element.name or connection.target == element.name).length() > 0).length() == sliceBoardElements.length()"
        ));
    }

    fn assert_slice_outcome_invariants(quint: &str) {
        assert!(quint.contains(
            "val outcomeLabelsAreUnique = sliceOutcomeDefinitions.select(outcome => sliceOutcomeDefinitions.select(other => other.label == outcome.label).length() == 1).length() == sliceOutcomeDefinitions.length()"
        ));
        assert!(quint.contains(
            "val outcomeEventSetsAreNonEmpty = sliceOutcomeDefinitions.select(outcome => outcome.eventSet.length() > 0).length() == sliceOutcomeDefinitions.length()"
        ));
        assert!(quint.contains(
            "val outcomeEventSetsAreDistinct = sliceOutcomeDefinitions.select(outcome => sliceOutcomeDefinitions.select(other => outcome.label == other.label or not(sameOutcomeEventSet(outcome, other))).length() == sliceOutcomeDefinitions.length()).length() == sliceOutcomeDefinitions.length()"
        ));
        assert!(quint.contains(
            "val outcomeEventsAreKnownToSlice = sliceOutcomeDefinitions.select(outcome => outcome.eventSet.select(eventName => eventIsKnownToSlice(eventName)).length() == outcome.eventSet.length()).length() == sliceOutcomeDefinitions.length()"
        ));
    }

    fn assert_slice_event_invariants(quint: &str) {
        assert!(quint.contains(
            "val eventsReferenceKnownStreams = sliceEventDefinitions.select(event => sliceStreams.select(stream => stream.name == event.stream).length() > 0).length() == sliceEventDefinitions.length()"
        ));
        assert!(quint.contains(
            "def commandEmittedEventIsKnown(eventName) = sliceEventNames.select(eventNameRef => eventNameRef == eventName).length() > 0 or sliceEventDefinitions.select(event => event.name == eventName).length() > 0"
        ));
        assert!(quint.contains(
            "def commandEmittedEventNames(command) = command.emittedEvents.foldl([], (names, eventRef) => names.append(eventRef.name))"
        ));
        assert!(quint.contains(
            "def eventProducedByCommand(event) = event.observed or event.shared or sliceCommandDefinitions.select(command => commandEmittedEventNames(command).select(eventName => eventName == event.name).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val commandEmittedEventsAreKnown = sliceCommandDefinitions.select(command => commandEmittedEventNames(command).select(eventName => commandEmittedEventIsKnown(eventName)).length() == commandEmittedEventNames(command).length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "val locallyEmittedEventsAreProducedByCommands = sliceEventDefinitions.select(event => eventProducedByCommand(event)).length() == sliceEventDefinitions.length()"
        ));
    }

    fn assert_slice_event_attribute_invariants(quint: &str) {
        assert!(quint.contains(
            "val eventAttributesHaveAllowedSources = sliceEventDefinitions.select(event => event.attributes.select(attribute => allowedEventAttributeSourceKinds.select(sourceKind => sourceKind == attribute.sourceKind).length() > 0).length() == event.attributes.length()).length() == sliceEventDefinitions.length()"
        ));
        assert!(quint.contains(
            "val eventAttributesHaveProvenance = sliceEventDefinitions.select(event => event.attributes.select(attribute => attribute.name != \"\" and attribute.sourceKind != \"\" and attribute.sourceName != \"\" and attribute.provenanceDescription != \"\").length() == event.attributes.length()).length() == sliceEventDefinitions.length()"
        ));
        assert!(quint.contains(
            "def externalPayloadFieldHasProvenance(payloadField) = payloadField.name != \"\" and payloadField.provenanceDescription != \"\" and payloadField.bitEncoding != \"\""
        ));
        assert!(quint.contains(
            "val externalPayloadFieldsHaveProvenance = sliceExternalPayloads.select(payload => payload.name != \"\" and payload.fields.select(payloadField => externalPayloadFieldHasProvenance(payloadField)).length() == payload.fields.length()).length() == sliceExternalPayloads.length()"
        ));
        assert!(quint.contains(
            "def externalPayloadFieldHasBitLevelFlow(payload, payloadField) = bitLevelFlowCoversTarget(payload.name, payloadField.name)"
        ));
        assert!(quint.contains(
            "def commandInputReferencesAttributeSource(event, attribute, command) = commandEmittedEventNames(command).select(eventName => eventName == event.name).length() > 0 and command.inputs.select(input => input.name == attribute.sourceName).length() > 0"
        ));
        assert!(quint.contains(
            "def externalPayloadFieldIsDeclared(attribute) = sliceExternalPayloads.select(payload => payload.name == attribute.sourceName and payload.fields.select(payloadField => payloadField.name == attribute.sourceField).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "def eventAttributeSourceIsComplete(event, attribute) = (attribute.sourceKind == \"command_input\" and attribute.sourceName != \"\" and attribute.sourceField != \"\" and sliceCommandDefinitions.select(command => commandInputReferencesAttributeSource(event, attribute, command)).length() > 0) or (attribute.sourceKind == \"external_payload\" and attribute.sourceName != \"\" and attribute.sourceField != \"\" and externalPayloadFieldIsDeclared(attribute)) or (attribute.sourceKind == \"generated\" and attribute.sourceName != \"\" and attribute.generatedSourceKind != \"\") or (attribute.sourceKind == \"session\" and attribute.sourceName != \"\") or (attribute.sourceKind == \"derivation\" and attribute.sourceName != \"\" and attribute.sourceField != \"\")"
        ));
        assert!(quint.contains(
            "def eventAttributeTracesToStoredFactSource(attribute) = storedEventFactSourceKinds.select(sourceKind => sourceKind == attribute.sourceKind).length() > 0"
        ));
        assert!(quint.contains(
            "val eventAttributeSourcesAreComplete = sliceEventDefinitions.select(event => event.attributes.select(attribute => eventAttributeSourceIsComplete(event, attribute)).length() == event.attributes.length()).length() == sliceEventDefinitions.length()"
        ));
        assert!(quint.contains(
            "val storedEventFactsTraceToOriginalSources = sliceEventDefinitions.select(event => event.attributes.select(attribute => eventAttributeTracesToStoredFactSource(attribute)).length() == event.attributes.length()).length() == sliceEventDefinitions.length()"
        ));
        assert!(quint.contains(
            "def eventAttributeHasBitLevelFlow(event, attribute) = bitLevelFlowCoversTarget(event.name, attribute.name)"
        ));
    }

    fn assert_slice_read_model_field_invariants(quint: &str) {
        assert!(quint.contains(
            "val readModelFieldsHaveAllowedSources = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => allowedReadModelFieldSourceKinds.select(sourceKind => sourceKind == readModelField.sourceKind).length() > 0).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "val readModelFieldsHaveProvenance = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelField.name != \"\" and readModelField.sourceKind != \"\" and readModelField.provenanceDescription != \"\").length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "def readModelFieldSourceIsComplete(readModelField) = (readModelField.sourceKind == \"event_attribute\" and readModelField.sourceEvent != \"\" and readModelField.sourceAttribute != \"\") or (readModelField.sourceKind == \"derivation\" and readModelField.derivationRule != \"\" and readModelField.derivationSourceFields.length() > 0) or (readModelField.sourceKind == \"absence_default\" and readModelField.absenceEvent != \"\")"
        ));
        assert!(quint.contains(
            "val readModelFieldSourcesAreComplete = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelFieldSourceIsComplete(readModelField)).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "def eventAttributeIsDeclared(eventName, attributeName) = sliceEventDefinitions.select(event => event.name == eventName and event.attributes.select(attribute => attribute.name == attributeName).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "def readModelFieldEventAttributeSourceResolves(readModelField) = readModelField.sourceKind != \"event_attribute\" or eventAttributeIsDeclared(readModelField.sourceEvent, readModelField.sourceAttribute)"
        ));
        assert!(quint.contains(
            "val readModelFieldEventAttributeSourcesResolve = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelFieldEventAttributeSourceResolves(readModelField)).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "def readModelFieldDerivationScenarioIsCovered(readModelField) = readModelField.sourceKind != \"derivation\" or (readModelField.derivationScenarioName != \"\" and scenarioNameIsModeled(readModelField.derivationScenarioName))"
        ));
        assert!(quint.contains(
            "def readModelFieldAbsenceScenarioIsCovered(readModelField) = readModelField.sourceKind != \"absence_default\" or (readModelField.absenceScenarioName != \"\" and scenarioNameIsModeled(readModelField.absenceScenarioName))"
        ));
        assert!(quint.contains(
            "val derivedReadModelFieldsHaveScenarioCoverage = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelFieldDerivationScenarioIsCovered(readModelField)).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "val absenceReadModelFieldsHaveScenarioCoverage = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelFieldAbsenceScenarioIsCovered(readModelField)).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "def transitiveReadModelHasSemantics(readModel) = not(readModel.transitive) or (readModel.relationshipFields.length() > 0 and readModel.transitiveRule != \"\" and readModel.exampleScenarioName != \"\" and scenarioNameIsModeled(readModel.exampleScenarioName))"
        ));
        assert!(quint.contains(
            "val transitiveReadModelsHaveSemantics = sliceReadModelDefinitions.select(readModel => transitiveReadModelHasSemantics(readModel)).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "def readModelFieldHasBitLevelFlow(readModel, readModelField) = bitLevelFlowCoversTarget(readModel.name, readModelField.name)"
        ));
    }

    fn assert_slice_view_field_invariants(quint: &str) {
        assert!(quint.contains(
            "val viewFieldsHaveAllowedSources = sliceViewDefinitions.select(view => view.fields.select(viewField => allowedViewFieldSourceKinds.select(sourceKind => sourceKind == viewField.sourceKind).length() > 0).length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewFieldsHaveProvenance = sliceViewDefinitions.select(view => view.fields.select(viewField => viewField.name != \"\" and viewField.sourceKind != \"\" and viewField.provenanceDescription != \"\" and viewField.bitEncoding != \"\").length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewFieldSourcesAreComplete = sliceViewDefinitions.select(view => view.fields.select(viewField => viewField.sourceKind == \"read_model\" and viewField.sourceReadModel != \"\" and viewField.sourceField != \"\" and viewField.sketchToken != \"\").length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewFieldsSourceFromUsedReadModels = sliceViewDefinitions.select(view => view.fields.select(viewField => view.readModels.select(readModel => readModel == viewField.sourceReadModel).length() > 0 and sliceReadModelNames.select(readModelName => readModelName == viewField.sourceReadModel).length() > 0).length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def viewFieldAppearsInSketch(view, viewField) = viewField.sketchToken != \"\" and view.sketchTokens.select(sketchToken => sketchToken == viewField.sketchToken).length() > 0"
        ));
        assert!(
            quint.contains("def viewHasInformationSketch(view) = view.sketchTokens.length() > 0")
        );
        assert!(quint.contains(
            "val viewsHaveInformationSketches = sliceViewDefinitions.select(view => viewHasInformationSketch(view)).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewFieldsAppearInSketch = sliceViewDefinitions.select(view => view.fields.select(viewField => viewFieldAppearsInSketch(view, viewField)).length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def sketchTokenMapsToModeledElement(view, token) = view.fields.select(viewField => viewField.sketchToken == token).length() > 0 or view.controls.select(control => control.sketchToken == token or control.inputs.select(input => input.sourceKind == CommandInputActor and input.sketchToken == token).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val viewSketchTokensMapToModeledElements = sliceViewDefinitions.select(view => view.sketchTokens.select(sketchToken => sketchTokenMapsToModeledElement(view, sketchToken)).length() == view.sketchTokens.length()).length() == sliceViewDefinitions.length()"
        ));
    }

    fn assert_slice_view_provenance_invariants(quint: &str) {
        assert!(quint.contains(
            "def readModelFieldIsDeclared(readModelName, fieldName) = sliceReadModelDefinitions.select(readModel => readModel.name == readModelName and readModel.fields.select(readModelField => readModelField.name == fieldName).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "def viewFieldSourceReadModelFieldResolves(viewField) = viewField.sourceKind != \"read_model\" or readModelFieldIsDeclared(viewField.sourceReadModel, viewField.sourceField)"
        ));
        assert!(quint.contains(
            "def readModelFieldHasOriginalProvenance(readModelField) = (readModelField.sourceKind == \"event_attribute\" and readModelFieldEventAttributeSourceResolves(readModelField)) or readModelField.sourceKind == \"derivation\" or readModelField.sourceKind == \"absence_default\""
        ));
        assert!(quint.contains(
            "def viewFieldTracesToOriginalProvenance(viewField) = viewField.sourceKind == \"read_model\" and sliceReadModelDefinitions.select(readModel => readModel.name == viewField.sourceReadModel and readModel.fields.select(readModelField => readModelField.name == viewField.sourceField and readModelFieldHasOriginalProvenance(readModelField)).length() > 0).length() > 0"
        ));
        assert!(quint.contains(
            "val viewFieldReadModelFieldSourcesResolve = sliceViewDefinitions.select(view => view.fields.select(viewField => viewFieldSourceReadModelFieldResolves(viewField)).length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val displayedDataTraceToOriginalProvenance = sliceViewDefinitions.select(view => view.fields.select(viewField => viewFieldTracesToOriginalProvenance(viewField)).length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
    }

    fn assert_slice_data_flow_invariants(quint: &str) {
        assert!(quint.contains(
            "def viewFieldHasBitLevelFlow(view, viewField) = bitLevelFlowCoversTarget(view.name, viewField.name)"
        ));
        assert!(quint.contains(
            "val commandInputDataFlowsAreComplete = sliceCommandDefinitions.select(command => command.inputs.select(input => commandInputHasBitLevelFlow(command, input)).length() == command.inputs.length()).length() == sliceCommandDefinitions.length()"
        ));
        assert!(quint.contains(
            "val eventAttributeDataFlowsAreComplete = sliceEventDefinitions.select(event => event.attributes.select(attribute => eventAttributeHasBitLevelFlow(event, attribute)).length() == event.attributes.length()).length() == sliceEventDefinitions.length()"
        ));
        assert!(quint.contains(
            "val readModelFieldDataFlowsAreComplete = sliceReadModelDefinitions.select(readModel => readModel.fields.select(readModelField => readModelFieldHasBitLevelFlow(readModel, readModelField)).length() == readModel.fields.length()).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewFieldDataFlowsAreComplete = sliceViewDefinitions.select(view => view.fields.select(viewField => viewFieldHasBitLevelFlow(view, viewField)).length() == view.fields.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val externalPayloadFieldDataFlowsAreComplete = sliceExternalPayloads.select(payload => payload.fields.select(payloadField => externalPayloadFieldHasBitLevelFlow(payload, payloadField)).length() == payload.fields.length()).length() == sliceExternalPayloads.length()"
        ));
        assert!(quint.contains(
            "val modeledDataFlowsAreBitComplete = commandInputDataFlowsAreComplete and eventAttributeDataFlowsAreComplete and readModelFieldDataFlowsAreComplete and viewFieldDataFlowsAreComplete and externalPayloadFieldDataFlowsAreComplete"
        ));
    }

    fn assert_slice_view_control_invariants(quint: &str) {
        assert!(quint.contains(
            "val viewControlsHaveSketchTokens = sliceViewDefinitions.select(view => view.controls.select(control => control.name != \"\" and control.commandName != \"\" and control.sketchToken != \"\").length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def controlAppearsInSketch(view, control) = control.sketchToken != \"\" and view.sketchTokens.select(sketchToken => sketchToken == control.sketchToken).length() > 0"
        ));
        assert!(quint.contains(
            "val viewControlsAppearInSketch = sliceViewDefinitions.select(view => view.controls.select(control => controlAppearsInSketch(view, control)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlsReferenceKnownCommands = sliceViewDefinitions.select(view => view.controls.select(control => sliceCommandNames.select(commandName => commandName == control.commandName).length() > 0 or sliceReferencedCommandNames.select(commandName => commandName == control.commandName).length() > 0 or sliceCommandDefinitions.select(command => command.name == control.commandName).length() > 0).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def controlProvidesCommandInput(control, input) = control.inputs.select(providedInput => providedInput.name == input.name).length() > 0"
        ));
        assert!(quint.contains(
            "def controlProvidesEveryCommandInput(control, command) = command.name != control.commandName or command.inputs.select(input => controlProvidesCommandInput(control, input)).length() == command.inputs.length()"
        ));
        assert!(quint.contains(
            "val viewControlsProvideCommandInputs = sliceViewDefinitions.select(view => view.controls.select(control => sliceCommandDefinitions.select(command => controlProvidesEveryCommandInput(control, command)).length() == sliceCommandDefinitions.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlInputsHaveAllowedSources = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => allowedControlInputSourceKinds.select(sourceKind => sourceKind == input.sourceKind).length() > 0).length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlInputsHaveProvenance = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => input.name != \"\" and input.sourceDescription != \"\").length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(
            quint.contains(
                "def controlInputHasDescription(input) = input.sourceDescription != \"\""
            )
        );
        assert!(quint.contains(
            "val viewControlInputsHaveDescriptions = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => controlInputHasDescription(input)).length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def controlInputSessionInputHasDescription(input) = input.sourceKind != CommandInputSession or input.sourceDescription != \"\""
        ));
        assert!(quint.contains(
            "val viewControlSessionInputsHaveDescriptions = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => controlInputSessionInputHasDescription(input)).length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlInputVisibilityIsModeled = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => (input.sourceKind != CommandInputActor or input.sketchToken != \"\" or input.visibleToActor) and (not(input.decisionField) or input.sketchToken != \"\" or input.visibleToActor)).length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def controlInputDecisionFieldIsVisible(input) = not(input.decisionField) or input.sketchToken != \"\" or input.visibleToActor"
        ));
        assert!(quint.contains(
            "val viewControlDecisionFieldsAreVisible = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => controlInputDecisionFieldIsVisible(input)).length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def controlInputActorInputIsVisible(input) = input.sourceKind != CommandInputActor or input.sketchToken != \"\" or input.visibleToActor"
        ));
        assert!(quint.contains(
            "val viewControlActorInputsAreVisible = sliceViewDefinitions.select(view => view.controls.select(control => control.inputs.select(input => controlInputActorInputIsVisible(input)).length() == control.inputs.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlsHandleCommandErrors = sliceViewDefinitions.select(view => view.controls.select(control => sliceCommandDefinitions.select(command => command.name != control.commandName or command.errors.select(error => control.handledErrors.select(handledError => handledError == error.name).length() > 0 and control.recoveryBehavior != \"\").length() == command.errors.length()).length() == sliceCommandDefinitions.length()).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "def controlRecoveryBehaviorIsModeled(control) = control.handledErrors.length() == 0 or allowedRecoveryKinds.select(recoveryKind => recoveryKind == control.recoveryBehavior).length() > 0"
        ));
        assert!(quint.contains(
            "val viewControlRecoveryBehaviorIsModeled = sliceViewDefinitions.select(view => view.controls.select(control => controlRecoveryBehaviorIsModeled(control)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
    }

    fn assert_slice_kind_ownership_invariants(quint: &str) {
        assert!(quint.contains(
            "val stateViewSlicesDoNotOwnCommands = sliceKind != SliceStateView or (sliceCommands.length() == 0 and sliceCommandDefinitions.length() == 0)"
        ));
        assert!(quint.contains(
            "val stateViewSlicesOwnViews = sliceKind != SliceStateView or (sliceViews.length() > 0 or sliceViewDefinitions.length() > 0)"
        ));
        assert!(quint.contains(
            "val stateViewSlicesOwnReadModels = sliceKind != SliceStateView or (sliceReadModels.length() > 0 or sliceReadModelDefinitions.length() > 0)"
        ));
        assert!(quint.contains(
            "def readModelOwnsProjectionPath(readModel) = readModel.fields.length() > 0 and readModel.fields.select(readModelField => readModelFieldSourceIsComplete(readModelField)).length() == readModel.fields.length()"
        ));
        assert!(quint.contains(
            "val stateViewSlicesOwnProjectionPaths = sliceKind != SliceStateView or sliceReadModelDefinitions.select(readModel => readModelOwnsProjectionPath(readModel)).length() == sliceReadModelDefinitions.length()"
        ));
        assert!(quint.contains(
            "val stateViewSlicesRepresentSingleViewProjectionBoundary = sliceKind != SliceStateView or (sliceViewDefinitions.length() == 1 and sliceReadModelDefinitions.length() > 0)"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesOwnCommands = sliceKind != SliceStateChange or (sliceCommands.length() > 0 or sliceCommandDefinitions.length() > 0)"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesOwnEvents = sliceKind != SliceStateChange or (sliceEvents.length() > 0 or sliceEventDefinitions.length() > 0)"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesOwnOutcomes = sliceKind != SliceStateChange or sliceOutcomeDefinitions.length() > 0"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesOwnErrors = sliceKind != SliceStateChange or commandErrorsAreDeclared"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesDoNotOwnReadModelsOrViews = sliceKind != SliceStateChange or (sliceReadModels.length() == 0 and sliceReadModelDefinitions.length() == 0 and sliceViews.length() == 0 and sliceViewDefinitions.length() == 0)"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesDoNotOwnAutomationsOrTranslations = sliceKind != SliceStateChange or (sliceAutomations.length() == 0 and sliceTranslations.length() == 0)"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesDoNotOwnControlsOrSketches = sliceKind != SliceStateChange or sliceViewDefinitions.select(view => view.controls.length() == 0 and view.sketchTokens.length() == 0).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val translationSlicesDoNotOwnViews = sliceKind != SliceTranslation or (sliceViews.length() == 0 and sliceViewDefinitions.length() == 0)"
        ));
    }

    fn assert_slice_coherence_invariants(quint: &str) {
        assert!(quint.contains("val recognizedSliceKind = true"));
        assert!(quint.contains(
            "val sliceRepresentsOneCoherentModelUnit = recognizedSliceKind and stateViewSlicesDoNotOwnCommands and stateViewSlicesOwnViews and stateViewSlicesOwnReadModels and stateViewSlicesOwnProjectionPaths and stateChangeSlicesOwnCommands and stateChangeSlicesOwnEvents and stateChangeSlicesOwnOutcomes and stateChangeSlicesOwnErrors and stateChangeSlicesDoNotOwnReadModelsOrViews and stateChangeSlicesDoNotOwnAutomationsOrTranslations and stateChangeSlicesDoNotOwnControlsOrSketches and translationSlicesDeclareExternalContracts and externalBoundariesHavePayloadContractsAndFieldProvenance and translationsTargetKnownCommands and translationsReferenceObservedExternalEvents and translationSlicesDoNotOwnViews and automationSlicesDeclareTriggers and automationSlicesRepresentOneReaction and automationsIssueKnownCommands and automationsHandleCommandErrors"
        ));
        assert!(quint.contains(
            "val stateChangeSlicesRepresentSingleCommandBoundary = sliceKind != SliceStateChange or sliceCommandDefinitions.length() == 1"
        ));
        assert!(quint.contains(
            "val sliceRepresentsSmallestUsefulBehaviorBoundary = sliceRepresentsOneCoherentModelUnit and stateViewSlicesRepresentSingleViewProjectionBoundary and stateChangeSlicesRepresentSingleCommandBoundary and automationSlicesRepresentOneReaction and translationSlicesDeclareExternalContracts"
        ));
    }

    fn assert_slice_navigation_invariants(quint: &str) {
        assert!(quint.contains(
            "def navigationTargetTypeIsModeled(target) = target.targetType == \"\" or allowedNavigationTargetTypes.select(targetType => targetType == target.targetType).length() > 0"
        ));
        assert!(quint.contains(
            "def navigationTargetHasPayload(target) = target.targetName != \"\" or target.externalWorkflowName != \"\" or target.externalSystemName != \"\" or target.handoffContract != \"\""
        ));
        assert!(quint.contains(
            "def navigationControlDeclaresType(target) = not(navigationTargetHasPayload(target)) or target.targetType != \"\""
        ));
        assert!(quint.contains(
            "def navigationModeledViewTargetsExistingView(target) = target.targetType != \"modeled_view\" or (target.targetName != \"\" and sliceViewNames.select(viewName => viewName == target.targetName).length() > 0)"
        ));
        assert!(quint.contains(
            "def localViewStateNavigationTargetResolves(view, target) = target.targetType != \"local_view_state\" or (target.targetName != \"\" and (view.localStates.select(localState => localState == target.targetName).length() > 0 or view.filters.select(viewFilter => viewFilter == target.targetName).length() > 0))"
        ));
        assert!(quint.contains(
            "def navigationExternalWorkflowTargetsNamed(target) = target.targetType != \"external_workflow\" or target.externalWorkflowName != \"\""
        ));
        assert!(quint.contains(
            "def navigationExternalSystemTargetsHaveContracts(target) = target.targetType != \"external_system\" or (target.externalSystemName != \"\" and target.handoffContract != \"\")"
        ));
        assert!(quint.contains(
            "def navigationTargetIsComplete(view, target) = (target.targetType == \"\" and target.targetName == \"\" and target.externalWorkflowName == \"\" and target.externalSystemName == \"\" and target.handoffContract == \"\") or (target.targetType == \"modeled_view\" and target.targetName != \"\" and sliceViewNames.select(viewName => viewName == target.targetName).length() > 0) or (target.targetType == \"local_view_state\" and localViewStateNavigationTargetResolves(view, target)) or (target.targetType == \"external_workflow\" and navigationExternalWorkflowTargetsNamed(target)) or (target.targetType == \"external_system\" and navigationExternalSystemTargetsHaveContracts(target))"
        ));
        assert!(quint.contains(
            "val viewControlNavigationTypesAreModeled = sliceViewDefinitions.select(view => view.controls.select(control => navigationTargetTypeIsModeled(control.navigation)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlNavigationTypesAreDeclared = sliceViewDefinitions.select(view => view.controls.select(control => navigationControlDeclaresType(control.navigation)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlModeledViewNavigationTargetsResolve = sliceViewDefinitions.select(view => view.controls.select(control => navigationModeledViewTargetsExistingView(control.navigation)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlExternalWorkflowNavigationTargetsNamed = sliceViewDefinitions.select(view => view.controls.select(control => navigationExternalWorkflowTargetsNamed(control.navigation)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlExternalSystemNavigationTargetsHaveContracts = sliceViewDefinitions.select(view => view.controls.select(control => navigationExternalSystemTargetsHaveContracts(control.navigation)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
        assert!(quint.contains(
            "val viewControlNavigationTargetsAreComplete = sliceViewDefinitions.select(view => view.controls.select(control => navigationTargetIsComplete(view, control.navigation)).length() == view.controls.length()).length() == sliceViewDefinitions.length()"
        ));
    }

    fn assert_slice_identity_and_model_state(quint: &str) {
        assert!(quint.contains("val sliceIdentityStable = sliceName == \"Capture ticket\""));
        assert!(
            quint.contains(
                "val sliceHasLocallyEmittedEvent = sliceEvents.length() > 0 or sliceEventDefinitions.select(event => not(event.observed) and not(event.shared)).length() > 0"
            ),
            "Quint slice artifacts must count locally emitted formal event definitions"
        );
        assert!(
            quint.contains(
                "val sliceStateChangeRequiresEvent = sliceKind != SliceStateChange or sliceHasLocallyEmittedEvent"
            ),
            "Quint slice artifacts must expose the state-change event obligation"
        );
        assert!(
            quint.contains(
                "val sliceBitLevelDataFlowsStructured = sliceBitLevelDataFlows.select(flow => flow.datum != \"\" and flow.sourceKind != \"\" and flow.source != \"\" and flow.transformationSemantics != \"\" and flow.target != \"\" and flow.bitEncoding != \"\").length() == sliceBitLevelDataFlows.length()"
            ),
            "Quint slice artifacts must verify represented data-flow rows include source, transformation/projection, target, and bit encoding fields"
        );
        assert!(
            quint.contains(
                "val modeledDataFlowsAreBitComplete = commandInputDataFlowsAreComplete and eventAttributeDataFlowsAreComplete and readModelFieldDataFlowsAreComplete and viewFieldDataFlowsAreComplete and externalPayloadFieldDataFlowsAreComplete"
            ),
            "Quint slice artifacts must verify modeled data has bit-level flow coverage"
        );
        assert!(quint.contains("var modelState: int"));
        assert!(quint.contains("action init = modelState' = 0"));
        assert!(quint.contains("action step = modelState' = modelState"));
    }
}
