Add llvm_verify_fixpoint / llvm_verify_fixpoint_chc for LLVM-bitcode loop fixpoint proofs

[AmeliaRose802]

Summary

Adds llvm_verify_fixpoint and llvm_verify_fixpoint_chc — the LLVM-bitcode counterparts of the existing llvm_verify_fixpoint_x86 / llvm_verify_fixpoint_chc_x86 primitives. They expose Lang.Crucible.LLVM.SimpleLoopFixpoint(.simpleLoopFixpoint) and Lang.Crucible.LLVM.SimpleLoopFixpointCHC.simpleLoopFixpoint for LLVM-bitcode verification, removing the requirement to drop down to the x86 machine-code path (with its ELF-object detour) when a function contains a loop with a symbolic bound.

Motivation

llvm_verify today can only handle loops with concrete bounds; users must either bound the loop in the spec or switch to llvm_verify_fixpoint_x86. The x86 path requires producing an ELF object, which is a significant detour on non-ELF targets (e.g. Windows / x86_64-pc-windows-msvc), and forces machine-code verification of optimized code — a heavier obligation than verifying the LLVM IR of the same function.

Concrete motivating example: a length-prefixed canonicalizer with two byte-copy loops for (uint8_t i = 0; i < nm; ++i) ... and for (uint8_t i = 0; i < nb; ++i) .... Wall-clock numbers for bounded llvm_verify against Z3 (otherwise identical script):

MAX_LEN	4	8	12	16	32
time	sec	10s	2min	13.5min	>25min (killed)

This is exactly the use case SimpleLoopFixpoint exists for.

Changes

Two commits:

1. Add loop fixpoint support for llvm_verify — adds the SAWCentral plumbing:

   • saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs:
     • FixpointSelect = NoFixpoint | SimpleFixpoint TypedTerm | SimpleFixpointCHC TypedTerm
     • llvm_verify_fixpoint and llvm_verify_fixpoint_chc top-level entry points
     • verifyMethodSpecWithFixpoint threading FixpointSelect into verifySimulate, which constructs and installs the fixpoint execution feature via Crucible.LLVM.Fixpoint.simpleLoopFixpoint / Crucible.LLVM.FixpointCHC.simpleLoopFixpoint
   • doc/developer/loop-fixpoint-llvm-verify.md: design doc
   • examples/loop-fixpoint/: simple_loop.c and demo .saw

2. Register llvm_verify_fixpoint{,_chc} as SAWScript primitives — wires the two functions into the interpreter:

   • saw-script/src/SAWScript/Interpreter.hs: two prim entries (Experimental) wrapping the SAWCentral functions directly via pureVal (no do_* wrapper needed since the underlying functions already take Text for the function name)
   • examples/loop-fixpoint/loop_fixpoint_demo.saw: un-gated (the three worked examples now compile and run)
   • doc/developer/loop-fixpoint-llvm-verify.md: status flipped to Implemented (Phase 1). Phase 2 (SimpleInvariant for LLVM bitcode) remains future work — it needs a different loop-identification mechanism (block labels rather than ELF symbol addresses) and is intentionally not exposed here.
   • intTests/test_llvm_loop_fixpoint/: binding-existence regression test

SAWScript types

llvm_verify_fixpoint     : LLVMModule -> String -> [LLVMSpec] -> Bool -> Term ->
                           LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec
llvm_verify_fixpoint_chc : LLVMModule -> String -> [LLVMSpec] -> Bool -> Term ->
                           LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec

The Term argument is the loop's next-state function (or, for the CHC variant, an optional hint that Z3's constrained horn-clause engine can use to synthesize the loop invariant).

Validation

• cabal build saw clean.
• New intTests/test_llvm_loop_fixpoint/ smoke test (binding existence + type check).
• Existing _x86 tests untouched and continue to use the same Crucible.LLVM.SimpleLoopFixpoint machinery.

Risk

Low. The new primitives sit alongside the existing _x86 variants and call into the same crucible-llvm libraries those variants already exercise. Marked Experimental.

[sauclovian-g]

For clarity, is this LLM-generated? It looks like it.

It seems to have rather a lot of cutpaste as it is...

[RyanGlScott]

Thanks for the PR, @AmeliaRose802!

I largely echo @sauclovian-g's sentiments here: this is something that would be nice to have, but I would want to make sure that we aren't blatantly duplicating large parts of llvm_verify_fixpoint_x86's internals in the process. Otherwise, we will have to maintain multiple copies of the same code going forward, which will increase the maintenance burden.