error in the paper, chapter 4.1, deferred return:

transformed code, but insecure

    secret mut uint32 rval = 0;
    secret mut bool notRet = true;
    if (sec) { rval = 1; notRet = false; }
    if (notRet) {
    // long-running computation ...
    }
    return rval;

the long running block depends on the secret, thus leaks it.