extraction: apply allowlisted-divergence transformations to signer scripts

Per extraction plan v38 §4.4, allowlisted-divergence files require
content normalization for the canonical context. This commit applies
the transformations declared in the source manifest for the 2 signer-
side allowlisted-divergence entries.

Transformations
- pkg/tbtc/signer/scripts/formal/check_roast_attempt_context_vectors.mjs:
  Rewrite vector path from
    `docs/frost-migration/test-vectors/roast-attempt-context-v1.json`
  to canonical signer layout
    `test/vectors/roast-attempt-context-v1.json`
  (both relative to rootDir which is two levels up from the script
  location; in canonical context that's pkg/tbtc/signer/)

- pkg/tbtc/signer/scripts/formal/run_tla_models.sh:
  Rewrite MODEL_DIR default from
    `$ROOT_DIR/docs/frost-migration/formal-verification/models`
  to canonical signer layout
    `$ROOT_DIR/docs/formal/models`
  Plus MODELS_PATH env-var override for alternate environments (CI
  matrices, local dev trees). ROOT_DIR is unchanged
  (`$(dirname $BASH_SOURCE)/../..` resolves to pkg/tbtc/signer/ here).

Verification
- Both files retain identical behavior to their monorepo counterparts
  when invoked from canonical signer layout
- Comments added documenting the path normalization with reference back
  to the source manifest's allowlisted-divergence status

Recompute expectedTargetSha256 for both entries in the source manifest
and collect dual signoff before merge per plan v38 §4.2.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: mswilkison

pkg/tbtc/signer/scripts/formal/check_roast_attempt_context_vectors.mjs

@@ -12,9 +12,15 @@ const VECTOR_SCHEMA_VERSION = "roast-attempt-context-v1"
 
 const scriptDir = path.dirname(fileURLToPath(import.meta.url))
 const rootDir = path.resolve(scriptDir, "../..")
+// Path normalization (allowlisted-divergence per source manifest):
+// canonical signer layout places the ROAST attempt context vector at
+// `<rootDir>/test/vectors/roast-attempt-context-v1.json` where rootDir
+// is `pkg/tbtc/signer/`. Monorepo source path was
+// `docs/frost-migration/test-vectors/roast-attempt-context-v1.json`
+// relative to monorepo root.
 const vectorsPath = path.join(
   rootDir,
-  "docs/frost-migration/test-vectors/roast-attempt-context-v1.json"
+  "test/vectors/roast-attempt-context-v1.json"
 )
 
 const fail = (message) => {

pkg/tbtc/signer/scripts/formal/run_tla_models.sh

@@ -2,7 +2,13 @@
 set -euo pipefail
 
 ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
-MODEL_DIR="$ROOT_DIR/docs/frost-migration/formal-verification/models"
+# Path normalization (allowlisted-divergence per source manifest):
+# canonical signer layout places TLA+ models at
+# `<ROOT_DIR>/docs/formal/models` (where ROOT_DIR = pkg/tbtc/signer/).
+# Monorepo source path was `docs/frost-migration/formal-verification/models`
+# relative to monorepo root. Override via MODELS_PATH env var for
+# alternate environments.
+MODEL_DIR="${MODELS_PATH:-$ROOT_DIR/docs/formal/models}"
 TLA_TOOLS_VERSION="${TLA_TOOLS_VERSION:-v1.8.0}"
 TLA_TOOLS_JAR="${TLA_TOOLS_JAR:-/tmp/tla2tools-${TLA_TOOLS_VERSION}.jar}"
 TLA_TOOLS_URL="${TLA_TOOLS_URL:-https://github.com/tlaplus/tlaplus/releases/download/${TLA_TOOLS_VERSION}/tla2tools.jar}"