security/framework/checks/ec-machine-check.sh

#!/usr/bin/env bash
# ec-machine-check.sh -- actually COMPILE every EasyCrypt theory in a repo and
# fail if any does not machine-check. A `.eco` on disk or a "proven" claim in a
# doc is NOT evidence; only `easycrypt compile` exiting 0 is. This catches the
# class of defect a grep gate cannot: a `.ec` that fails to compile (stale
# require, type-order bug, `nothing to introduce`, `cannot prove goal`) yet sits
# in the tree looking authoritative -- exactly how corona's Combine_Wrapper and
# pulsar's V04_Sign_Ctx orphan hid until the toolchain was pointed at them.
#
# Toolchain: EasyCrypt installs via opam (OCaml) + dispatches to z3/alt-ergo.
# This script sources the opam env so it works whether or not the caller did.
# If no easycrypt is reachable, it SKIPS honestly (CI is the authority) -- it
# never fakes a pass.
#
# Usage: ec-machine-check.sh <repo-root>
set -uo pipefail
ROOT="${1:?usage: ec-machine-check.sh <repo-root>}"

ECDIR=""
for d in "$ROOT/proofs/easycrypt" "$ROOT/proofs" "$ROOT"; do
  if [ -d "$d" ] && find "$d" -maxdepth 2 -name '*.ec' -print -quit 2>/dev/null | grep -q .; then
    ECDIR="$d"; break
  fi
done
[ -z "$ECDIR" ] && { echo "    [skip] no EasyCrypt theories"; exit 0; }

# Make easycrypt reachable via the opam switch if it isn't already.
if ! command -v easycrypt >/dev/null 2>&1 && command -v opam >/dev/null 2>&1; then
  eval "$(opam env 2>/dev/null)" || true
fi
if ! command -v easycrypt >/dev/null 2>&1; then
  echo "    [skip] easycrypt not installed on host -- CI (scripts/checks/ec-compile.sh) is the authority"
  echo "           install: opam switch + 'opam install easycrypt why3 alt-ergo' (z3 as solver)"
  exit 0
fi

pass=0; fail=0; faillist=""
# Compile from within the EC dir so co-located `require import` resolve.
while IFS= read -r f; do
  rel="${f#"$ECDIR"/}"
  if ( cd "$ECDIR" && easycrypt compile "$rel" ) >/tmp/ec_gate_$$.log 2>&1; then
    pass=$((pass + 1))
  else
    fail=$((fail + 1))
    why=$(tr '\r' '\n' < /tmp/ec_gate_$$.log | grep -iE 'critical|error|cannot|unknown|nothing to' | head -1)
    faillist="$faillist
      [FAIL] $rel  <- ${why:-did not compile}"
  fi
done < <(find "$ECDIR" -maxdepth 2 -name '*.ec' 2>/dev/null | sort)
rm -f /tmp/ec_gate_$$.log

if [ "$fail" -eq 0 ]; then
  echo "    [ok]   EasyCrypt: $pass/$pass theories machine-check (easycrypt compile)"
  exit 0
fi
echo "    [FAIL] EasyCrypt: $fail of $((pass + fail)) theories do NOT machine-check:$faillist"
echo "           a non-compiling .ec must be fixed, or removed from the closed set and"
echo "           reclassified OPEN in AXIOM-INVENTORY / OPEN-BRIDGES -- never counted green."
exit 2