@@ -26,6 +26,10 @@ PASSED_CHECKS=0
2626FAILED_CHECKS=0
2727SKIPPED_CHECKS=0
2828
29+ # Create a secure temporary directory for check logs
30+ TMPDIR_CHECKS=" $( mktemp -d) "
31+ trap ' rm -rf "${TMPDIR_CHECKS}"' EXIT
32+
2933# Function to check if command exists
3034command_exists () {
3135 command -v " $1 " > /dev/null 2>&1
@@ -34,18 +38,21 @@ command_exists() {
3438# Function to run a check
3539run_check () {
3640 local name=" $1 "
37- local command=" $2 "
41+ shift
42+ local check_cmd=(" $@ " )
3843 TOTAL_CHECKS=$(( TOTAL_CHECKS + 1 ))
3944
40- echo -n " [$TOTAL_CHECKS ] $name ... "
41- if eval " $command " > /tmp/absolute-zero-check-$TOTAL_CHECKS .log 2>&1 ; then
45+ local log_file=" ${TMPDIR_CHECKS} /check-${TOTAL_CHECKS} .log"
46+
47+ echo -n " [${TOTAL_CHECKS} ] ${name} ... "
48+ if " ${check_cmd[@]} " > " ${log_file} " 2>&1 ; then
4249 echo -e " ${GREEN} PASS${NC} "
4350 PASSED_CHECKS=$(( PASSED_CHECKS + 1 ))
4451 return 0
4552 else
4653 echo -e " ${RED} FAIL${NC} "
4754 FAILED_CHECKS=$(( FAILED_CHECKS + 1 ))
48- echo " Error log: /tmp/absolute-zero-check- $TOTAL_CHECKS .log "
55+ echo " Error log: ${log_file} "
4956 return 1
5057 fi
5158}
@@ -56,7 +63,7 @@ skip_check() {
5663 local reason=" $2 "
5764 TOTAL_CHECKS=$(( TOTAL_CHECKS + 1 ))
5865 SKIPPED_CHECKS=$(( SKIPPED_CHECKS + 1 ))
59- echo -e " [$TOTAL_CHECKS ] $name ... ${YELLOW} SKIP${NC} ($reason )"
66+ echo -e " [${ TOTAL_CHECKS} ] ${ name} ... ${YELLOW} SKIP${NC} (${ reason} )"
6067}
6168
6269echo " ==== Tool Availability Check ===="
@@ -112,35 +119,35 @@ echo "==== Running Verification ===="
112119echo " "
113120
114121# Z3 SMT Verification
115- if [ $ Z3_AVAILABLE -eq 1 ]; then
122+ if [ " ${ Z3_AVAILABLE} " -eq 1 ]; then
116123 echo " ---- Z3 SMT Solver ----"
117- run_check " Z3: CNO Properties" " z3 proofs/z3/cno_properties.smt2"
124+ run_check " Z3: CNO Properties" z3 proofs/z3/cno_properties.smt2
118125 echo " "
119126else
120127 skip_check " Z3: CNO Properties" " z3 not installed"
121128 echo " "
122129fi
123130
124131# Coq Verification
125- if [ $ COQ_AVAILABLE -eq 1 ]; then
132+ if [ " ${ COQ_AVAILABLE} " -eq 1 ]; then
126133 echo " ---- Coq Proof Assistant ----"
127- run_check " Coq: Phase 1 Core (CNO.v)" " coqc -Q proofs/coq/common CNO proofs/coq/common/CNO.v"
128- run_check " Coq: Statistical Mechanics" " coqc -Q proofs/coq/common CNO -Q proofs/coq/physics Physics proofs/coq/physics/StatMech.v"
129- run_check " Coq: Category Theory" " coqc -Q proofs/coq/common CNO -Q proofs/coq/category Category proofs/coq/category/CNOCategory.v"
130- run_check " Coq: Lambda Calculus" " coqc -Q proofs/coq/common CNO -Q proofs/coq/lambda Lambda proofs/coq/lambda/LambdaCNO.v"
131- run_check " Coq: Quantum CNO" " coqc -Q proofs/coq/common CNO -Q proofs/coq/quantum Quantum proofs/coq/quantum/QuantumCNO.v"
132- run_check " Coq: Filesystem CNO" " coqc -Q proofs/coq/common CNO -Q proofs/coq/filesystem Filesystem proofs/coq/filesystem/FilesystemCNO.v"
134+ run_check " Coq: Phase 1 Core (CNO.v)" coqc -Q proofs/coq/common CNO proofs/coq/common/CNO.v
135+ run_check " Coq: Statistical Mechanics" coqc -Q proofs/coq/common CNO -Q proofs/coq/physics Physics proofs/coq/physics/StatMech.v
136+ run_check " Coq: Category Theory" coqc -Q proofs/coq/common CNO -Q proofs/coq/category Category proofs/coq/category/CNOCategory.v
137+ run_check " Coq: Lambda Calculus" coqc -Q proofs/coq/common CNO -Q proofs/coq/lambda Lambda proofs/coq/lambda/LambdaCNO.v
138+ run_check " Coq: Quantum CNO" coqc -Q proofs/coq/common CNO -Q proofs/coq/quantum Quantum proofs/coq/quantum/QuantumCNO.v
139+ run_check " Coq: Filesystem CNO" coqc -Q proofs/coq/common CNO -Q proofs/coq/filesystem Filesystem proofs/coq/filesystem/FilesystemCNO.v
133140 echo " "
134141else
135142 skip_check " Coq: All proofs" " coqc not installed"
136143 echo " "
137144fi
138145
139146# Lean 4 Verification
140- if [ $ LEAN_AVAILABLE -eq 1 ]; then
147+ if [ " ${ LEAN_AVAILABLE} " -eq 1 ]; then
141148 echo " ---- Lean 4 Proof Assistant ----"
142149 if [ -f " proofs/lean4/lakefile.lean" ]; then
143- run_check " Lean 4: Build all proofs" " cd proofs/lean4 && lake build"
150+ run_check " Lean 4: Build all proofs" bash -c " cd proofs/lean4 && lake build"
144151 else
145152 skip_check " Lean 4: Build all proofs" " lakefile.lean not found"
146153 fi
@@ -151,19 +158,19 @@ else
151158fi
152159
153160# Agda Verification
154- if [ $ AGDA_AVAILABLE -eq 1 ]; then
161+ if [ " ${ AGDA_AVAILABLE} " -eq 1 ]; then
155162 echo " ---- Agda Proof Assistant ----"
156- run_check " Agda: CNO Core" " agda proofs/agda/CNO.agda"
163+ run_check " Agda: CNO Core" agda proofs/agda/CNO.agda
157164 echo " "
158165else
159166 skip_check " Agda: CNO Core" " agda not installed"
160167 echo " "
161168fi
162169
163170# Isabelle Verification
164- if [ $ ISABELLE_AVAILABLE -eq 1 ]; then
171+ if [ " ${ ISABELLE_AVAILABLE} " -eq 1 ]; then
165172 echo " ---- Isabelle/HOL ----"
166- run_check " Isabelle: CNO Theory" " isabelle build -d proofs/isabelle -b CNO"
173+ run_check " Isabelle: CNO Theory" isabelle build -d proofs/isabelle -b CNO
167174 echo " "
168175else
169176 skip_check " Isabelle: CNO Theory" " isabelle not installed"
@@ -175,22 +182,22 @@ echo "========================================"
175182echo " Verification Summary"
176183echo " ========================================"
177184echo " "
178- echo " Total checks: $TOTAL_CHECKS "
179- echo -e " ${GREEN} Passed: $PASSED_CHECKS ${NC} "
180- echo -e " ${RED} Failed: $FAILED_CHECKS ${NC} "
181- echo -e " ${YELLOW} Skipped: $SKIPPED_CHECKS ${NC} "
185+ echo " Total checks: ${ TOTAL_CHECKS} "
186+ echo -e " ${GREEN} Passed: ${ PASSED_CHECKS} ${NC} "
187+ echo -e " ${RED} Failed: ${ FAILED_CHECKS} ${NC} "
188+ echo -e " ${YELLOW} Skipped: ${ SKIPPED_CHECKS} ${NC} "
182189echo " "
183190
184- if [ $ FAILED_CHECKS -eq 0 ] && [ $ PASSED_CHECKS -gt 0 ]; then
191+ if [ " ${ FAILED_CHECKS} " -eq 0 ] && [ " ${ PASSED_CHECKS} " -gt 0 ]; then
185192 echo -e " ${GREEN} ✓ All available verifications passed!${NC} "
186193 exit 0
187- elif [ $ PASSED_CHECKS -eq 0 ]; then
194+ elif [ " ${ PASSED_CHECKS} " -eq 0 ]; then
188195 echo -e " ${YELLOW} ⚠ No verification tools available locally${NC} "
189196 echo " Consider installing: coqc, z3, lean, agda, isabelle"
190197 echo " Or run: podman build -t absolute-zero . && podman run --rm absolute-zero ./verify-proofs.sh"
191198 exit 2
192199else
193200 echo -e " ${RED} ✗ Some verifications failed${NC} "
194- echo " Check error logs in /tmp/absolute-zero-check-*.log "
201+ echo " Check error logs in ${TMPDIR_CHECKS} / "
195202 exit 1
196203fi
0 commit comments