Skip to content

Commit

Permalink
Use camelCase instead of snake_case for locals
Browse files Browse the repository at this point in the history
  • Loading branch information
@fzaiser
fzaiser committed Oct 13, 2023
1 parent 223cd18 commit 5efab50
Show file tree
Hide file tree
Showing 5 changed files with 41 additions and 41 deletions.
8 changes: 4 additions & 4 deletions src/Distributions/Uniform/Implementation.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,14 +16,14 @@ module Uniform.Implementation {
ensures u < n
ensures Model.Sample(n)(old(s)) == (u, s)
{
ghost var prev_s := s;
ghost var prevS := s;
u := UniformPowerOfTwoSample(2 * n);
while u >= n
decreases *
invariant Model.Sample(n)(old(s)) == Model.Sample(n)(prev_s)
invariant (u, s) == Model.Proposal(n)(prev_s)
invariant Model.Sample(n)(old(s)) == Model.Sample(n)(prevS)
invariant (u, s) == Model.Proposal(n)(prevS)
{
prev_s := s;
prevS := s;
u := UniformPowerOfTwoSample(2 * n);
}
}
Expand Down
34 changes: 17 additions & 17 deletions src/Distributions/UniformPowerOfTwo/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -271,13 +271,13 @@ module UniformPowerOfTwo.Correctness {
lemma SampleSetEquality(n: nat, m: nat)
requires n >= 2
ensures
var b_of := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0;
var a_of := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0;
(iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*a_of(s) + Helper.boolToNat(b_of(s)) == m)
var bOf := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0;
var aOf := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0;
(iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*aOf(s) + Helper.boolToNat(bOf(s)) == m)
{
var b_of := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0;
var a_of := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0;
forall s ensures Model.Sample(n)(s).0 == m <==> (2 * a_of(s) + Helper.boolToNat(b_of(s)) == m) {
var bOf := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0;
var aOf := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0;
forall s ensures Model.Sample(n)(s).0 == m <==> (2 * aOf(s) + Helper.boolToNat(bOf(s)) == m) {
var (a, s') := Model.Sample(n / 2)(s);
var (b, s'') := Monad.Coin(s');
calc {
Expand All @@ -300,20 +300,20 @@ module UniformPowerOfTwo.Correctness {
requires n >= 2
ensures Random.Prob(iset s | Model.Sample(n)(s).0 == m) == Random.Prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0
{
var a_of: Random.Bitstream -> nat := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0;
var b_of: Random.Bitstream -> bool := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0;
var aOf: Random.Bitstream -> nat := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0;
var bOf: Random.Bitstream -> bool := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0;
var A: iset<nat> := (iset x: nat | x == m / 2);
var E: iset<Random.Bitstream> := (iset s | m % 2 as nat == Helper.boolToNat(Monad.Coin(s).0));
var f := (s: Random.Bitstream) => Model.Sample(n / 2)(s).1;

var e1 := (iset s | Model.Sample(n / 2)(s).1 in E);
var e2 := (iset s | Model.Sample(n / 2)(s).0 in A);
var e3 := (iset s | 2*a_of(s) + Helper.boolToNat(b_of(s)) == m);
var e3 := (iset s | 2*aOf(s) + Helper.boolToNat(bOf(s)) == m);

assert SplitEvent: e3 == e1 * e2 by {
forall s ensures s in e3 <==> s in e1 && s in e2 {
var a: nat := a_of(s);
var b: nat := Helper.boolToNat(b_of(s));
var a: nat := aOf(s);
var b: nat := Helper.boolToNat(bOf(s));
assert b < 2;
calc {
s in e3;
Expand All @@ -325,14 +325,14 @@ module UniformPowerOfTwo.Correctness {
}
}

assert Eq2: (iset s | a_of(s) == m / 2) == e2 by {
forall s ensures a_of(s) == m / 2 <==> Model.Sample(n / 2)(s).0 in A {
assert Eq2: (iset s | aOf(s) == m / 2) == e2 by {
forall s ensures aOf(s) == m / 2 <==> Model.Sample(n / 2)(s).0 in A {
}
}

assert Eq3: (iset s | a_of(s) == m / 2) == (iset s | Model.Sample(n / 2)(s).0 == m / 2) by {
forall s ensures a_of(s) == m / 2 <==> Model.Sample(n / 2)(s).0 == m / 2 {
assert a_of(s) == Model.Sample(n / 2)(s).0;
assert Eq3: (iset s | aOf(s) == m / 2) == (iset s | Model.Sample(n / 2)(s).0 == m / 2) by {
forall s ensures aOf(s) == m / 2 <==> Model.Sample(n / 2)(s).0 == m / 2 {
assert aOf(s) == Model.Sample(n / 2)(s).0;
}
}

Expand Down Expand Up @@ -385,7 +385,7 @@ module UniformPowerOfTwo.Correctness {
==
Random.Prob(e2) / 2.0;
== { reveal Eq2; }
Random.Prob(iset s | a_of(s) == m / 2) / 2.0;
Random.Prob(iset s | aOf(s) == m / 2) / 2.0;
== { reveal Eq3; }
Random.Prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0;
}
Expand Down
22 changes: 11 additions & 11 deletions src/Math/Analysis/Limits.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,20 +228,20 @@ module Limits {
}
}

lemma LimitOfMultiplicationWithZeroSequence(sequence: nat -> real, bound: real, zero_seq: nat -> real)
lemma LimitOfMultiplicationWithZeroSequence(sequence: nat -> real, bound: real, zeroSeq: nat -> real)
requires Sequences.IsBounded(sequence, bound)
requires ConvergesTo(zero_seq, 0.0)
ensures ConvergesTo(Sequences.Mul(sequence, zero_seq), 0.0)
requires ConvergesTo(zeroSeq, 0.0)
ensures ConvergesTo(Sequences.Mul(sequence, zeroSeq), 0.0)
{
var productSequence := Sequences.Mul(sequence, zero_seq);
var productSequence := Sequences.Mul(sequence, zeroSeq);
forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(productSequence, 0.0, epsilon) {
var epsilon' := epsilon / Reals.Max(bound, 1.0);
assert ExistsCloseSuffix(zero_seq, 0.0, epsilon');
var N :| SuffixIsClose(zero_seq, 0.0, epsilon', N);
assert ExistsCloseSuffix(zeroSeq, 0.0, epsilon');
var N :| SuffixIsClose(zeroSeq, 0.0, epsilon', N);
assert SuffixIsClose(productSequence, 0.0, epsilon, N) by {
forall n: nat | n >= N ensures Reals.Dist(productSequence(n), 0.0) < epsilon {
var s := sequence(n);
var z := zero_seq(n);
var z := zeroSeq(n);
calc {
Reals.Dist(productSequence(n), 0.0);
==
Expand Down Expand Up @@ -364,8 +364,8 @@ module Limits {
ensures ConvergesTo(Sequences.OneOverNPlus1, 0.0)
{
forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(Sequences.OneOverNPlus1, 0.0, epsilon) {
var epsilon_inv := 1.0 / epsilon;
var N := epsilon_inv.Floor;
var epsilonInv := 1.0 / epsilon;
var N := epsilonInv.Floor;
assert SuffixIsClose(Sequences.OneOverNPlus1, 0.0, epsilon, N) by {
forall n: nat ensures n >= N ==> Reals.Dist(Sequences.OneOverNPlus1(n), 0.0) < epsilon {
assert Sequences.OneOverNPlus1(n) > 0.0;
Expand All @@ -377,8 +377,8 @@ module Limits {
Sequences.OneOverNPlus1(N);
==
1.0 / (N + 1) as real;
< { Reals.DivisionIsAntiMonotonicStrict(1.0, (N + 1) as real, epsilon_inv); }
1.0 / epsilon_inv;
< { Reals.DivisionIsAntiMonotonicStrict(1.0, (N + 1) as real, epsilonInv); }
1.0 / epsilonInv;
==
epsilon;
}
Expand Down
10 changes: 5 additions & 5 deletions src/Math/Measures.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,14 +63,14 @@ module Measures {
}

// Definition 9
ghost predicate IsMeasurable<S(!new),T>(event_space_s: iset<iset<S>>, event_space_t: iset<iset<T>>, f: S -> T) {
forall e | e in event_space_t :: PreImage(f, e) in event_space_s
ghost predicate IsMeasurable<S(!new),T>(eventSpaceS: iset<iset<S>>, eventSpaceT: iset<iset<T>>, f: S -> T) {
forall e | e in eventSpaceT :: PreImage(f, e) in eventSpaceS
}

// Definition 10
ghost predicate IsMeasurePreserving<S(!new),T>(event_space_s: iset<iset<S>>, mu_s: iset<S> -> real, event_space_t: iset<iset<T>>, mu_t: iset<T> -> real, f: S -> T) {
&& IsMeasurable(event_space_s, event_space_t, f)
&& forall e | e in event_space_t :: mu_s(PreImage(f, e)) == mu_t(e)
ghost predicate IsMeasurePreserving<S(!new),T>(eventSpaceS: iset<iset<S>>, measureS: iset<S> -> real, eventSpaceT: iset<iset<T>>, measureT: iset<T> -> real, f: S -> T) {
&& IsMeasurable(eventSpaceS, eventSpaceT, f)
&& forall e | e in eventSpaceT :: measureS(PreImage(f, e)) == measureT(e)
}

// Definition 12
Expand Down
8 changes: 4 additions & 4 deletions src/Math/Rationals.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,16 +121,16 @@ module Rationals {
var floor := r.numer / r.denom;
var multiple := floor * r.denom;
assert r.numer == multiple + r.numer % r.denom;
var next_multiple := multiple + r.denom;
var nextMultiple := multiple + r.denom;
assert Floor(r) as real <= ToReal(r);
assert ToReal(r) < Floor(r) as real + 1.0 by {
assert r.numer < next_multiple;
assert r.numer < nextMultiple;
calc {
ToReal(r);
==
r.numer as real / r.denom as real;
< { DivStrictlyMonotonic(r.denom as real, r.numer as real, next_multiple as real); }
next_multiple as real / r.denom as real;
< { DivStrictlyMonotonic(r.denom as real, r.numer as real, nextMultiple as real); }
nextMultiple as real / r.denom as real;
==
(floor + 1) as real;
==
Expand Down

0 comments on commit 5efab50

Please sign in to comment.