absolute-zero.oil

#!/usr/bin/env oil
# Absolute Zero: Oil Shell Wrapper
# Modern shell interface for CNO formal verification
#
# Author: Jonathan D. A. Jewell
# Project: Absolute Zero
# License: AGPL-3.0 / Palimpsest 0.5

# Use Oil's block syntax for better structure
proc show_help {
  echo "Absolute Zero - Certified Null Operations"
  echo ""
  echo "Usage: oil absolute-zero.oil <command>"
  echo ""
  echo "Commands:"
  echo "  build         - Build all proof systems"
  echo "  build-coq     - Build Coq proofs only"
  echo "  build-lean    - Build Lean 4 proofs only"
  echo "  build-z3      - Verify Z3 SMT specifications"
  echo "  verify        - Run all verification checks"
  echo "  test          - Run all tests"
  echo "  clean         - Clean build artifacts"
  echo "  stats         - Show proof statistics"
  echo "  status        - Show proof completion status"
  echo "  help          - Show this help message"
  echo ""
  echo "For more commands, see: just --list"
}

proc check_command {
  var cmd = $1
  if ! which $cmd &>/dev/null {
    echo "⚠ $cmd not found"
    return 1
  }
  return 0
}

proc build_all {
  echo "=== Building All Proof Systems ==="

  # Check for just
  if check_command just {
    just build-all
    return
  }

  # Fallback: Manual build
  echo "Using manual build (just not found)"

  # Build Coq
  if check_command coqc {
    echo "Building Coq proofs..."
    cd proofs/coq/common && coqc CNO.v || {
      echo "✗ Coq build failed"
      return 1
    }
    cd ../physics && {
      coqc -R ../common CNO StatMech.v
      coqc -R ../common CNO LandauerDerivation.v
    }
    cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v
    echo "✓ Coq proofs built"
  }

  # Build Z3
  if check_command z3 {
    echo "Verifying Z3 specifications..."
    z3 proofs/z3/cno_properties.smt2 && echo "✓ Z3 verification complete"
  }

  # Build Lean 4
  if check_command lake {
    echo "Building Lean 4 proofs..."
    cd proofs/lean4 && lake build && echo "✓ Lean 4 proofs built"
  }

  # Build TypeScript
  if check_command npm {
    echo "Building TypeScript..."
    npm install && npm run build && echo "✓ TypeScript built"
  }
}

proc verify_all {
  echo "=== Running All Verification ==="

  if check_command just {
    just verify-all
    return
  }

  # Manual verification
  echo "Checking Coq proofs for Admitted..."
  var admitted = $(grep -r "Admitted\." proofs/coq/ | wc -l)
  echo "Found $admitted Admitted statements"

  echo "Checking Lean 4 proofs for sorry..."
  var sorry = $(grep -r "sorry" proofs/lean4/ | wc -l)
  echo "Found $sorry sorry statements"

  if check_command z3 {
    echo "Running Z3 verification..."
    z3 proofs/z3/cno_properties.smt2
  }
}

proc show_stats {
  echo "=== Proof Statistics ==="

  if check_command just {
    just proof-status
    return
  }

  # Manual stats
  echo "Coq files:"
  find proofs/coq -name "*.v" -exec wc -l {} + | tail -1

  echo "Lean 4 files:"
  find proofs/lean4 -name "*.lean" -exec wc -l {} + 2>/dev/null | tail -1 || echo "0"

  echo "Z3 specifications:"
  wc -l proofs/z3/cno_properties.smt2
}

proc clean_all {
  echo "=== Cleaning Build Artifacts ==="

  if check_command just {
    just clean
    return
  }

  # Manual clean
  find proofs/coq -name "*.vo" -delete
  find proofs/coq -name "*.vok" -delete
  find proofs/coq -name "*.vos" -delete
  find proofs/coq -name "*.glob" -delete

  cd proofs/lean4 && lake clean 2>/dev/null

  rm -rf node_modules dist

  echo "✓ Clean complete"
}

# Main command dispatch using Oil's case syntax
proc main {
  var cmd = ${1:-help}

  case $cmd in
    (build)
      build_all
      ;;
    (build-coq)
      if check_command just {
        just build-coq
      } else {
        cd proofs/coq/common && coqc CNO.v
      }
      ;;
    (build-lean)
      if check_command just {
        just build-lean
      } else {
        cd proofs/lean4 && lake build
      }
      ;;
    (build-z3)
      if check_command just {
        just build-z3
      } else {
        z3 proofs/z3/cno_properties.smt2
      }
      ;;
    (verify)
      verify_all
      ;;
    (test)
      if check_command just {
        just test-all
      } else {
        echo "Running tests..."
        verify_all
      }
      ;;
    (clean)
      clean_all
      ;;
    (stats)
      show_stats
      ;;
    (status)
      if check_command just {
        just proof-status
      } else {
        show_stats
      }
      ;;
    (help|--help|-h)
      show_help
      ;;
    (*)
      echo "Unknown command: $cmd"
      echo ""
      show_help
      return 1
      ;;
  esac
}

# Entry point
main @ARGV