leonardoalt

--- extensions/womir_circuit/cuda/include/womir/adapters/alu.cuh	2026-03-04 17:06:33.450505710 +0100
+++ extensions/womir_circuit/cuda/include/womir/adapters/jump.cuh	2026-03-04 17:10:52.534016146 +0100
@@ -1,9 +1,8 @@
-// Adapted from <openvm>/extensions/rv32im/circuit/cuda/include/rv32im/adapters/alu.cuh
-// Main changes: adds frame pointer (fp) field, WomirExecutionState, fp_read_aux, timestamp +1 shift
-// Diff: https://gist.github.com/leonardoalt/09fd3d60bd571851bb656dc53cec0a4b#file-diff-adapters-alu-cuh-diff
+// WOMIR Jump adapter for CUDA tracegen.
+// Reads FP + 1 register (condition/offset), no writes.
+// Simpler than the ALU adapter: single register read, no rs2, no write.
 #pragma once

leonardoalt

--- extensions/womir_circuit/cuda/include/womir/adapters/alu.cuh	2026-03-04 16:22:21.368217432 +0100
+++ extensions/womir_circuit/cuda/include/womir/const32.cuh	2026-03-04 16:26:53.584878211 +0100
@@ -1,9 +1,9 @@
-// Adapted from <openvm>/extensions/rv32im/circuit/cuda/include/rv32im/adapters/alu.cuh
-// Main changes: adds frame pointer (fp) field, WomirExecutionState, fp_read_aux, timestamp +1 shift
-// Diff: https://gist.github.com/leonardoalt/09fd3d60bd571851bb656dc53cec0a4b#file-diff-adapters-alu-cuh-diff
+// CUDA tracegen for Const32 chip.
+// Unlike ALU chips, Const32 has no adapter+core split: it's a single unified structure.
 #pragma once
 

leonardoalt

--- /home/leo/devel/openvm/extensions/rv32im/circuit/cuda/include/rv32im/adapters/alu.cuh	2026-03-02 14:57:12.776007921 +0100
+++ /home/leo/devel/womir-openvm/extensions/womir_circuit/cuda/include/womir/adapters/alu.cuh	2026-03-02 15:50:33.500343846 +0100
@@ -7,63 +7,81 @@
 
 using namespace riscv;
 
-template <typename T> struct Rv32BaseAluAdapterCols {
-    ExecutionState<T> from_state; // { pub pc: T, pub timestamp: T}
+// WOMIR ExecutionState includes frame pointer (fp) between pc and timestamp.
+template <typename T> struct WomirExecutionState {

leonardoalt

; fixed inputs
(declare-const imm_limbs_1 Int)
(declare-const imm_limbs_2 Int)
(declare-const imm_limbs_3 Int)

(declare-const from_pc Int)

; two versions of every variable and constraint, to check for nondeterminism
(declare-const pc_limbs_1 Int)
(declare-const pc_limbs_2 Int)

leonardoalt

 ./INSTALL                                 
+ cargo run --bin creusot-install --
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.14s
     Running `target/debug/creusot-install`
Building prelude...
Installing Why3 and Why3find...
Package creusot-deps does not exist, create as a NEW package? [y/n] y
The following additional pinnings are required by creusot-deps.dev:
  - why3.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb
  - why3-ide.git-9c6f at git+https://gitlab.inria.fr/why3/why3.git#9c6f54fbb

leonardoalt

use std::machines::large_field::binary::Binary;
use std::machines::range::Bit2;
use std::machines::range::Bit6;
use std::machines::range::Bit7;
use std::machines::range::Byte;
use std::machines::range::Byte2;
use std::machines::binary::ByteBinary;
use std::machines::split::ByteCompare;
use std::machines::large_field::shift::ByteShift;
use std::machines::hash::poseidon_gl_memory::PoseidonGLMemory;

leonardoalt

#![no_main]
#![no_std]

extern crate powdr_riscv_runtime;

#[no_mangle]
fn main() {
    loop_test_matrix();
}

leonardoalt

use std::machines::binary::Binary;
use std::machines::range::Bit2;
use std::machines::range::Bit6;
use std::machines::range::Bit7;
use std::machines::range::Byte;
use std::machines::range::Byte2;
use std::machines::binary::ByteBinary;
use std::machines::split::ByteCompare;
use std::machines::shift::ByteShift;
use std::machines::shift::Shift;

leonardoalt

owner(owner).
tx(id, calldata, addr).
approved(owner, tx).
executed(tx).
quorum(quorum).

public(add_tx).
public(approve).
public(execute).

leonardoalt

namespace std::convert(1024);
    let int = [];
namespace std::prover(1024);
    enum Query {
        Input(int),
        PrintChar(int),
        Hint(fe),
        DataIdentifier(int, int),
    }
    let eval: expr -> fe = [];