File size: 1,470 Bytes
d8df231 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 | #!/usr/bin/env bash
# Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
# SPDX-License-Identifier: LicenseRef-Proprietary
# Public source visibility does not grant an open-source license. See LICENSE.
set -euo pipefail
ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
IDRIS_DIR="$ROOT/idris"
ADA_DIR="$ROOT/ada"
ATS_DIR="$ROOT/ats"
# Guardrail only: semantic review and compiler checks remain necessary.
if grep -RniE '\b(believe_me|sorry|admit|assert_total|assert_smaller)\b|pragma[[:space:]]+Assume' \
"$IDRIS_DIR" "$ADA_DIR" "$ATS_DIR"; then
echo "FAIL: prohibited proof escape hatch detected" >&2
exit 20
fi
for tool in idris2 patsopt gprbuild gnatprove; do
if ! command -v "$tool" >/dev/null 2>&1; then
echo "FAIL: $tool not installed" >&2
exit 2
fi
done
mkdir -p "$ROOT/build"
patsopt -tc -s "$ATS_DIR/heap.sats"
patsopt -tc -s "$ATS_DIR/state.sats"
cd "$IDRIS_DIR"
idris2 --total --check Main.idr
idris2 --total --check LambdaProofs.idr
idris2 --total -o unlambda_model Main.idr
test "$(build/exec/unlambda_model)" = 'step: advanced'
cd "$ADA_DIR"
gprbuild -p -P heap_model.gpr
test "$("$ROOT/build/heap_demo")" = 'heap contract smoke test: PASS'
# All required checks must be proved; ordinary successful invocation is insufficient.
gnatprove -P heap_model.gpr -u heap_model.adb --mode=all \
--checks-as-errors=on --warnings=error --report=all --level=2
echo "PASS: ATS interfaces, Idris model, and allocation-counter heap."
|