-
Notifications
You must be signed in to change notification settings - Fork 5
Circuitous IR
Circuitous IR is still unstable - node types can still change (there will be some additions for sure, removals are not happening very often).
Current structure is as follows bitsize name - comments:
1 used - flag whether hint is used
1 mode - whether hint serves as read or write
6 reserved
4 id - internal id of memory hint - so they can be ordered
4 size - size of the value that is read/written (trunc or extension can be applied based on this)
PTR addr
PTR value
64 timestamp - current timestamp
Since circuitous can already also support 64bit, the memory hint must reflect this - PTR is either 32 or 64 depending on architecture.
Here is an incomplete list of node types used inside the circuits.
For a complete look please look at include/circuitous/IR/IR.hpp.
There are three kinds of storage, registers, memory locations, and constants
Registers are fixed-size storage units, these are either in or out registers depending on their role.
They follow the following naming scheme: [In|Out].register.<register_name>. i.e the output register for rax is Out.register.RAX.
Note that specific flag values tend to have their own registers.
TODO
Constants are variable-length integer values, internally they hold their value as a string of bits.
Their naming scheme is CONST_<LEN>_VALUE
Notice that VALUE has its most significant bit at the first index (Big endian). Which is in contrast to instruction_bits/extract nodes.
This is a special node holding the value of the instruction pointer. These are also named instruciton_bits.
The value of this node is formatted as a sequence of little-endian bytes.
i.e
- instruction_bits[0] -> lsb for first byte
- instruction_bits[7] -> msb for first byte
- instruction_bits[8] -> lsb for second byte
These address a range inside from <low inclusive> to <high_exlcusive> inside instruction_bits.
Naming scheme: Extract.<hi_excl>.<low_incl>
We support the following arithmetic nodes which we shadow from LLVM IR.
Add, Sub, Mul, UDiv, SDiv, Shl, LShr, AShr, Trunc, ZExt, SExt, Icmp_ult, Icmp_slt, Icmp_ugt, Icmp_eq, Icmp_ne, Icmp_uge, Icmp_ule, Icmp_sgt, Icmp_sge, Icmp_sle, SRem, URem, Xor, And, Or
Constraint nodes are used to represent equality across nodes.
For example, if we want the circuit to only evaluate to true if rax = 2,
we can put a constraint node on top of the register connected to a constant node of 2.
Currently, we sub-type constraints based on their function. This is mainly for convenience during the search for specific nodes. Supported constraints:
- RegisterConstraint
- AdviceConstraint
- ReadConstraint
- WriteConstraint
- UnusedConstraint
Read and Write constraints are only concerned with the reading/writing of memory.
Conditions are specialized forms of constraints in that they do not strictly represent equality. We got 4 Conditions:
This node is used to represent the successful decoding of a context.
It acts as a AND node with an arbitrary number of operands, meaning it returns true if all operands return true.
This node represents an XOR and can take an arbitrary number of operands
Akin to VerifyInstruction, this node is an AND node containing all conditions for identifying whether the instruction located in instruction_bits corresponds to an instruction represented by the context containing DecoderResult
This node checks if two nodes are of equal value, typically these nodes only have a CONST and Extract node as operands.
Advice nodes are meant to inverse the dependencies of nodes. They can be best seen as a temp variable that will be set through an advice_constraint.
Select are the equivalent of multiplexers. It is assumed that it has (2^x)+1 operands.
The first operand should be a value of 2^x and indicates the index which should be selected.
[in|out].timestamp related to trace info, can be seen as another register.
[in|out].error_flag saves whether there was an error, also relates to trace info.
Circuit Root of the tree indicating successful execution