Fix the three defects blocking natspec spec publication

[shellygr]

Problem

Greenfield tui-natspec cannot publish a spec, and never could. publish is gated on a passing typecheck, and three separate defects sat in that gate, each hidden behind the one before it. The symptom is the same every time: the authoring agents write complete CVL, the feedback judge approves it, every publish attempt is rejected, the agents burn their remaining turns and give up — and the pipeline still writes the interface and the stub, so the run looks like it merely failed to produce specs.

1 & 2 — doubled certora/ segments

temp_certora_file yields a path already relative to the project root, so it carries the certora/ segment; its docstring says callers use it verbatim, "no certora/ prefixing". Two ConfigurationBuilder methods prefixed it again:

yield path / "certora" / basename                # -> <root>/certora/certora/run_<uid>.conf
verify=f"{main_contract}:certora/{spec_file}"    # -> <C>:certora/certora/generated_<uid>.spec

typecheck.py runs the CLI with cwd at the project root and validate_readable_file resolves against the CWD, so both paths were simply missing:

read_from_conf_file: /tmp/tmpXXXXXXXX/certora/certora/run_YYYY.conf: not found
attribute/flag 'verify': file certora/certora/generated_YYYY.spec not found

They mask each other — fixing the conf location just moves the failure to the second message.

3 — interfaces in the conf's files list

With the paths fixed, the CLI got far enough to assemble a scene and refused:

Contract IFoo has no bytecode. It may be caused because the contract is abstract,
or is missing constructor code.

Every entry in files must compile to bytecode. The pipeline registers only stubs, but the authoring agent also registered the interface — reasonably, since its spec references it and register_verification_file invited "any contract source the spec references". There is no unregister tool, so the session poisoned itself irrecoverably. The agent's own diagnosis, after its sixth rejected publish: "blocking error is scene assembly of the pre-registered interface-only file."

The registration also outlives the run that made it: FILES_NS is keyed by document digest, not by cache namespace, so re-running the same document under a fresh --cache-ns reuses the poisoned entry.

Fix

1. Join the project-root-relative paths to the root without re-prefixing, in both places.
2. FileRegistry learns which paths are interfaces: register refuses them with an explanation the agent can act on, and read_all filters them so entries persisted before this commit stay out of the conf. The tool docstring now says not to register interfaces and why. Interfaces reach the scene regardless, through the stubs' imports.

Tests

• tests/test_natspec_conf_path.py mirrors typecheck.run_typecheck — materialize a spec, build a conf around it — and asserts the invariant both path bugs broke: every path the conf hands to the CLI must resolve, from the project root, to a file on disk.
• tests/test_file_registry_non_units.py covers both guards, including the persisted-entry case.

Verified against each code state in the AutoProver container:

Code state	Result
origin/master	conf not written at yielded path: …/certora/certora/run_9c1cb9dc.conf
conf location fixed	verify points at a file that was never written: certora/certora/generated_b80726c8.spec
both paths fixed	scene assembly fails: Contract IFoo has no bytecode
all three fixed	passes

The last row is an end-to-end run of the real typecheck gate — a generated interface + stub and rule sanity { assert true; } through typecheck_spec — which now returns clean. pytest tests/test_natspec_conf_path.py tests/test_file_registry_non_units.py → 3 passed.

Still draft pending a full greenfield pipeline run.