Anomaly with `rnd`

[chdoc]

The following produces an
anomaly: File "src/ecUtils.ml", line 233, characters 24-30: Assertion failed

require import AllCore.

type r_t, c_t.

op[lossless] dC : c_t distr.

op p : c_t -> bool.

module M = { 
  proc p1() = { 
    var e1,e2 <- true;
    var k1,k2 <- 0;
    var r,c <- witness;
    while(e1) { 
      c <$ dC;
      k1 <- k1 + 1;
      if (p c) { e1 <- false; r <- c; }
    }
    return (k1,k2,r);
  }
}.

module F = { 
  proc p1'(i1') = { 
    var e1,e2 <- true;
    var k1,k2 <- 0;
    var r,c <- witness;
    while(e1 /\ k1 < i1') { 
      c <$ dC;
      k1 <- k1 + 1;
      if (p c) { e1 <- false; r <- c; }
    } 
    c <$ dC;  
    if(e1) { 
      k1 <- k1 + 1;
      if (p c) { e1 <- false; r <- c; }
    }
    while(e1) { 
      c <$ dC;
      k1 <- k1 + 1;
      if (p c) { e1 <- false; }
    }
    return (k1,k2,r);
  }
}.

lemma eqv_p1_p2 i1 : 
  0 <= i1 => equiv [ M.p1 ~ F.p1' : arg{2} = i1 ==> ={res} ].
move => il_ge0.
proc. 
splitwhile{1} 7 : k1 < i1.
unroll{1} 8. 
seq 7 7 : (={e1,e2,k1,k2,r,c} /\ (e1 => k1 = i1){1} /\ i1'{2} = i1).
while (={e1,e2,k1,k2,r,c} /\  i1'{2} = i1 /\ 0 <= k1{1} <= i1).
(* auto. same anomaly *)
wp. 
rnd.

[chdoc]

Okay, looking at this again, here is a simplified example exhibiting the same problem:

require import AllCore.

type r_t, c_t.

op[lossless] dC : c_t distr.

op p : c_t -> bool.

module M = { 
  proc p1() = { 
    var e1 <- true;
    var c <- witness;
    while(e1) { 
      c <$ dC;
      if (p c) { e1 <- false; } 
    }
    return c;
  }
}.

equiv foo : M.p1 ~ M.p1 : true ==> ={res}.
proc. 
while (={e1,c}). 
wp. 
rnd. (* anomaly *)

Looks like EC really doesn't like random sampling in while loops ^^

[chdoc]

Okay, as suggested by @strub , require import Distr sidesteps the issue. But then something else is strange with the lossless tag:

require import AllCore.
type c_t.
op[lossless] dC : c_t distr.
print dC_ll.
require import Distr.
print dC_ll.

What is the Top.Distr.is_lossless used by the lossless tag if AllCore is required but Distr is not? If AllCore isn't loaded, an error asking to load Distr is produced.