More extensive help documentation for llvm_verify_x86_with_invariant.

src/SAWScript/Interpreter.hs

@@ -3184,9 +3184,34 @@ primitives = Map.fromList
     "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec"
     (pureVal llvm_verify_x86_with_invariant)
     Experimental
-    [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties"
+    [ "An experimental extension of 'llvm_verify_x86'. This extension can prove some properties"
     , "involving simple loops with the help of a user-provided loop invariant that describes"
     , "how the live variables in the loop evolve as the loop computes."
+    , ""
+    , "The loop invariant is provided by the tuple argument, which indicates what symbol the loop"
+    , "appears in (which might differ from the function the specification is for), which loop within"
+    , "that function to reason about (starts counting from 0), and a term that desribes the loop invariant"
+    , "itself. For this verification command to succeed, the loop in question must have a single entry-point,"
+    , "must have a single back-edge, and must have a constant memory footprint."
+    , ""
+    , "The SAWCore type expected of the loop invariant will depend on the results of an analysis done"
+    , "on the indicated loop, which will attempt to discover what are all the loop-carried dependencies."
+    , "The result of this analysis will be packaged into a tuple, and any relevant top-level specification"
+    , "variables will be found. The expected type of the loop invariant will then be a function over all"
+    , "the implicit variables found, and two tuples consisting of the initial values of the loop-carried"
+    , "dependencies, and the current value of the loop-carried dependencies. The function should return Bool."
+    , "Some trial-and-error will generally be required to match the results of the analysis with a sutiable"
+    , "function."
+    , ""
+    , "As part of the verification process, the loop invariant will be used in several ways. First, a proof"
+    , "obligation will be issued upon first entry to the loop, establishing the loop invariant holds at the"
+    , "beginning of the loop. Second, the loop invariant is used when starting execution from the loop head"
+    , "to make a generic assumption that the invariant holds. Finally, the invariant is used when execution"
+    , "once again reaches the loop head to assert that the invariant holds inductively across the execution"
+    , "of the loop body."
+    , ""
+    , "Provided all the generated verification conditions are discharged, this results in a partial"
+    , "correctness proof for the indicated function. Note that termination is not proved via this procedure."
     ]
 
   , prim "enable_x86_what4_hash_consing" "TopLevel ()"