Constant-time & randombytes

[vbgl]

Is the following program secure (w.r.t. the constant-time policy)?

export
fn main() -> #secret reg u64 {
  stack u64[1] s;
  reg u64 r;
  s = #randombytes(s);
  r = s[0];
  while (r < 64) {
    r += 64;
  }
  return r;
}

jasminc -checkCT claims its OK.