Hi Mathias, Nice detective work! I just loaded this up on the CI, so we'll see if this does work across the board.
It sounds like the original code also had this bug -- the "r"(out) should be in the output constraints, not in the input constraints, right? Sounds like something I should report to the EverCrypt authors and also fix upstream too then. Jason
