/*
 * Copyright (C) 2026 HCALC / Foundry J contributors
 * SPDX-License-Identifier: AGPL-3.0-only
 *
 * Module: Evolve — production Ξ + InstanceBridge ShapeMap (NOT Foundry39≡nested).
 * Cite: PRODUCTION.md §5 Gap-Ξ, §6 Gap-ShapeMap / L7 CLOSED (InstanceBridge).
 * Ξ(t,y)=ξ_t·y+g_t; Uniform ξ_t=1.
 * bridgeMode = InstanceBridge; NestedFaithful/FoundryAdditive stay DISTINCT from identity.
 * Provenance: SpecDefined
 */

module modules/Evolve

open modules/State
open modules/PrimeIndex
open modules/Transform
open modules/Stabilize
open modules/Contract
open modules/Recursion

/* ---- Production Ξ: ξ_t·y + g_t, Uniform ξ=1 ----
 * Provenance: SpecDefined — PRODUCTION.md §5. */
abstract sig XiScheduleKind {}
one sig UniformXi extends XiScheduleKind {}

one sig XiSchedule {
  kind: one XiScheduleKind,
  /* xiIsOne=1 encodes Uniform ξ_t = 1 for all t */
  xiIsOne: Int
}

sig Kick {
  /* g_t affine kick (default zero vector — presence optional) */
  target: lone State
}

sig Intermediate {
  fromState: one State,
  viaTp: lone TpMap,
  viaC: lone COp,
  viaLambda: lone Scalar
}

/* HCALC Ξ(t, ·) — affine Uniform; NOT Foundry Ξ_t schedule weights. */
sig HCALC_Xi {
  atTime: one Time,
  map: Intermediate -> lone State,
  /* isAffine=1 encodes Ξ(t,y)=ξ_t·y+g_t */
  isAffine: Int,
  schedule: one XiScheduleKind
}

fact fact_P5_xi_uniform_affine {
  XiSchedule.kind = UniformXi
  XiSchedule.xiIsOne = 1
  all xi: HCALC_Xi |
    xi.isAffine = 1 and xi.schedule = UniformXi
}

pred xi_uniform_affine_ok {
  XiSchedule.kind = UniformXi
  XiSchedule.xiIsOne = 1
  all xi: HCALC_Xi |
    xi.isAffine = 1 and xi.schedule = UniformXi
}

assert P5_xi_uniform_affine {
  /* Production assert P5 — Ξ affine with Uniform ξ=1 */
  xi_uniform_affine_ok
}

/* Foundry schedule weights — distinct sigs from HCALC_Xi / LambdaM. */
sig FoundryXiWeights {
  schedule: one ScheduleVector
}

sig FoundryLambdaWeights {
  schedule: one ScheduleVector
}

sig FoundryT {
  apply: State -> lone State
}

sig FoundryG {
  kick: lone State
}

/* Foundry additive Step (prop 39) — diagnostic / Foundry instance only. */
pred foundry_additive_step[x: State, xNext: State] {
  some xi: FoundryXiWeights, lam: FoundryLambdaWeights, tn: FoundryT |
    some xi.schedule and some lam.schedule and
    (xNext in x.(tn.apply) or (some g: FoundryG | xNext = g.kick) or xNext = x)
}

/* HCALC nested: X' = Ξ(t, Λm · C[T_p(X)]) */
pred hcalc_nested_step[t: Time, X: State, XNext: State] {
  some xi: HCALC_Xi, tp: TpMap, c: COp, mid: Intermediate |
    xi.atTime = t and
    xi.isAffine = 1 and
    mid.fromState = X and
    mid.viaTp = tp and
    mid.viaC = c and
    mid.viaLambda = LambdaM.scalar and
    XNext in mid.(xi.map)
}

pred evolve_next[t: Time] {
  some t.next implies (
    (ActiveInstance.kind = HCALCInstance implies
      hcalc_nested_step[t, t.at, t.next.at])
    and
    (ActiveInstance.kind = FoundryInstance implies
      foundry_additive_step[t.at, t.next.at])
  )
}

fact INV_evolve_respects_active_instance {
  all t: Time | evolve_next[t]
}

/* A4 — Foundry additive ONLY when instance = Foundry; not equated to HCALC nested. */
pred A4_foundry_step_only_if_foundry_instance {
  ActiveInstance.kind = FoundryInstance or ActiveInstance.kind = HCALCInstance
  ActiveInstance.kind = FoundryInstance implies
    (all t: Time | some t.next implies foundry_additive_step[t.at, t.next.at])
  ActiveInstance.kind = HCALCInstance implies
    (all t: Time | some t.next implies hcalc_nested_step[t, t.at, t.next.at])
}

assert A4_foundry_additive_only_if_Foundry_instance {
  /* Sealed assert id A4 — PROPERTY_MAP */
  A4_foundry_step_only_if_foundry_instance
}

/* ---- ShapeMap / L7: InstanceBridge morphism (NOT identity / NOT Foundry39≡nested) ----
 * Provenance: SpecDefined — PRODUCTION.md §6.
 * NestedFaithful / FoundryAdditive remain DISTINCT modes — never identity claims. */
abstract sig BridgeMode {}
one sig InstanceBridge, NestedFaithful, FoundryAdditive extends BridgeMode {}

/* Explicit morphism table under InstanceBridge (Option B production). */
one sig InstanceBridgeTable {
  /* Parameter assignments (flags=1) — NOT symbol identities */
  T_assigned_C_circ_Tp: Int,
  Lambda_scalar_broadcast: Int,
  Xi_from_hcalc_schedule: Int,
  g_instance_param: Int,
  /* claimsIdentity MUST stay 0 — forbid Foundry39 ≡ nested */
  claimsIdentity: Int
}

one sig ShapeMapConfig {
  bridgeMode: one BridgeMode
}

fact fact_P6_instance_bridge_morphism {
  ShapeMapConfig.bridgeMode = InstanceBridge
  InstanceBridgeTable.T_assigned_C_circ_Tp = 1
  InstanceBridgeTable.Lambda_scalar_broadcast = 1
  InstanceBridgeTable.Xi_from_hcalc_schedule = 1
  InstanceBridgeTable.g_instance_param = 1
  InstanceBridgeTable.claimsIdentity = 0
}

pred instance_bridge_morphism_ok {
  ShapeMapConfig.bridgeMode = InstanceBridge
  InstanceBridgeTable.T_assigned_C_circ_Tp = 1
  InstanceBridgeTable.Lambda_scalar_broadcast = 1
  InstanceBridgeTable.Xi_from_hcalc_schedule = 1
  InstanceBridgeTable.g_instance_param = 1
  InstanceBridgeTable.claimsIdentity = 0
}

assert P6_instance_bridge_morphism {
  /* Production assert P6 — bridgeMode=InstanceBridge; forbid identity */
  instance_bridge_morphism_ok
}

/* INV: bridge is InstanceBridge morphism, never silent identity. */
pred bridge_instance_not_identity {
  ShapeMapConfig.bridgeMode = InstanceBridge
  InstanceBridgeTable.claimsIdentity = 0
}

fact fact_bridge_production {
  bridge_instance_not_identity
}

assert INV_step_shape_bridge_instance {
  /* INV_step_shape_bridge_instance — production InstanceBridge (not axiom-gap) */
  bridge_instance_not_identity
}

assert INV_evolve_total_State_reachable {
  evolution_total_on_State
}