[bitc-dev] temporarily mutable arrays

[Geoffrey Irving]

On Wed, Mar 11, 2009 at 4:25 PM, Jonathan S. Shapiro <shap at eros-os.com> wrote:
> On Wed, Mar 11, 2009 at 11:23 AM, Geoffrey Irving <irving at naml.us> wrote:
>> Uninitialized allocation is perfectly safe as long as you don't mind
>> errors resulting in nondeterministic (but still safe) behavior.
>
> You mean "undefined", not "nondeterministic". And unfortunately, we
> *do* mind. Since we want to be able to embed BitC in a prover,
> undefined behavior is double plus ungood.

Having a constructor that produces undefined memory is equivalent to
having a function of the form

    undefined-vector : int -> '_a vector

where the prover knows that

1. The resulting vector has the appropriate size.
2. Each slot contains a valid integer.
3. undefined-vector has a "nondeterminism" effect bit, which just
means that you can't apply CSE.

Why does that break a prover?  Do random number generators also break provers?

Geoffrey