fix: apply safety triangle fixes (recipe-heredoc-to-install,recipe-shell-quote-vars)

Auto-applied by hypatia dispatch-runner via gitbot-fleet.
3 file(s) modified.

Recipes: recipe-heredoc-to-install,recipe-shell-quote-vars

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: Jonathan D.A. Jewell

.clusterfuzzlite/build.sh

@@ -1,6 +1,6 @@
 #!/bin/bash -eu
 # SPDX-License-Identifier: PMPL-1.0
-cd $SRC/absolute-zero
+cd "$SRC"/absolute-zero
 cargo +nightly fuzz build
 for target in $(cargo +nightly fuzz list); do
     cp ./target/x86_64-unknown-linux-gnu/release/$target $OUT/

setup-and-verify.sh

@@ -123,7 +123,11 @@ if [ ${#MISSING_TOOLS[@]} -gt 0 ]; then
     echo "Install with:"
     echo "  Fedora: sudo dnf install coq z3 && cargo install just"
     echo "  Ubuntu: sudo apt install coq z3 && cargo install just"
+# WARNING: Pipe-to-shell is unsafe — download and verify first
+# WARNING: Pipe-to-shell is unsafe — download and verify first
     echo "  Deno: curl -fsSL https://deno.land/install.sh | sh"
+# WARNING: Pipe-to-shell is unsafe — download and verify first
+# WARNING: Pipe-to-shell is unsafe — download and verify first
     echo "  Lean 4: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh"
     echo ""
 fi
@@ -217,7 +221,7 @@ if [[ $REPLY =~ ^[Yy]$ ]]; then
         if command -v coqc &> /dev/null; then
             echo "Building Coq proofs..."
             cd proofs/coq/common && coqc CNO.v || echo "⚠ CNO.v failed"
-            cd $REPO_ROOT
+            cd "$REPO_ROOT"
         fi
 
         # Try Z3
@@ -230,7 +234,7 @@ if [[ $REPLY =~ ^[Yy]$ ]]; then
         if command -v lake &> /dev/null; then
             echo "Building Lean 4..."
             cd proofs/lean4 && lake build || echo "⚠ Lean build failed"
-            cd $REPO_ROOT
+            cd "$REPO_ROOT"
         fi
     fi
 fi

src/abi/Layout.idr

@@ -242,10 +242,15 @@ instructionCrossPlatform = InvariantProof
 public export
 verifyAlignment : (p : Platform) -> (t : Type) ->
                   HasAlignment t n -> So (n `mod` (ptrSize p `div` 8) == 0)
+-- PROOF_TODO: Replace believe_me with actual proof
 verifyAlignment Linux t (AlignProof {n}) = believe_me Oh
+-- PROOF_TODO: Replace believe_me with actual proof
 verifyAlignment Windows t (AlignProof {n}) = believe_me Oh
+-- PROOF_TODO: Replace believe_me with actual proof
 verifyAlignment MacOS t (AlignProof {n}) = believe_me Oh
+-- PROOF_TODO: Replace believe_me with actual proof
 verifyAlignment BSD t (AlignProof {n}) = believe_me Oh
+-- PROOF_TODO: Replace believe_me with actual proof
 verifyAlignment WASM t (AlignProof {n}) = believe_me Oh
 
 ||| ProgramState alignment is valid on all platforms
@@ -277,6 +282,7 @@ alignedSize size align =
 public export
 alignedSizeCorrect : (size : Nat) -> (align : Nat) -> {auto 0 nonZero : So (align /= 0)} ->
   So (alignedSize size align `mod` align == 0)
+-- PROOF_TODO: Replace believe_me with actual proof
 alignedSizeCorrect size align = believe_me Oh
 
 --------------------------------------------------------------------------------