Lightweight formal verification requires the use of a workload generator that can cover all relevant code paths with a high enough probability. This is an approximation to model-checking in the traditional formal verification, which deterministically tests all possible code paths. But as we don't use a formal language, we can't actually do that. The first step in building such workload generator is to define an alphabet of operations. (Workload operations in the literature are called symbols, and the set of all possible symbols is thus called an alphabet.)

In this ticket, we'll represent the set of operations in a format that is well-suited for workload generation, which we will then implement in WT-11621.