This is Jasmin, with all theorems proved

Generic functions, branched from glob_array3

Preservation of the Constant-Time security property

Branched from master on 2020-02-13, following release-21

Checking for speculative safety and speculative constant-time

Cost analysis of low-level Jasmin programs using precise models of the micro-architecture

Use dpdgraph to find dead code and unused lemmas.