From 08aef4e22e0ebce7ccd305036b3a9a15e7e2b26b Mon Sep 17 00:00:00 2001
From: dan <70999565+belovdv@users.noreply.github.com>
Date: Fri, 25 Sep 2026 14:32:37 +0300
Subject: [PATCH 1/3] wip

---
 docs/stmts.md | 525 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 525 insertions(+)
 create mode 100644 docs/stmts.md

diff --git a/docs/stmts.md b/docs/stmts.md
new file mode 100644
index 0000000..d5e083c
--- /dev/null
+++ b/docs/stmts.md
@@ -0,0 +1,525 @@
+# Statements
+
+Semantic for standard statement kinds in pseudocode
+
+This text assumes a general understanding of LIRA IR
+
+## Environment
+
+```python
+# Vector of Bit Vectors
+class Value:
+    bit_width: int
+    values: list[int]
+
+# Constant
+class Context:
+    dyn_consts: dict[str, int]
+    snippets: dict[str, StatementSeq]
+    operations: dict[str, ContextOperation]
+    environment_functions: dict[str, ContextEnvironmentFunction]
+    float_operations: dict[str, _]
+    ...
+
+# Mutable
+class State:
+    pc: int
+    set_pc: OnceInit[int]
+    registers: dict[str, StateRegFile]
+    system_registers: dict[str, StateSystemRegister]
+    ... # e.g. Memory, FPU
+class StateRegFile:
+    size: int # Full size, shape.instantiate(dyn_consts)
+    values: list[int]
+    def read(self, idx: int, shape: int, ty: int) -> Value:
+        assert self.size == shape * ty
+        idx = idx % self.values.len()
+        return reinterpret(self.values[idx], shape, ty)
+    def write(self, idx: int, value: Value):
+        assert self.size == value.shape * value.bit_width
+        idx = idx % self.values.len()
+        self.values[idx] = reinterpret(value, value.shape, value.bit_width)
+
+class StmtExecCtx:
+    shape: int
+    specifier: str
+    stmt_inputs: list[Value]
+    stmt_outputs_types: list[int]
+    snippet_inputs: list[Value]
+    snippet_outputs: list[OnceInit[Value]]
+    context: Context
+    state: State
+
+    def alloc_outputs(self) -> list[Value]:
+        return [Value(ty, []) for ty in self.stmt_outputs_types]
+
+def execute_statement_sequence(
+    context: Context,
+    state: State,
+    stmts: StatementSeq,
+    snippet_inputs: list[Value],
+    snippet_outputs: list[OnceInit[Value]],
+):
+    values = {}
+    for stmt in stmts:
+        stmt_shape = stmt.shape.instantiate(context.dyn_consts)
+        stmt_inputs = [values[name] for name in stmt.inputs]
+        ctx = StmtExecCtx(
+            stmt_shape,
+            stmt.specifier,
+            stmt_inputs,
+            stmt.outputs_types,
+            snippet_inputs,
+            snippet_outputs,
+            context,
+            state,
+        )
+        stmt_outputs = (semantic(stmt.kind))(ctx)
+        # Note: these two guarantees don't have to be checked in semantics
+        #   Tbd: outline more checks
+        assert all(shape(output) == stmt_shape for output in stmt_outputs)
+        assert types(stmt_outputs) == stmt.outputs_types
+        for name, value in zip(stmt.outputs, stmt_outputs):
+            values.insert_new(name, value)
+    assert all(output.initialized() for output in snippet_outputs)
+```
+
+Different execution contexts:
+- `Context/State` are collections of interpretation-specific data.
+- Statement kinds (including standard ones) can assume presence of specific data in `Context/State`.
+- Not every `Context/State` should include everything, if statement kind requires data that is not available - this statement is invalid in the given context.
+  - Example: `State` for execution of `Operation.semantic_func` must be empty (operation is a pure function by definition).
+- Given `Context/State` definitions contain union of fields required by standard statements.
+
+### Notation
+
+- `Value(bit_width, lanes)` constructs a vector of `lanes` bit-vectors of `bit_width` bits each.
+- `value[i]` is sugar for `value.values[i]`.
+- `shape(value)` is sugar for `len(value.values)`.
+- `types(values) -> list[int]` returns bit widths of the given values.
+- `(a, b) = inputs` is used as an arity check: it panics if the number of inputs differs.
+- `OnceInit[T]` is a single-assignment slot with `.set_first_time(value)` and `.initialized()`.
+- `insert_new` assert key was not present
+- `parse_int`: todo: should this be limited to positive decimal number?
+
+## Semantics
+
+TODO: grouping feels off
+
+### Utils
+
+#### Cond prefix
+
+While the exact interpretation of `cond.` prefix varies between statement kinds, there's a general rule of input values interpretation.
+
+```python
+def cond_prefix_split(
+    inputs: list[Value],
+    output_types: list[int],
+    shape: int,
+) -> tuple[Value, list[Value], list[Value]]:
+    cond = inputs[0]
+    assert cond.bit_width == 1
+    assert shape(cond) == shape
+    on_false = inputs[1:][:len(output_types)]
+    inputs = inputs[1:][len(output_types):]
+    assert len(on_false) == len(output_types)
+    assert all(shape(of) == shape for of in on_false)
+    assert types(on_false) == output_types
+    return cond, on_false, inputs
+```
+
+### General semantics
+
+#### Input
+
+```python
+def semantic_input(ctx: StmtExecCtx) -> list[Value]:
+    () = ctx.stmt_inputs
+    input_id = parse_int(ctx.specifier)
+    input_value = ctx.snippet_inputs[input_id]
+    return [input_value]
+```
+
+#### Output
+
+```python
+def semantic_output(ctx: StmtExecCtx) -> list[Value]:
+    assert ctx.shape == 1
+    (value,) = ctx.stmt_inputs
+    output_id = parse_int(ctx.specifier)
+    ctx.snippet_outputs[output_id].set_first_time(value)
+    return []
+```
+
+#### Const
+
+```python
+def semantic_const(ctx: StmtExecCtx) -> list[Value]:
+    () = ctx.stmt_inputs
+    (ty,) = ctx.stmt_outputs_types
+    value = parse_int(ctx.specifier)
+    return [Value(ty, [value] * ctx.shape)]
+```
+
+#### Dyn Const
+
+```python
+def semantic_dyn_const(ctx: StmtExecCtx) -> list[Value]:
+    () = ctx.stmt_inputs
+    (ty,) = ctx.stmt_outputs_types
+    value = ctx.context.dyn_consts[ctx.specifier]
+    return [Value(ty, [value] * ctx.shape)]
+```
+
+#### Snippet
+
+```python
+def semantic_snippet(ctx: StmtExecCtx) -> list[Value]:
+    outputs = [OnceInit() for _ in ctx.stmt_outputs_types]
+    execute_statement_sequence(
+        ctx.context,
+        ctx.state,
+        ctx.context.snippets[ctx.specifier],
+        ctx.stmt_inputs,
+        outputs
+    )
+    return [output.value() for output in outputs]
+```
+
+#### Cond PC
+
+TODO: should `read/write` be a part of statement kind?
+- For consistency with registers
+
+```python
+def semantic_cond_pc(ctx: StmtExecCtx) -> list[Value]:
+    assert ctx.shape == 1
+    (cond, on_false, inputs) = cond_prefix_split(ctx.stmt_inputs, ctx.stmt_outputs_types, ctx.shape)
+    if ctx.specifier == 'read':
+        () = inputs
+        if cond:
+            return [ctx.state.read_pc()]
+        else:
+            return on_false
+    elif ctx.specifier == 'write':
+        (value,) = inputs
+        if cond:
+            ctx.state.write_pc(value)
+        return []
+    else:
+        panic
+```
+
+#### Cond SysReg Read/Write
+
+```python
+def semantic_cond_sys_reg_read(ctx: StmtExecCtx) -> list[Value]:
+    '''
+    Implementation-defined
+    similar to `cond.pc.read` get value of system register or return provided default
+    '''
+    (cond, on_false, inputs) = cond_prefix_split(ctx.stmt_inputs, ctx.stmt_outputs_types, ctx.shape)
+    (sys_reg_id,) = inputs
+
+def semantic_cond_sys_reg_write(ctx: StmtExecCtx) -> list[Value]:
+    '''
+    Implementation-defined
+    similar to `cond.pc.write` set value of system register if cond
+    '''
+    (cond, on_false, inputs) = cond_prefix_split(ctx.stmt_inputs, ctx.stmt_outputs_types, ctx.shape)
+    (sys_reg_id, value) = inputs
+```
+
+### Lane-wise semantics
+
+TODO: it should be possible to outline smth like this
+- Note: cond prefix is used the same way for lanewise semantics
+
+```python
+def execute_semantic_lanewise(
+    ctx: StmtExecCtx,
+    semantic: Callable[[StmtExecCtx, list[Value]], list[Value]]
+) -> list[Value]:
+    assert all(shape(value) == ctx.shape for value in ctx.stmt_inputs)
+    outputs = ctx.alloc_outputs()
+    for lane in range(ctx.shape):
+        stmt_inputs = [stmt_input[lane] for stmt_input in ctx.stmt_inputs]
+        stmt_outputs = semantic(ctx, stmt_inputs)
+        assert types(stmt_outputs) == ctx.stmt_outputs_types
+        for j in range(len(outputs)):
+            outputs[j].values.append(stmt_outputs[j])
+    return outputs
+```
+
+#### Op
+
+```python
+def semantic_op(ctx: StmtExecCtx) -> list[Value]:
+    inputs = ctx.stmt_inputs
+    assert all(ctx.shape == shape(value) for value in inputs)
+    op = ctx.context.operations[ctx.specifier]
+    assert types(inputs) == op.inputs
+
+    outputs = ctx.alloc_outputs()
+    for lane in range(ctx.shape):
+        result = op.eval([value[lane] for value in inputs])
+        add_new_lane(outputs, result)
+    return outputs
+```
+
+#### FOp
+
+```python
+def semantic_fop(ctx: StmtExecCtx) -> list[Value]:
+    inputs = ctx.stmt_inputs
+    assert all(ctx.shape == shape(value) for value in inputs)
+    fop = ctx.context.float_operations[ctx.specifier]
+    assert types(inputs) == fop.inputs
+
+    outputs = ctx.alloc_outputs()
+    for lane in range(ctx.shape):
+        result = fop.eval(ctx.Context, ctx.State, [value[lane] for value in inputs])
+        add_new_lane(outputs, result)
+    return outputs
+```
+
+#### Env
+
+```python
+def semantic_env(ctx: StmtExecCtx) -> list[Value]:
+    inputs = ctx.stmt_inputs
+    assert all(ctx.shape == shape(value) for value in inputs)
+    env = ctx.context.environment_functions[ctx.specifier]
+    assert types(inputs) == env.inputs
+
+    outputs = ctx.alloc_outputs()
+    for lane in range(ctx.shape):
+        result = env.eval(ctx.context, ctx.state, [value[lane] for value in inputs])
+        add_new_lane(outputs, result)
+    return outputs
+```
+
+#### Cond Env
+
+```python
+def semantic_cond_env(ctx: StmtExecCtx) -> list[Value]:
+    (cond, on_false, inputs) = cond_prefix_split(ctx.stmt_inputs, ctx.stmt_outputs_types, ctx.shape)
+    assert all(ctx.shape == shape(value) for value in inputs)
+    env = ctx.context.environment_functions[ctx.specifier]
+    assert types(inputs) == env.inputs
+
+    outputs = ctx.alloc_outputs()
+    for lane in range(ctx.shape):
+        if cond[lane]:
+            result = env.eval(ctx.context, ctx.state, [value[lane] for value in inputs])
+        else:
+            result = on_false[0][lane]
+        add_new_lane(outputs, result)
+    return outputs
+```
+
+#### Read
+
+```python
+def semantic_read(ctx: StmtExecCtx) -> list[Value]:
+    inputs = ctx.stmt_inputs
+    (rsi,) = inputs
+    assert shape(rsi) == 1
+    rf = ctx.state.registers[ctx.specifier]
+    (ty,) = ctx.stmt_outputs_types
+    result = rf.read(rsi[0], ctx.shape, ty)
+    return [result]
+```
+
+#### Cond Read
+
+```python
+def semantic_cond_read(ctx: StmtExecCtx) -> list[Value]:
+    (cond, on_false, inputs) = cond_prefix_split(ctx.stmt_inputs, ctx.stmt_outputs_types, ctx.shape)
+    (rsi,) = inputs
+    assert shape(rsi) == 1
+    rf = ctx.state.registers[ctx.specifier]
+    (ty,) = ctx.stmt_outputs_types
+    result = rf.read(rsi[0], ctx.shape, ty)
+    for lane in range(ctx.shape):
+        if not cond[lane]:
+            result.values[lane] = on_false[0][lane]
+    return [result]
+```
+
+#### Write
+
+```python
+def semantic_write(ctx: StmtExecCtx) -> list[Value]:
+    inputs = ctx.stmt_inputs
+    (rsi, value) = inputs
+    assert shape(rsi) == 1
+    assert shape(value) == ctx.shape
+    rf = ctx.state.registers[ctx.specifier]
+    rf.write(rsi[0], value)
+    return []
+```
+
+#### Cond Write
+
+```python
+def semantic_cond_write(ctx: StmtExecCtx) -> list[Value]:
+    (cond, on_false, inputs) = cond_prefix_split(ctx.stmt_inputs, ctx.stmt_outputs_types, ctx.shape)
+    (rsi, value) = inputs
+    assert shape(rsi) == 1
+    assert shape(value) == ctx.shape
+    rf = ctx.state.registers[ctx.specifier]
+    value_on_false = rf.read(rsi[0], ctx.shape, value.bit_width)
+    for lane in range(ctx.shape):
+        if not cond[lane]:
+            value.values[lane] = value_on_false[lane]
+    rf.write(rsi[0], value)
+    return []
+```
+
+### Vector semantics
+
+#### Replicate
+
+```python
+# TODO: rename into broadcast?
+# Note: can be expressed as `gather(value, 0, _)`
+def semantic_replicate(ctx: StmtExecCtx) -> list[Value]:
+    inputs = ctx.stmt_inputs
+    (value,) = inputs
+    assert shape(value) == 1
+    return [Value(value.bit_width, [value[0]] * ctx.shape)]
+```
+
+#### Index
+
+```python
+def semantic_index(ctx: StmtExecCtx) -> list[Value]:
+    () = ctx.stmt_inputs
+    (ty,) = ctx.stmt_outputs_types
+    return [Value(ty, list(range(ctx.shape)))]
+```
+
+#### Extract First
+
+```python
+# Note: can be expressed as `gather(value, index, _)`
+def semantic_extract_first(ctx: StmtExecCtx) -> list[Value]:
+    (value,) = ctx.stmt_inputs
+    assert shape(value) >= ctx.shape
+    value.values = value.values[:ctx.shape]
+    return [value]
+```
+
+#### Extend Zero
+
+```python
+# Note: can be expressed as `gather(value, index, 0)`
+def semantic_extend_zero(ctx: StmtExecCtx) -> list[Value]:
+    (value,) = ctx.stmt_inputs
+    assert shape(value) <= ctx.shape
+    value.values.extend_with(ctx.shape, 0)
+    return [value]
+```
+
+#### Extend Ones
+
+```python
+# Note: can be expressed as `gather(value, index, 1)`
+def semantic_extend_ones(ctx: StmtExecCtx) -> list[Value]:
+    (value,) = ctx.stmt_inputs
+    assert shape(value) <= ctx.shape
+    # Note: this can be relaxed in future
+    assert value.bit_width == 1
+    value.values.extend_with(ctx.shape, 1)
+    return [value]
+```
+
+#### Gather
+
+```python
+def semantic_gather(ctx: StmtExecCtx) -> list[Value]:
+    (val, idx, on_false) = ctx.stmt_inputs
+    # Note: val can have different shape
+    assert shape(idx) == shape(on_false) == ctx.shape
+    (ty,) = ctx.stmt_outputs_types
+    result = []
+    for lane in range(ctx.shape):
+        if idx[lane] < shape(val):
+            result.append(val[idx[lane]])
+        else:
+            result.append(on_false[lane])
+    return [Value(ty, result)]
+```
+
+#### CVI
+
+```python
+# Note: reverse of gather
+# Note: ideally should not be used: it's bad for both formal analysis and hardware implementation
+# Name: Conditional Vector Insert (or cond value index)
+def semantic_cvi(ctx: StmtExecCtx) -> list[Value]:
+    (base, cond, value, index) = ctx.stmt_inputs
+    assert shape(base) == ctx.shape
+    assert shape(cond) == shape(value) == shape(index)
+    for lane in range(shape(cond)):
+        if cond[lane]:
+            if index[lane] < shape(base):
+                base[index[lane]] = value[lane]
+    return [base]
+```
+
+#### Scan/Fold
+
+```python
+def semantic_scan(ctx):
+    return semantic_scan_fold('scan', ctx)
+def semantic_fold(ctx):
+    return semantic_scan_fold('fold', ctx)
+def semantic_scan_fold(kind: str, ctx: StmtExecCtx) -> list[Value]:
+    op = ctx.context.operations[ctx.specifier]
+
+    # First `width` inputs (at least one) are scalars
+    width = 0
+    while shape(ctx.stmt_inputs[width]) != 1:
+        width += 1
+    # All other inputs (at least one) have same non-scalar shape
+    vec_shape = shape(ctx.stmt_inputs[width])
+    for lane in range(width, len(ctx.stmt_inputs)):
+        assert vec_shape == shape(ctx.stmt_inputs[lane])
+
+    inputs_scalar, inputs_vector = ctx.stmt_inputs.split_at(width)
+
+    # Initialize state with scalar inputs
+    # For each lane of vector inputs
+    #   Evaluate operation on state and new part of input
+    #   Split result of operation into new state and new output
+    state = inputs_scalar
+    outputs = ctx.alloc_outputs()
+    for lane in range(vec_shape):
+        inputs_vector_part = [value[lane] for value in inputs_vector]
+        inputs_current = list(chain(state, inputs_vector_part))
+        values = op.eval(inputs_current)
+        new_state, new_outputs = values.split_at(width)
+        state = new_state
+        for i in range(len(outputs)):
+            outputs[i].values.append(new_outputs[i])
+
+    # Note: joining these two requires one statement to produce values with different shape.
+    #   At the moment of writing this is not supported for the sake of simplicity,
+    #   since it was never needed in practice.
+    #   (Note: same with shape - there was no need in making it multidimensional)
+    if kind == 'scan':
+        # Note: final state is ignored
+        return outputs
+    if kind == 'fold':
+        # Note: outputs are ignored. Normally, for `fold` there should be 0 of them
+        return state
+```
+
+#### Suggestions
+
+##### Cast/Reinterpret
+
+##### Concat

