Pass `Globals` externally to the executable spec instead of hardcoding

The implementation uses a `Globals` record for storing certain global values, such as `SlotsPerEpoch`, `SecurityParameter` etc. Right now the spec hard-codes those values in the `Implementation` data structure but it would be better if those values were passed from the implementation instead, perhaps with the `ExternalFunctions` record.