L2 · OPERATIONMEASURED

Encrypted Byte Extraction

encrypted-byte · spec v0.1.0 · 0 implementations · 6 runners

Create implementationSpecification

DESCRIPTION

Returns the byte at position i of an encrypted word, counting from the most significant end as the EVM does.

It is a lookup where the table is the word itself. Since nothing can address a position chosen by encrypted data, a realization touches every byte and combines them so only the selected one survives — the same shape as encrypted table lookup, at the scale of a single word.

INTERFACE

encrypted_byte(
  in  ct     : Ciphertext  // the encrypted first operand
  in  ct_i   : Ciphertext  // the encrypted byte position
  out ct     : Ciphertext  // the encrypted result of the opcode
  ...               // anything else the realization needs — keys, context, encoding — is its own concern
)

PARAMETER SCHEMA

NAMETYPERANGE

word_maxinteger255 – 2^32

target_precisionnumber0.5 – 1

The schema belongs to the kernel. Each implementation declares which part of it it supports.

CORRECTNESS

01The result is the selected byte, zero-extended to a full word.

02A position beyond the width of the word yields zero, as the EVM defines.

03The result matches the EVM definition of the opcode exactly, including its behaviour at the boundaries.

An opcode is exact by definition. Where the scheme is approximate, the precision threshold is what stands in for exactness, and it has to hold at every integer in range.

SECURITY PROPERTIES

Operands and result stay encrypted throughout. Nothing about the values may be observable through timing or control flow, which rules out any realization that branches on a decrypted intermediate.

ASSUMPTIONS

Operands are integers held exactly at the point of encryption.

REFERENCES

repoFHERMA participation guide