From f6d3bc94e8d7ef2cc6563afb5dbcf6a9578be125 Mon Sep 17 00:00:00 2001
From: dan <70999565+belovdv@users.noreply.github.com>
Date: Fri, 25 Sep 2026 18:03:36 +0300
Subject: [PATCH 2/3] wip: operations

---
 docs/ops.md | 149 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 149 insertions(+)
 create mode 100644 docs/ops.md

diff --git a/docs/ops.md b/docs/ops.md
new file mode 100644
index 0000000..156fd8c
--- /dev/null
+++ b/docs/ops.md
@@ -0,0 +1,149 @@
+# Operations
+
+List of standard operation bases, their signature and semantic.
+
+Arithmetic: `add`, `sub`, `mul`, `neg`, `div_s`, `div_u`, `rem_s`, `rem_u`
+
+Comparators: `eq`, `ne`, `ugt`, `uge`, `ult`, `ule`, `sgt`, `sge`, `slt`, `sle`
+
+Overflow: `add_s_overflow`, `add_u_overflow`, `sub_s_overflow`, `sub_u_overflow`
+
+Bitwise: `and`, `orr`, `xor`, `not`
+
+Shifts: `lsl`, `lsr`, `asr`
+
+Others:
+- `clz`, `ctz`, `cnt`, `rev`, `rol`, `ror`
+- `extend_zero`, `extend_sign`, `extract_low`
+- `insert`, `extract`, `orr_shifted`
+- `concat_hi_lo`
+- `select`
+
+## Signature
+
+Basic operation is parametrized by a list of variables, they can have positive integer value.
+Suggested way to name concrete operations is to use `<base> <"_" param value>*` name e.g. `add_18`
+
+Signature is written in a form `<const/variable>+ "<-" <const/variable>+`, e.g. `1 <- n n`.
+
+Some operations also have constraint on allowed values, e.g. `n <- m with n <= m`.
+
+Note, that this way directly translates in a following way to define and constraint operation:
+```python
+interface BasicOperation:
+    params_num: int
+    # Note: these have to be constants (no arbitrary-number inputs)
+    outputs_num: int
+    inputs_num: int
+    # Usually not needed
+    def check_constraint(params: list[int]) -> bool:
+        return True
+    # Note: this should be a total function, which correctness is guaranteed on a valid inputs
+    # Note: `list[ty; len]` notation is used to write a type `list with len elements`
+    def parse(outputs: list[int], inputs: list[int]) -> list[int; self.params_num]:
+    # Translate params to the signature
+    def signature(params: list[int]) -> tuple[list[int], list[int]]:
+
+# This is enough to implement
+def is_signature_valid(base: BasicOperation, outputs: list[int], inputs: list[int]) -> bool:
+    params = base.parse(outputs, inputs)
+    expected = base.signature(params)
+    return expected == (outputs, inputs) and base.check_constraint(params)
+```
+Usually, defining this set of functions is way more concise, than explicitly validating concrete signature.
+The form to present signature, specified above, is trivially convertible to implementation of this interface.
+
+### Signatures
+
+Unary: `n <- n`:
+- `neg`, `not`, `clz`, `ctz`, `cnt`, `rev`
+
+Binary: `n <- n n`:
+- `add`, `sub`, `mul`, `rem_s`, `rem_u`
+- `and`, `orr`, `xor`
+- `lsl`, `lsr`, `asr`
+- `ror`, `rol`
+
+Ternary: `n <- n n n`:
+- `div_s`, `div_u`
+
+Cmp: `1 <- n n`:
+- `eq`, `ne`, `ugt`, `uge`, `ult`, `ule`, `sgt`, `sge`, `slt`, `sle`
+- `add_s_overflow`, `add_u_overflow`, `sub_s_overflow`, `sub_u_overflow`
+
+Select: `n <- 1 n n`
+- `select`
+
+Constrained:
+- `n <- m with n <= m`: `extract_low`
+- `n <- m with n >= m`: `extend_zero`, `extend_sign`
+- `n <- n m n with m <= n`: `insert`, `orr_shifted`
+- `n <- m m with n <= m`: `extract`
+- `n <- m l with n = m + l`: `concat_hi_lo`
+
+Note: in some cases (`xor_1` with `1 <- n n`) concrete operation can be parsed with different signatures, code should not rely on the opposite
+
+## Semantic
+
+Semantic is explicitly written in cases there different interpretations are widely used.
+
+It's based on integer representation. Conversion between bit vectors and integers assumes standard two's complement representation:
+- `bv2s`: bit vector as signed integer
+- `bv2u`: bit vector as unsigned integer
+- `i2bv`: integer to bit vector
+
+Conventions:
+- `bv2i` is used in case signedness of conversion doesn't matter
+- `*` is used in place there exact number doesn't influence the result
+- final `i2bv` is omitted
+  - bool is treated as a bit vector of length one
+
+
+Example: `add(a, b) = bv2i(a) + bv2i(b)`, here `a` and `b` have types `BV<n>`, result of expression is `int`, but it's assumed to be converted with `i2bv` back to bit vector. Note, that this is a standard wrapping behavior definition.
+
+Arithmetic:
+- `div_s(a, b, d) = if b != 0 then bv2s(a) / bv2s(b) else d`
+  - `div_u` is the same with `bv2u`
+  - Note: this provides `div_s(INT_MIN, -1, *) = INT_MIN`
+- `rem_s(a, b) = a - b * div_s(a, b, *)`
+  - `rem_u` is the same with `bv2u`
+  - Note: this provides normal behavior of remainder, except `rem(a, 0) = a`
+
+Comparators:
+- `eq`, `ne`: equal and not equal
+- `<signedness><greater/less><than/than or equal>`, e.g `uge`: unsigned greater than or equal: `>=`
+
+Overflow:
+- `add_s_overflow(a, b) = (bv2s(a) + bv2s(b)) != bv2s(i2bv(bv2s(a) + bv2s(b)))`
+  - i.e. if limitation of finite bit vector representation cause wrong result
+  - same for others with signedness and operation set correspondingly
+
+Shifts:
+- `lsl(a, b) = bv2u(a) * 2^bv2u(b)`
+  - Note: this provides `lsl(a, huge number) = 0`
+- `lsr(a, b) = bv2u(a) / 2^bv2u(b)`
+  - Note: this provides `lsr(a, huge number) = 0`
+- `asr(a, b) = bv2s(a) / 2^bv2u(b)`
+  - Note: this provides `asr(a, huge number) = replicate sign bit`
+  - Note: `b` is treated as unsigned
+
+Others:
+- `clz`, `ctz`: count leading/trailing zeroes
+- `cnt`: count ones
+- `rev`: reverse bits
+- `extend_zero(a) = i2bv(bv2u(a))`
+- `extend_sign(a) = i2bv(bv2s(a))`
+- `extract_low(a) = i2bv(bv2u(a))`
+  - Note: the formula looks the same as `extend_zero`, the difference lies in type constraint
+- `select(cond, a, b) = if bv2bool(cond) then a else b`
+
+Others: complex: are standard, but have to be defined (have `semantic_func`):
+- `rol<N>(a, b) = lsl(a, b%N) | lsr(a, N - b%N)`
+  - same for `ror` with `lsl` and `lsr` swapped
+- `concat_hi_lo<_, _, L>(a, b) = bv2u(a) * 2^L + bv2u(b)`
+- `extract(val, lsb) = extract_low(lsr(val, lsb))`
+  - Note: standard extraction of several bits from a bigger bit vector from a given offset
+- `orr_shifted(base, val, lsb) = orr(base, lsl(extend_zero(val), lsb))`
+  - Note: this is simplified `insert` created for encoding - it behaves the same way if `base` has 0 bits in the place of modification
+- `insert<_, M>(base, val, lsb) = orr(and(base, (2^M - 1) * 2^lsb), lsl(extend_zero(val), lsb))`
+  - Note: standard inserting of several bits into a bigger bit vector at a given offset

