JarConfig: provides protocol configuration and validity proofs.
Used by struct types and Fin-based index aliases.
Extended by JarVariant (in Jar/Variant.lean) to add JAVM function fields.
Instance Constructor
Jar.JarConfig.mk
Methods
name : String
Variant name, e.g. "gp072_tiny", "gp072_full".
config : Params
valid : JarConfig.config.Valid
memoryModel : MemoryModel
PVM memory layout for program initialization.
gasModel : GasModel
PVM gas metering strategy.
capabilityModel : CapabilityModel
PVM capability model: .none = flat memory, .v2 = capability-based.
useCompactDeblob : Bool
PVM blob deblob encoding: true = JAM compact natural, false = u32 LE (jar1).
variableValidators : Bool
Whether validator set size is variable (GP#514). When true, designate hostcall accepts a length argument and active core count scales with validator count. Default false for gp072 variants.
EconType : Type
Economic model type for service accounts (BalanceEcon or QuotaEcon).
TransferType : Type
Transfer payload type (BalanceTransfer or QuotaTransfer).
econBEq : BEq JarConfig.EconType
BEq instance for economic model (required for state comparison).
econInhabited : Inhabited JarConfig.EconType
Inhabited instance for economic model (required for default construction).
xferBEq : BEq JarConfig.TransferType
BEq instance for transfer payload.
xferInhabited : Inhabited JarConfig.TransferType
Inhabited instance for transfer payload.
econRepr : Repr JarConfig.EconType
Repr instance for economic model (for debugging).
xferRepr : Repr JarConfig.TransferType
Repr instance for transfer payload (for debugging).
econModel : EconModel JarConfig.EconType JarConfig.TransferType
EconModel instance linking EconType and TransferType.