alloy/modules/Recursion.als

/*
 * Copyright (C) 2026 HCALC / Foundry J contributors
 * SPDX-License-Identifier: AGPL-3.0-only
 *
 * Module: Recursion — prime-indexed recursion (bounded, not unrestricted).
 * Cite: FOUNDRY_J_CROSSLINKS.md §0; HCALC pipeline.
 * GapId: Gap-Tp-from-P64 (COHERENCE.md)
 * Core witnesses (intent): rec_step, P64.
 */

module modules/Recursion

open modules/State
open modules/PrimeIndex
open modules/Transform

pred recurse_via_Tp[t: Time, tp: TpMap, sNext: State] {
  tp.index in P64Carrier.primes
  sNext in (t.at).(tp.apply)
}

/* Assert id: INV_bounded_recursion_depth */
fact INV_bounded_recursion_depth {
  all t: Time | lone t.next
}

assert INV_recursion_uses_prime_index {
  /* INV_recursion_uses_prime_index */
  all tp: TpMap | tp.index in P64Carrier.primes or
    (some e: PrimeExtension | tp.index in e.extra)
}