coq/harness/differentialar.py: two unsupported inputs escape as raw TypeError / KeyError instead of Unsupported

[tetsuo-jp]

differentialar.check() documents Unsupported as the way a program outside
the extracted core is reported, and callers catch it to record a skip. Two
input shapes bypass that contract and propagate a raw Python exception, which
callers must either crash on or swallow with a bare except Exception.

This matters more than a normal crash: a harness that raises the wrong exception
type turns "we did not check this" into "this failed" (or, with a broad
except, into "no problem found"). We hit exactly that confusion while
measuring a third-party corpus.

Both are reproducible against main and development.

git clone https://github.com/yokoyama-lab/PyJanus.git && cd PyJanus
cat > /tmp/repro.py <<'EOF'
import sys
sys.path.insert(0, "."); sys.path.insert(0, "coq/harness")
import differentialar
for p in sys.argv[1:]:
    try:
        print("OK", p, differentialar.check("coq/harness/driverar", p))
    except differentialar.Unsupported as e:
        print("Unsupported", p, e)
    except Exception as e:
        print("LEAK", p, type(e).__name__ + ":", e)
EOF
PYTHONPATH=$PWD python3 /tmp/repro.py /tmp/nodim.j /tmp/litpush.j

---

(1) An array declared without an explicit dimension

procedure main()
  int A[] = {1, 2, 3}
  A[0] += 1

Expected: Unsupported, or (better) support — the length is statically
known from the initializer.
Actual:

LEAK /tmp/nodim.j TypeError: 'NoneType' object is not subscriptable

File "coq/harness/differentialar.py", line 447, in translate
    L *= int(d["value"])

int A[] = {...} parses with dimensions == [None] — the length comes from the
initializer, not from a dimension expression — and the two size(A) resolution
loops index d["value"] without checking. There are two such sites:
differentialar.py:320 (procedure-local declarations) and :447 (main's
declarations); we only trip :447 here, but :320 looks identical.

A working pattern already exists in the sibling harness: codegen_diff.py's
_dims_of() raises its own _Ragged for exactly this case:

if d is None or not hasattr(d, "value"):
    raise _Ragged("array with a non-constant dimension")

and codegen_diff.py correctly reports SKIP: array with a non-constant dimension for the program above. Guess at a fix (unverified): apply the
same guard at both differentialar.py sites, raising Unsupported. Resolving
len(initializer) instead would be strictly better, but the guard is the part
that is clearly correct.

---

(2) push/pop whose first argument is not an lvalue

procedure main()
  stack s = nil
  int m = 0
  push(1, s)
  pop(m, s)
  m -= 1

Expected: Unsupported.
Actual:

LEAK /tmp/litpush.j KeyError: 'lval'

File "coq/harness/differentialar.py", line 385, in stmt
    lval = s["expr"]["lval"]

The statement translator assumes the push/pop argument node carries an
lval key. For a constant argument it does not.

Guess at a fix (unverified): if "lval" not in s["expr"]: raise Unsupported("push/pop of a non-lvalue") — but see the cross-reference: if
validate_program is tightened to reject this shape (companion issue, item
(3)), the harness inherits the guarantee and only needs the guard as defence in
depth.

---

Cross-reference

Item (2) has the same trigger as the third C++-back-end defect in the companion
issue. Whoever decides whether push(<literal>, s) is legal Janus should fix
both.

Scope

Across 150 parsed Janus programs in the two corpora we sweep: 2 files hit (1),
6 files contain the trigger for (2). Three of them are the programs on which we
originally observed this, so the leak rate on a real corpus is about 2%.

Suggestion

Consider adding a harness-level regression test that asserts the exception
type: for each file in a small "known-unsupported" fixture set, check() must
raise Unsupported and nothing else. Unsupported is raised in 23 places in
differentialar.py, so the contract is clearly intended — it is just not
enforced anywhere.

[tetsuo-jp]

Companion issue on the C++ back-end: #4 (item (3) there has the same trigger as item (2) here).