dafny-lang/dafny-vmc

VMC: a Library for Verified Monte Carlo Algorithms

dafny-vmc's Issues

Simplify the definition of UniformPowerOfTwo model

I believe the current definition of UniformPowerOfTwo.Model.Sample is suboptimal and makes the proofs around it more painful than they'd have to be. Currently the correctness predicate has the precondition (n == 0 && k == 0) || (k != 0 && Helper.Power(2, k - 1) <= n < Helper.Power(2, k)), which is annoying because of the case split and (I believe) because of this we have the weird Helper.Log2 which computes something slightly different from the actual log2.
Instead I think it would be better if Sample were defined as follows:

function Sample(n: nat): Monad.Hurd<nat>
  requires n >= 1
{
  if n == 1 then Monad.Return(0) else Monad.Bind(Sample(n/2), UnifStep)
}

Then the correctness predicate would have the precondition Helper.Power(2, k) <= n < Helper.Power(2, k + 1) and the result range of return values m would be 0 <= m < Helper.Power(2, k). Then k would be the actual logarithm of base 2 rounded down. I think this would be much cleaner because it avoids the extra case split and the - 1 in the exponent, which could a priori lead to negative numbers and has to be proved impossible.

C# code potentially insecure?

I noticed that Java uses SecureRandom, but C# just Random. We should look into whether Random is actually secure enough in C#.

Add header comment to generated files

e.g. https://github.com/dafny-lang/Dafny-VMC/blob/main/src/DafnyVMCTrait.dfy should have a header stating that it is machine generated.