On Wed, Mar 11, 2009 at 4:25 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Wed, Mar 11, 2009 at 11:23 AM, Geoffrey Irving <[email protected]> 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
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
