From 9b104130eaf89c3ef3b2b4e7a1f15463468f28b4 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Tue, 5 Mar 2024 13:46:49 +0000 Subject: [PATCH] Axiomatise Uniform (#159) By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- audit.log | 2 + src/DafnyVMCTrait.dfy | 12 +-- src/Distributions/Uniform/Correctness.dfy | 111 +--------------------- src/Distributions/Uniform/Model.dfy | 73 +------------- src/Util/FisherYates/Correctness.dfy | 75 +++++++++++---- src/Util/FisherYates/Model.dfy | 41 ++++++-- 6 files changed, 99 insertions(+), 215 deletions(-) diff --git a/audit.log b/audit.log index f1ca8109..373a2aa0 100644 --- a/audit.log +++ b/audit.log @@ -1,4 +1,6 @@ src/DafnyVMC.dfy(28,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. +src/Distributions/Uniform/Correctness.dfy(34,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. +src/Distributions/Uniform/Model.dfy(21,33): Sample: Declaration has explicit `{:axiom}` attribute. src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute. src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute. diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index ab198d06..ad0ec7a3 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -26,7 +26,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliSample (num: nat, den: pos) returns (o: bool) - requires num <= den + requires num <= den modifies this decreases * { @@ -36,7 +36,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos)) returns (o: (bool,pos)) - requires num <= den + requires num <= den modifies this decreases * { @@ -46,7 +46,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos) returns (o: nat) - requires num <= den + requires num <= den modifies this decreases * { @@ -62,7 +62,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos) returns (o: bool) - requires num <= den + requires num <= den modifies this decreases * { @@ -140,7 +140,7 @@ module DafnyVMCTrait { method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,pos)) returns (o: (bool,pos)) - requires num <= den + requires num <= den modifies this decreases * { @@ -226,6 +226,6 @@ module DafnyVMCTrait { } -} + } } diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index a41a3fde..43d11af8 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -31,108 +31,10 @@ module Uniform.Correctness { // Correctness theorem for Model.Sample // Equation (4.12) / PROB_BERN_UNIFORM - lemma UniformFullCorrectness(n: nat, i: nat) + lemma {:axiom} UniformFullCorrectness(n: nat, i: nat) requires 0 <= i < n ensures SampleEquals(n, i) in Rand.eventSpace ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real) - { - var equalsI := (x: nat) => x == i; - - assert Independence.IsIndep(Model.Proposal(n)) && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Model.Proposal(n), Model.Accept(n))) by { - Model.SampleTerminates(n); - } - - Loops.UntilProbabilityFraction(Model.Proposal(n), Model.Accept(n), equalsI); - var eventResultEqualsI := Loops.UntilLoopResultHasProperty(Model.Proposal(n), Model.Accept(n), equalsI); - var eventProposalAcceptedAndEqualsI := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI); - var proposalAccepted := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); - - assert Fraction: Rand.prob(eventResultEqualsI) == Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted); - - assert Eq: eventResultEqualsI == SampleEquals(n, i) by { - forall s ensures s in eventResultEqualsI <==> s in SampleEquals(n, i) { - reveal Model.Sample(); - assert s in eventResultEqualsI <==> s in SampleEquals(n, i); - } - } - - assert SampleEquals(n, i) in Rand.eventSpace by { - reveal Eq; - } - - assert Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real) by { - calc { - Rand.prob(SampleEquals(n, i)); - { reveal Eq; } - Rand.prob(eventResultEqualsI); - { reveal Fraction; } - Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted); - { ProbabilityProposalAcceptedAndEqualsI(n, i); } - (1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)) / Rand.prob(proposalAccepted); - { ProbabilityProposalAccepted(n); } - (1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)) / ((n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)); - { RealArith.SimplifyFractions(1.0, n as real, NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real); } - 1.0 / (n as real); - } - } - } - - lemma ProbabilityProposalAcceptedAndEqualsI(n: nat, i: nat) - requires 0 <= i < n - ensures - Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i)) == 1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real) - { - var e := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i); - var nextPowerOfTwo := NatArith.Power(2, NatArith.Log2Floor(2 * n)); - assert iBound: i < nextPowerOfTwo by { - calc { - i; - < - n; - < { NatArith.NLtPower2Log2FloorOf2N(n); } - nextPowerOfTwo; - } - } - assert setEq: Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i) == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i) by { - forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i { - assert s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i; - } - } - calc { - Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i)); - { reveal setEq; } - Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i); - { reveal iBound; UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); } - 1.0 / (nextPowerOfTwo as real); - } - } - - lemma ProbabilityProposalAccepted(n: nat) - requires n >= 1 - ensures - Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real) - { - var e := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); - assert n < NatArith.Power(2, NatArith.Log2Floor(2 * n)) by { NatArith.NLtPower2Log2FloorOf2N(n); } - assert Equal: e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n) by { - forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n { - calc { - s in e; - Model.Accept(n)(Model.Proposal(n)(s).value); - UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n; - } - } - } - assert Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real) by { - calc { - Rand.prob(e); - { reveal Equal; } - Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n); - { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); } - (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real); - } - } - } // Correctness theorem for Model.IntervalSample lemma UniformFullIntervalCorrectness(a: int, b: int, i: int) @@ -160,16 +62,7 @@ module Uniform.Correctness { lemma SampleIsIndep(n: nat) requires n > 0 ensures Independence.IsIndep(Model.Sample(n)) - { - assert Independence.IsIndep(Model.Proposal(n)) by { - UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n); - } - assert Loops.UntilTerminatesAlmostSurely(Model.Proposal(n), Model.Accept(n)) by { - Model.SampleTerminates(n); - } - Loops.UntilIsIndep(Model.Proposal(n), Model.Accept(n)); - reveal Model.Sample(); - } + {} lemma IntervalSampleIsIndep(a: int, b: int) requires a < b diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index 5194468b..6cf5d5c1 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -18,24 +18,10 @@ module Uniform.Model { ************/ // Definition 49 - opaque ghost function Sample(n: nat): Monad.Hurd + opaque ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd) requires n > 0 - { - SampleTerminates(n); - Loops.Until(Proposal(n), Accept(n)) - } - - function Proposal(n: nat): Monad.Hurd - requires n > 0 - { - UniformPowerOfTwo.Model.Sample(2 * n) - } - - function Accept(n: nat): nat -> bool - requires n > 0 - { - (m: nat) => m < n - } + ensures Independence.IsIndep(h) + ensures forall s :: h(s).Result? ==> 0 <= h(s).value < n ghost function IntervalSample(a: int, b: int): (f: Monad.Hurd) requires a < b @@ -47,62 +33,11 @@ module Uniform.Model { Lemmas *******/ - lemma SampleTerminates(n: nat) - requires n > 0 - ensures - && Independence.IsIndep(Proposal(n)) - && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n))) - && Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n)) - { - assert Independence.IsIndep(Proposal(n)) by { - UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n); - } - var e := iset s | Loops.ProposalIsAccepted(Proposal(n), Accept(n))(s); - assert e in Rand.eventSpace by { - var ltN := iset m: nat | m < n; - var resultsLtN := Monad.ResultsWithValueIn(ltN); - assert e == Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN); - assert Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN) in Rand.eventSpace by { - assert Independence.IsIndep(UniformPowerOfTwo.Model.Sample(2 * n)) by { - UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n); - } - assert Measures.IsMeasurable(Rand.eventSpace, Monad.natResultEventSpace, UniformPowerOfTwo.Model.Sample(2 * n)) by { - Independence.IsIndepImpliesMeasurableNat(UniformPowerOfTwo.Model.Sample(2 * n)); - } - assert resultsLtN in Monad.natResultEventSpace by { - Monad.LiftInEventSpaceToResultEventSpace(ltN, Measures.natEventSpace); - } - } - } - assert Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n))) by { - assert Rand.prob(e) > 0.0 by { - assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n); - assert n <= NatArith.Power(2, NatArith.Log2Floor(2 * n)) by { - NatArith.NLtPower2Log2FloorOf2N(n); - } - calc { - Rand.prob(e); - == { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); } - n as real / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real); - > - 0.0; - } - } - } - assert Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n)) by { - Loops.EnsureUntilTerminates(Proposal(n), Accept(n)); - } - } - lemma SampleBound(n: nat, s: Rand.Bitstream) requires n > 0 requires Sample(n)(s).Result? ensures 0 <= Sample(n)(s).value < n - { - reveal Sample(); - SampleTerminates(n); - Loops.UntilResultIsAccepted(Proposal(n), Accept(n), s); - } + {} lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream) requires a < b diff --git a/src/Util/FisherYates/Correctness.dfy b/src/Util/FisherYates/Correctness.dfy index 74fc81fd..809bb8e6 100644 --- a/src/Util/FisherYates/Correctness.dfy +++ b/src/Util/FisherYates/Correctness.dfy @@ -13,6 +13,26 @@ module FisherYates.Correctness { import Independence import RealArith + /************ + Definitions + ************/ + + ghost function CorrectnessConstructEvent(xs: seq, p: seq, i: nat): iset + requires i <= |xs| + requires i <= |p| + { + iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..] + } + + ghost predicate CorrectnessPredicate(xs: seq, p: seq, i: nat) + requires i <= |xs| + requires i <= |p| + { + var e := CorrectnessConstructEvent(xs, p, i); + e in Rand.eventSpace + && Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) + } + /******* Lemmas *******/ @@ -59,10 +79,7 @@ module FisherYates.Correctness { requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b] requires |xs| == |p| requires multiset(p[i..]) == multiset(xs[i..]) - ensures - var e := iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]; - e in Rand.eventSpace - && Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) + ensures CorrectnessPredicate(xs, p, i) { var e := iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]; if |xs[i..]| <= 1 { @@ -80,10 +97,7 @@ module FisherYates.Correctness { requires |xs| == |p| requires multiset(p[i..]) == multiset(xs[i..]) requires |xs[i..]| <= 1 - ensures - var e := iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]; - e in Rand.eventSpace - && Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) + ensures CorrectnessPredicate(xs, p, i) { Model.PermutationsPreserveCardinality(p[i..], xs[i..]); var e := iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]; @@ -107,7 +121,7 @@ module FisherYates.Correctness { } } } - assert e in Rand.eventSpace && Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) by { + assert CorrectnessPredicate(xs, p, i) by { reveal NatArith.FactorialTraditional(); Rand.ProbIsProbabilityMeasure(); assert Measures.IsProbability(Rand.eventSpace, Rand.prob); @@ -130,10 +144,7 @@ module FisherYates.Correctness { requires |xs| == |p| requires multiset(p[i..]) == multiset(xs[i..]) requires |xs[i..]| > 1 - ensures - var e := iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]; - e in Rand.eventSpace - && Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) + ensures CorrectnessPredicate(xs, p, i) { Model.PermutationsPreserveCardinality(p[i..], xs[i..]); var e := iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]; @@ -183,8 +194,8 @@ module FisherYates.Correctness { BitStreamsInA(xs, p, i, j, h, A); } var ys := Model.Swap(xs, i, j); - var e' := iset s | Model.Shuffle(ys, i+1)(s).Result? && Model.Shuffle(ys, i+1)(s).value[i+1..] == p[i+1..]; - assert InductionHypothesis: e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) by { + var e' := CorrectnessConstructEvent(ys, p, i+1); + assert InductionHypothesis: CorrectnessPredicate(ys, p, i+1) by { assert multiset(ys[i+1..]) == multiset(p[i+1..]) by { InductionHypothesisPrecondition1(xs, ys, p, i, j); } @@ -227,14 +238,31 @@ module FisherYates.Correctness { assert DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by { DecomposeE(xs, ys, p, i, j, h, A, e, e'); } - assert e in Rand.eventSpace && Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) by { + assert CorrectnessPredicate(xs, p, i) by { reveal DecomposeE; reveal HIsIndependent; - reveal InductionHypothesis; reveal BitStreamsInA; - ProbabilityOfE(xs, p, i, j, h, A, e, e'); + assert e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) by { + assert e' in Rand.eventSpace by { + assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; } + assert e' == CorrectnessConstructEvent(ys, p, i+1); + } + calc { + Rand.prob(e'); + { assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; } + assert e' == CorrectnessConstructEvent(ys, p, i+1); } + 1.0 / (NatArith.FactorialTraditional(|ys|-(i+1)) as real); + { assert |xs| == |ys|; + assert |ys|-(i+1) == |xs|-(i+1); + assert NatArith.FactorialTraditional(|ys|-(i+1)) == NatArith.FactorialTraditional(|xs|-(i+1)); + assert (NatArith.FactorialTraditional(|ys|-(i+1)) as real) == (NatArith.FactorialTraditional(|xs|-(i+1)) as real); } + 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real); + } + } + ProbabilityOfE(xs, ys, p, i, j, h, A, e, e'); EInEventSpace(xs, p, h, A, e, e'); } + } lemma BitStreamsInA(xs: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset) @@ -285,6 +313,7 @@ module FisherYates.Correctness { if s in e { var zs := Model.Shuffle(xs, i)(s).value; assert zs[i..] == p[i..]; + assert h(s).Result?; var k := Uniform.Model.IntervalSample(i, |xs|)(s).value; Uniform.Model.IntervalSampleBound(i, |xs|, s); var s' := Uniform.Model.IntervalSample(i, |xs|)(s).rest; @@ -296,6 +325,7 @@ module FisherYates.Correctness { p[i]; zs[i]; zs'[i]; + { assert Model.ShuffleInvariancePredicatePointwise(ys', Model.Shuffle(ys', i+1)(s'), i); } ys'[i]; xs[k]; } @@ -328,7 +358,7 @@ module FisherYates.Correctness { Model.Shuffle(ys, i+1)(s').value[i..]; { SliceOfSequences(Model.Shuffle(ys, i+1)(s').value, i); } [Model.Shuffle(ys, i+1)(s').value[i]] + Model.Shuffle(ys, i+1)(s').value[i+1..]; - { assert Model.Shuffle(ys, i+1)(s').value[i] == ys[i]; } + { assert Model.ShuffleInvariancePredicatePointwise(ys, Model.Shuffle(ys, i+1)(s'), i); assert Model.Shuffle(ys, i+1)(s').value[i] == ys[i]; } [ys[i]] + Model.Shuffle(ys, i+1)(s').value[i+1..]; { assert ys[i] == xs[k]; } [xs[k]] + Model.Shuffle(ys, i+1)(s').value[i+1..]; @@ -448,17 +478,20 @@ module FisherYates.Correctness { reveal DecomposeE; } - lemma ProbabilityOfE(xs: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset, e: iset, e': iset) + lemma ProbabilityOfE(xs: seq, ys: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset, e: iset, e': iset) requires i <= |xs| requires i <= |p| requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b] requires |xs| == |p| requires multiset(p[i..]) == multiset(xs[i..]) requires i <= j < |xs| && xs[j] == p[i] + requires ys == Model.Swap(xs, i, j) requires |xs|-i > 1 + requires e' in Rand.eventSpace + requires |xs| == |ys| requires DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') requires HIsIndependent: Independence.IsIndepFunction(h) - requires InductionHypothesis: e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) + requires InductionHypothesis: Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) requires BitStreamsInA: Monad.BitstreamsWithValueIn(h, A) == (iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) ensures Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) diff --git a/src/Util/FisherYates/Model.dfy b/src/Util/FisherYates/Model.dfy index 4dda99a1..ff5fbe95 100644 --- a/src/Util/FisherYates/Model.dfy +++ b/src/Util/FisherYates/Model.dfy @@ -12,20 +12,41 @@ module FisherYates.Model { Definitions ************/ + ghost predicate ShuffleInvariancePredicatePointwise(xs: seq, r: Monad.Result>, j: int) + requires 0 <= j < |xs| + { + r.Result? ==> |r.value| == |xs| && r.value[j] == xs[j] + } + ghost function Shuffle(xs: seq, i: nat := 0): (h: Monad.Hurd>) requires i <= |xs| - decreases |xs| - i ensures forall s :: h(s).Result? ==> multiset(h(s).value) == multiset(xs) && |h(s).value| == |xs| - ensures forall s, j | 0 <= j < i :: h(s).Result? ==> h(s).value[j] == xs[j] + ensures forall s, j | 0 <= j < i :: ShuffleInvariancePredicatePointwise(xs, h(s), j) { - (s: Rand.Bitstream) => - if |xs[i..]| > 1 then - var (j, s') :- Uniform.Model.IntervalSample(i, |xs|)(s); - assert i <= j < |xs| by { Uniform.Model.IntervalSampleBound(i, |xs|, s); } - var ys := Swap(xs, i, j); - Shuffle(ys, i + 1)(s') - else - Monad.Return(xs)(s) + (s: Rand.Bitstream) => ShuffleCurried(xs, s, i) + } + + ghost function ShuffleCurried(xs: seq, s: Rand.Bitstream, i: nat := 0): (r: Monad.Result>) + requires i <= |xs| + decreases |xs| - i + ensures r.Result? ==> multiset(r.value) == multiset(xs) && |r.value| == |xs| + ensures forall j | 0 <= j < i :: ShuffleInvariancePredicatePointwise(xs, r, j) + { + if |xs| - i > 1 then + var (j, s') :- Uniform.Model.IntervalSample(i, |xs|)(s); + assert i <= j < |xs| by { Uniform.Model.IntervalSampleBound(i, |xs|, s); } + var ys := Swap(xs, i, j); + var r := ShuffleCurried(ys, s', i + 1); + assert forall j | 0 <= j < i :: ShuffleInvariancePredicatePointwise(xs, r, j) by { + forall j | 0 <= j < i + ensures ShuffleInvariancePredicatePointwise(xs, r, j) + { + assert ShuffleInvariancePredicatePointwise(ys, r, j); + } + } + r + else + Monad.Return(xs)(s) } function Swap(s: seq, i: nat, j: nat): (t: seq)