JAR: Join-Accumulate Refine

9.2. Constants🔗

🔗def
Jar.JAVM.numRegisters : Nat
Jar.JAVM.numRegisters : Nat

Number of general-purpose registers.

🔗def
Jar.JAVM.pageSize : Nat
Jar.JAVM.pageSize : Nat

Page size in bytes. Z_P = 2^12. GP §4.6.

🔗def
Jar.JAVM.memorySize : Nat
Jar.JAVM.memorySize : Nat

Total addressable memory: 2^32 bytes.

🔗def
Jar.JAVM.numPages : Nat
Jar.JAVM.numPages : Nat

Number of pages: 2^32 / Z_P.

🔗def
Jar.JAVM.initZoneStart : Nat
Jar.JAVM.initZoneStart : Nat

First accessible address: Z_Z = 2^16. GP §4.6.

🔗def
Jar.JAVM.maxInitInput : Nat
Jar.JAVM.maxInitInput : Nat

Maximum input size for standard initialization: Z_I = 2^24.