ltl-accumulator-verified/verification/fidelity/pacta_pin.py

#!/usr/bin/env python3
"""Pin the pacta sources the fidelity harness actually consumes.

    pacta_pin.py --write    # regenerate PACTA-PIN.sha256 (deliberate act)
    pacta_pin.py --verify   # check the subject; exit 1 on any drift

─────────────────────────────────────────────────────────────────────────────
WHY THIS EXISTS — round-8 review (GPT-5.6, register key `pacta-subject-unpinned`)

Phase 4 compares this repository's Lean definitions against the DEPLOYED
verifier. It did so by putting `$PACTA_SRC` on `sys.path` and importing
`pacta.transparency` — whatever happened to be there. No repository URL, no
commit, no clean-state check, no source hashes.

So the fidelity counts pinned OUTPUTS while the SUBJECT was unpinned. Any
implementation producing the same finite family of answers passed, and the
recorded result named no version of the thing it agreed with. The reviewer's
zero-divergence run was specifically against pacta `cd3b1bc…` — because the
reviewer selected and recorded that checkout, not because the button required
it.

A proof about a model is not evidence about an unnamed program.

WHAT IS PINNED, AND WHY IT IS NOT A GLOB. The pin covers the transitive set of
pacta modules the harness ACTUALLY LOADS, discovered by importing the harness's
entry point and reading `sys.modules` — a membership property, not a directory
listing. Globbing `pacta/*.py` would pin files the comparison never touches
(noise that breaks the pin for unrelated edits) and would miss anything loaded
from outside that directory. The estate has been bitten by name-shaped
measurement before; this is the same error class.

WHAT THIS DOES NOT ESTABLISH. Byte identity of a source tree is not proof that
the deployed service runs it, and finite-family agreement is not extensional
equality. This pin names the subject; it does not widen the claim.
─────────────────────────────────────────────────────────────────────────────
"""
import hashlib
import os
import subprocess
import sys

HERE = os.path.dirname(os.path.abspath(__file__))
VERIF = os.path.dirname(HERE)
PIN = os.path.join(VERIF, 'PACTA-PIN.sha256')
PACTA_SRC = os.environ.get(
    'PACTA_SRC', os.path.join(VERIF, '..', '..',
                              'proof-aware-crypto-tooling-agent', 'src'))
PACTA_SRC = os.path.abspath(PACTA_SRC)


def loaded_sources():
    """{path relative to PACTA_SRC: sha256} for every pacta module imported.

    Imports the same entry point the fidelity harness does, then keeps the
    modules whose file lives under PACTA_SRC. That is the consumed set by
    construction: if the harness stops using a module, it leaves the pin; if it
    starts using one, the pin fails until someone regenerates it deliberately.
    """
    sys.path.insert(0, PACTA_SRC)
    try:
        import pacta.transparency  # noqa: F401
    except Exception as e:                                   # pragma: no cover
        print(f'PACTA PIN: cannot import pacta.transparency from {PACTA_SRC}:'
              f' {e}', file=sys.stderr)
        raise SystemExit(1)

    out = {}
    for mod in list(sys.modules.values()):
        f = getattr(mod, '__file__', None)
        if not f:
            continue
        f = os.path.abspath(f)
        if not f.startswith(PACTA_SRC + os.sep) or not f.endswith('.py'):
            continue
        with open(f, 'rb') as fh:
            out[os.path.relpath(f, PACTA_SRC)] = hashlib.sha256(
                fh.read()).hexdigest()
    return out


def head_commit():
    """The pacta commit, for the record. NOT the enforcement — hashes are."""
    try:
        r = subprocess.run(['git', '-C', PACTA_SRC, 'rev-parse', 'HEAD'],
                           capture_output=True, text=True, timeout=10)
        c = r.stdout.strip() if r.returncode == 0 else 'unknown'
        d = subprocess.run(['git', '-C', PACTA_SRC, 'status', '--porcelain'],
                           capture_output=True, text=True, timeout=10)
        dirty = bool(d.stdout.strip()) if d.returncode == 0 else True
        return c, dirty
    except Exception:                                        # pragma: no cover
        return 'unknown', True


def write():
    got = loaded_sources()
    commit, dirty = head_commit()
    if dirty:
        print('PACTA PIN: refusing to pin a DIRTY pacta working tree.'
              ' Commit or stash first — a pin taken over uncommitted edits'
              ' names a subject nobody else can obtain.', file=sys.stderr)
        raise SystemExit(1)
    with open(PIN, 'w', encoding='utf-8') as fh:
        fh.write(f'# pacta subject pinned by fidelity/pacta_pin.py --write\n')
        fh.write(f'# commit {commit}\n')
        fh.write(f'# {len(got)} module(s), discovered by import, not by glob\n')
        for rel in sorted(got):
            fh.write(f'{got[rel]}  {rel}\n')
    print(f'PACTA PIN: wrote {len(got)} module(s) at commit {commit[:7]}')


def verify():
    if not os.path.exists(PIN):
        print('PACTA PIN: PACTA-PIN.sha256 is missing — the fidelity subject'
              ' is unpinned. Refusing to certify agreement with an unnamed'
              ' program.', file=sys.stderr)
        return 1
    want = {}
    commit = 'unknown'
    for line in open(PIN, encoding='utf-8'):
        if line.startswith('# commit '):
            commit = line.split()[2]
        if line.startswith('#') or not line.strip():
            continue
        h, rel = line.rstrip('\n').split('  ', 1)
        want[rel] = h
    got = loaded_sources()

    bad = []
    for rel in sorted(set(want) | set(got)):
        if rel not in got:
            bad.append(f'    {rel}: pinned but NOT LOADED by the harness')
        elif rel not in want:
            bad.append(f'    {rel}: loaded by the harness but NOT PINNED')
        elif want[rel] != got[rel]:
            bad.append(f'    {rel}: bytes differ from the pin')
    if bad:
        print('PACTA SUBJECT MISMATCH — the fidelity comparison would be'
              ' against a different program than the one pinned:',
              file=sys.stderr)
        print('\n'.join(bad), file=sys.stderr)
        print(f'    pinned commit: {commit}', file=sys.stderr)
        print('    Re-pin deliberately with fidelity/pacta_pin.py --write'
              ' if the new subject is the intended one.', file=sys.stderr)
        return 1
    _, dirty = head_commit()
    state = ' (WORKING TREE DIRTY)' if dirty else ''
    print(f'  pacta subject: {len(got)} module(s) match the pin,'
          f' commit {commit[:7]}{state}')
    return 1 if dirty else 0


if __name__ == '__main__':
    if '--write' in sys.argv:
        write()
    elif '--verify' in sys.argv:
        raise SystemExit(verify())
    else:
        raise SystemExit(__doc__)