Merge pull request #935 from abdoo8080/proofs

Add support for proof flattening.

doc/usr/source/9_other/5_proofs.rst

@@ -80,7 +80,7 @@ Requirements
 Frontend certificates and proofs production require the user to have JKind
 installed on their machine (together with a suitable version of Java).
 
-SMT-LIB 2 certificates do not require anything additional excepted for an SMT
+SMT-LIB 2 certificates do not require anything additional except for an SMT
 solver to check the certificates.
 
 LFSC proofs production requires cvc5 (the binary can be specified with
@@ -248,7 +248,17 @@ or use the convenient bash script generated by ``lfsc/get-lfsc-checker.sh``:
    lfsc/bin/lfsc-check.sh add_two.lus.out/add_two.lus.1.lfsc
 
 The return code for either command execution is ``0`` when everything was checked
-correctly. Three lines will be displayed when both the proof of invariance and
+correctly.
+
+When the bash script is used and the whole proof is correct,
+the following line will be displayed:
+
+.. code-block:: none
+
+   Valid LFSC proof!
+
+When the LFSC checker is called instead,
+three lines will be displayed when both the proof of invariance and
 the proof of correct translation by the frontend are valid:
 
 .. code-block:: none
@@ -259,7 +269,28 @@ the proof of correct translation by the frontend are valid:
 
 In the case where only the invariance proof was produced and checked, the
 return code will still be ``0`` but only a single ``success`` will be in the
-output of ``lfsc-check.sh``.
+output. 
+
+Proof options
+^^^^^^^^^^^^^
+
+Kind 2 supports several options to control the format and granularity of proofs:
+
+* ``--smaller_holes <bool>`` (default ``false``\ ) -- By default, LFSC proofs
+  generated by Kind 2 contain holes encoded as ``(trust ..)`` steps. This option
+  reduces the size of holes in the generated proofs, and thus, increases trust in
+  Kind 2's result. The option is disabled by default as the more granular proofs
+  take significantly more time to generate, are orders of magnitude larger, and
+  take longer time to verify than proofs with bigger holes. Note: this option
+  reduces the size of holes in the proofs and not their number, which is likely to
+  increase when it is enabled.
+
+* ``--flatten_proof <bool>`` (default ``false``\ ) -- Break the proof down into
+  a sequence of lemmas. The proof for each lemma is verified by the LFSC checker
+  and erased immediately. This option helps reduce the memory footprint of the
+  LFSC checker and improve its performance. It is recommended to enable this
+  option with ``--smaller_holes``. Note: enabling this option will increase the
+  number of ``success`` messages displayed by the LFSC checker.
 
 Contents of certificates
 ------------------------

lfsc/get-lfsc-checker.sh

@@ -77,7 +77,16 @@ SIGS="\$SIG_DIR/core_defs.plf \\
     \$SIG_DIR/quantifiers_rules.plf \\
     \$SIG_DIR/kind.plf"
 ### Release version
-\$LFSC_DIR/bin/lfscc \$SIGS \$@
+tempfile=\$(mktemp)
+\$LFSC_DIR/bin/lfscc \$SIGS \$@ 2> \$tempfile > /dev/null
+status=\$?
+if [ \$status -ne 0 ]; then
+  cat \$tempfile 1>&2
+else
+  echo "Valid LFSC proof!"
+fi
+rm \$tempfile
+exit \$status
 
 ### Debugging version
 #\$LFSC_DIR/bin/lfscc \$SIGS \$@ >& lfsc.out