|
| 1 | +#!/usr/bin/env bash |
| 2 | +# Agda↔Typst consistency lint. |
| 3 | +# |
| 4 | +# Full type-checking of the Typst against Agda needs an Agda→Typst backend we |
| 5 | +# don't have, so this guards the two single-source links that matter: |
| 6 | +# |
| 7 | +# (1) every transition rule the prose cites as `<name>` rule is a real |
| 8 | +# constructor of the Agda relation `_⟶⟨_⟩_`; and |
| 9 | +# (2) the head state-machine DIAGRAM (data in diagrams.typ) has exactly the same |
| 10 | +# (source, rule, target) transitions as that Agda relation — so the picture |
| 11 | +# cannot drift from the formal state machine. |
| 12 | +set -euo pipefail |
| 13 | +cd "$(dirname "$0")" |
| 14 | + |
| 15 | +ON=src/Hydra/Protocol/OnChain.lagda.typ |
| 16 | +DIAG=src/diagrams.typ |
| 17 | +fail=0 |
| 18 | + |
| 19 | +# --- Agda transition relation: emit "source|rule|target" per constructor ---- |
| 20 | +agda_transitions() { |
| 21 | + awk ' |
| 22 | + /data _⟶⟨_⟩_ :/ { inrel=1; next } |
| 23 | + inrel && /^```/ { inrel=0 } |
| 24 | + !inrel { next } |
| 25 | + /^ [a-z]/ { if (name != "") emit(); name=$1; buf=$0; next } |
| 26 | + { buf = buf " " $0 } |
| 27 | + END { if (name != "") emit() } |
| 28 | + function emit( a, b, s, t) { |
| 29 | + s = (match(buf, /→[ ]*([A-Za-z]+)/, a) ? a[1] : "?") |
| 30 | + t = (match(buf, /⟩[ ]*([A-Za-z]+)/, b) ? b[1] : "?") |
| 31 | + print s "|" name "|" t |
| 32 | + } |
| 33 | + ' "$ON" | sort -u |
| 34 | +} |
| 35 | + |
| 36 | +# --- Diagram data: emit "from|rule|to" per transition -------------------------- |
| 37 | +diagram_transitions() { |
| 38 | + grep -oE '\(from: "[A-Za-z]+", rule: "[A-Za-z]+", to: "[A-Za-z]+"' "$DIAG" \ |
| 39 | + | sed -E 's/.*from: "([A-Za-z]+)", rule: "([A-Za-z]+)", to: "([A-Za-z]+)".*/\1|\2|\3/' \ |
| 40 | + | sort -u |
| 41 | +} |
| 42 | + |
| 43 | +# --- Check (1): cited rule names exist ---------------------------------------- |
| 44 | +rules=$(agda_transitions | cut -d'|' -f2 | sort -u) |
| 45 | +cited=$(grep -oE '`[A-Za-z]+` rule' "$ON" | sed -E 's/`([A-Za-z]+)` rule/\1/' | sort -u) |
| 46 | +for c in $cited; do |
| 47 | + if ! grep -qx "$c" <<<"$rules"; then |
| 48 | + echo "ERROR: prose cites transition rule '$c' that is not a constructor of _⟶⟨_⟩_" |
| 49 | + fail=1 |
| 50 | + fi |
| 51 | +done |
| 52 | + |
| 53 | +# --- Check (2): diagram transitions == Agda transitions ------------------------ |
| 54 | +only_agda=$(comm -23 <(agda_transitions) <(diagram_transitions)) |
| 55 | +only_diag=$(comm -13 <(agda_transitions) <(diagram_transitions)) |
| 56 | +if [ -n "$only_agda" ]; then |
| 57 | + echo "ERROR: transitions in the Agda relation but MISSING from the diagram (diagrams.typ):" |
| 58 | + echo "$only_agda" | sed 's/^/ /' |
| 59 | + fail=1 |
| 60 | +fi |
| 61 | +if [ -n "$only_diag" ]; then |
| 62 | + echo "ERROR: transitions in the diagram but NOT in the Agda relation _⟶⟨_⟩_:" |
| 63 | + echo "$only_diag" | sed 's/^/ /' |
| 64 | + fail=1 |
| 65 | +fi |
| 66 | + |
| 67 | +# --- Check (3): diagrams.typ `state-fields` keys == HeadDatum constructors ----- |
| 68 | +datum_ctors=$(awk ' |
| 69 | + /data HeadDatum :/ { ind=1; next } |
| 70 | + ind && (/^```/ || /^$/ || /^data /) { ind=0 } |
| 71 | + ind && /^ [A-Z]/ { print $1 } |
| 72 | +' "$ON" | sort -u) |
| 73 | +state_keys=$(awk ' |
| 74 | + /#let state-fields = \(/ { ins=1; next } |
| 75 | + ins && /^\)/ { ins=0 } |
| 76 | + ins && /^ "[A-Za-z]+":/ { gsub(/[",:]/,"",$1); print $1 } |
| 77 | +' "$DIAG" | sort -u) |
| 78 | +if [ -z "$datum_ctors" ] || [ -z "$state_keys" ]; then |
| 79 | + # A silent skip here would let real drift through: if either parse comes back empty the |
| 80 | + # anchors (`data HeadDatum :` / `#let state-fields = (`) no longer match the sources. |
| 81 | + echo "ERROR: check (3) parsed no HeadDatum constructors or no state-fields keys (anchor drift);" |
| 82 | + echo " update the awk anchors in check-refs.sh to match the current source layout." |
| 83 | + fail=1 |
| 84 | +elif [ "$datum_ctors" != "$state_keys" ]; then |
| 85 | + echo "ERROR: diagrams.typ state-fields keys do not match HeadDatum constructors:" |
| 86 | + echo " HeadDatum: $(echo $datum_ctors)" |
| 87 | + echo " state-fields: $(echo $state_keys)" |
| 88 | + fail=1 |
| 89 | +fi |
| 90 | + |
| 91 | +# --- Check (4): every tx-rule diagram maps to a real transition rule ----------- |
| 92 | +tx_rules=$(awk ' |
| 93 | + /#let tx-rule = \(/ { intr=1; next } |
| 94 | + intr && /^\)/ { intr=0 } |
| 95 | + intr && /: "[A-Za-z]+"/ { match($0, /"([A-Za-z]+)"/, a); print a[1] } |
| 96 | +' "$DIAG" | sort -u) |
| 97 | +for r in $tx_rules; do |
| 98 | + if ! grep -qx "$r" <<<"$rules"; then |
| 99 | + echo "ERROR: diagrams.typ tx-rule maps to '$r', not a constructor of _⟶⟨_⟩_" |
| 100 | + fail=1 |
| 101 | + fi |
| 102 | +done |
| 103 | + |
| 104 | +# --- Check (5): every code fence opens as ``` (bare) or ```agda exactly -------- |
| 105 | +# Agda's literate mode typechecks a fence only when its info string is empty or |
| 106 | +# exactly `agda`; a mistyped tag (```Agda, ```agda2, ```haskell) is silently NOT |
| 107 | +# typechecked AND renders as a literal raw block. Flag any non-`agda` tag. |
| 108 | +badfence=$(grep -nE '^```[^`]' src/Hydra/Protocol/*.lagda.typ | grep -vE ':```agda$' || true) |
| 109 | +if [ -n "$badfence" ]; then |
| 110 | + echo "ERROR: code fence with a tag other than 'agda' (skips Agda typecheck AND misrenders):" |
| 111 | + echo "$badfence" | sed 's/^/ /' |
| 112 | + fail=1 |
| 113 | +fi |
| 114 | + |
| 115 | +if [ "$fail" -eq 0 ]; then |
| 116 | + echo "check-refs: OK — cited rules exist, the head-state diagram matches the Agda" |
| 117 | + echo "relation, state-fields KEYS match the HeadDatum constructors (names only, not" |
| 118 | + echo "the per-state field tuples), tx diagrams map to real rules, and" |
| 119 | + echo "every code fence is bare or \`\`\`agda." |
| 120 | +fi |
| 121 | +exit "$fail" |
0 commit comments