Modification of `mv-let` supporting speculative and parallel execution

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism, and see parallel-programming, which has a disclaimer.

Example Form: (defun pfib-with-step-count (x) (declare (xargs :mode :program)) (if (or (zp x) (< x 33)) (fib-with-step-count x) (spec-mv-let (a cnt1) (pfib-with-step-count (- x 1)) (mv-let (b cnt2) (pfib-with-step-count (- x 2)) (if t (mv (+ a b) (+ 1 cnt1 cnt2)) (mv "speculative result is always needed" -1)))))) General Form: (spec-mv-let (v1 ... vn) ; bind distinct variables <spec> ; evaluate speculatively; return n values (mv-let ; or, use mv?-let if k=1 below (w1 ... wk) ; bind distinct variables <eager> ; evaluate eagerly (if <test> ; use results from <spec> if true <typical-case> ; may mention v1 ... vn <abort-case>))) ; does not mention v1 ... vn

Our design of `mv-let`. (In ordinary ACL2, the semantics agree with this
description but without speculative or parallel execution.)

Evaluation of the above general form proceeds as suggested by the comments.
First, `mv-let` call, without waiting for the result of evaluating

The calls to

The following definition of

(defun fib-with-step-count (x) (declare (xargs :mode :program)) (cond ((<= x 0) (mv 0 1)) ((= x 1) (mv 1 1)) (t (mv-let (a cnt1) (fib-with-step-count (- x 1)) (mv-let (b cnt2) (fib-with-step-count (- x 2)) (mv (+ a b) (+ 1 cnt1 cnt2)))))))