From c6a07d59ce1e61e75427a7d27fd70d5f446167b7 Mon Sep 17 00:00:00 2001
From: dan <70999565+belovdv@users.noreply.github.com>
Date: Mon, 28 Sep 2026 12:14:53 +0300
Subject: [PATCH 3/3] wip: replace ^ -> **

---
 docs/ops.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/ops.md b/docs/ops.md
index 156fd8c..d420e09 100644
--- a/docs/ops.md
+++ b/docs/ops.md
@@ -119,11 +119,11 @@ Overflow:
   - same for others with signedness and operation set correspondingly
 
 Shifts:
-- `lsl(a, b) = bv2u(a) * 2^bv2u(b)`
+- `lsl(a, b) = bv2u(a) * 2**bv2u(b)`
   - Note: this provides `lsl(a, huge number) = 0`
-- `lsr(a, b) = bv2u(a) / 2^bv2u(b)`
+- `lsr(a, b) = bv2u(a) / 2**bv2u(b)`
   - Note: this provides `lsr(a, huge number) = 0`
-- `asr(a, b) = bv2s(a) / 2^bv2u(b)`
+- `asr(a, b) = bv2s(a) / 2**bv2u(b)`
   - Note: this provides `asr(a, huge number) = replicate sign bit`
   - Note: `b` is treated as unsigned
 
@@ -140,10 +140,10 @@ Others:
 Others: complex: are standard, but have to be defined (have `semantic_func`):
 - `rol<N>(a, b) = lsl(a, b%N) | lsr(a, N - b%N)`
   - same for `ror` with `lsl` and `lsr` swapped
-- `concat_hi_lo<_, _, L>(a, b) = bv2u(a) * 2^L + bv2u(b)`
+- `concat_hi_lo<_, _, L>(a, b) = bv2u(a) * 2**L + bv2u(b)`
 - `extract(val, lsb) = extract_low(lsr(val, lsb))`
   - Note: standard extraction of several bits from a bigger bit vector from a given offset
 - `orr_shifted(base, val, lsb) = orr(base, lsl(extend_zero(val), lsb))`
   - Note: this is simplified `insert` created for encoding - it behaves the same way if `base` has 0 bits in the place of modification
-- `insert<_, M>(base, val, lsb) = orr(and(base, (2^M - 1) * 2^lsb), lsl(extend_zero(val), lsb))`
+- `insert<_, M>(base, val, lsb) = orr(and(base, (2**M - 1) * 2**lsb), lsl(extend_zero(val), lsb))`
   - Note: standard inserting of several bits into a bigger bit vector at a given offset