Cómo funciona · para desarrolladores y arquitectos

Fuente que entra.
Rust seguro que sale.

Constat convierte programas IBM i (ILE COBOL, RPG IV en formato fijo y libre, SQL embebido, DDS y CL) en un workspace Rust que compila y se ejecuta. Un compilador de verdad, no un script ni un LLM. Un solo pipeline, sin reescritura manual, sin lógica perdida.

El pipeline

Cinco fases, de principio a fin

01

Analizar sintaxis

Tu RPG, COBOL, DDS y CL se leen con un parser de verdad en un modelo interno preciso. Nada inferido, nada supuesto.

02

Bajar a IR

El modelo se baja a representaciones intermedias tipadas en forma SSA, de modo que cada operación es explícita y queda contabilizada.

03

Optimizar

Pasadas de compilador ordenan el código como haría cualquier compilador de verdad, sin cambiar lo que calcula.

04

Generar Rust

Sale Rust idiomático de un generador de código respaldado por pruebas, más un esquema PostgreSQL cuando DB2 está dentro del alcance.

05

Verificar

La salida se comprueba por equivalencia con pruebas verificadas por máquina (Lean 4) y solvers SMT (Z3, CVC5), y se empaqueta con evidencia que puedes auditar.

Comportamiento exacto

Qué preserva

La lógica de negocio no se aproxima. La salida reproduce las partes de la semántica de IBM i que un conversor ingenuo hace mal:

  1. 01

    Aritmética decimal empaquetada y zoned, hasta el último dígito

  2. 02

    Ordenación EBCDIC y semántica de caracteres

  3. 03

    Layout de registro y memoria con REDEFINES / OCCURS

  4. 04

    Flujo de control con PERFORM / GO TO

  5. 05

    Facilidades de plataforma: colas de datos, colas de mensajes, áreas de datos, spool, journaling

Cómo lo probamos

Un compilador verificado, y un límite de confianza claro

La mayoría de herramientas comprueban la salida a posteriori. Constat verifica el propio generador, y luego declara exactamente qué queda confiado y no probado.

  1. 01

    El generador es la prueba

    El generador de código es en sí mismo un programa, escrito y verificado por máquina dentro de un probador de teoremas. Lo que escribe tu Rust es justo aquello sobre lo que tratan las pruebas, no una especificación aparte.

  2. 02

    Probado en el generador, re-verificado por programa

    La corrección del generador se verifica por máquina una vez, en el demostrador, así que lo que escribe tu Rust es aquello de lo que tratan las pruebas. Cada programa se comprueba además de principio a fin sobre tus entradas. Cuando una operación aún no está modelada, o el Rust emitido necesita un paso de post-procesado auditado, lo contamos dentro del límite de confianza en vez de llamarlo probado.

  3. 03

    Dos solvers, contraste independiente

    Además, los programas migrados se comprueban con los solvers Z3 y CVC5, que demuestran que su aritmética y su manejo de datos son equivalentes sobre las operaciones que modelamos, con un segundo solver como contraste independiente. Cada obligación indica su alcance; no es una garantía general sobre todo programa.

  4. 04

    El límite de confianza, nombrado

    Declaramos exactamente qué queda confiado y no probado: el kernel del probador, el compilador de Rust sobre un subconjunto acotado de salida, la librería de runtime, un paso corto de post-procesado auditado aplicado al Rust emitido, y una lista nombrada de supuestos sobre la plataforma legacy, cada uno respaldado por un test reproducible.

Córrelo en hierro

Un programa público, en IBM i real, byte a byte idéntico

NC116A es un test de precisión decimal de la suite pública de conformidad NIST COBOL-85, escrito por NIST, no por nosotros. Lo transpilamos y lo corrimos en un IBM i V7R5 vivo y en el Rust generado. La salida es la misma, hasta el byte.

NC116A NIST COBOL-85 conformance suite Redondeo, truncación, escala, multiplicación de 18 dígitos. Un programa que cualquiera puede buscar.
NC116A.cbl cobol 
*> Test 3: ROUNDED (3 dec to 2 dec)    MOVE 123.456 TO WS-DEC3    COMPUTE WS-DEC2 ROUNDED = WS-DEC3    IF WS-DEC2 = 123.46        PERFORM PASS    ELSE        PERFORM FAIL    END-IF*> Test 7: Division with decimal result    MOVE 10 TO WS-INT5    COMPUTE WS-DEC2 = WS-INT5 / 3    IF WS-DEC2 = 3.33        PERFORM PASS    ELSE        PERFORM FAIL    END-IF
NC116A.rs rust 
let ws_dec2_v40 = scaled_divide(ws_int5_v39, 0u8, v38, 0u8, 2u8);let ws_large_c_v32 = axiom_arith_mul_overflow_pic(ws_large_a_v30, ws_large_b_v31, 18u8).0;

Corre los dos. Compara la salida.

IBM i V7R5 · IBM Power (live) hardware real 
PASS NC116A-01PASS NC116A-02PASS NC116A-03PASS NC116A-04PASS NC116A-05PASS NC116A-06PASS NC116A-07PASS NC116A-08PASS NC116A-09PASS NC116A-10NC116A PRECISION TESTSPASS: 10FAIL: 00
axiom-rt · generated Rust rust 
PASS NC116A-01PASS NC116A-02PASS NC116A-03PASS NC116A-04PASS NC116A-05PASS NC116A-06PASS NC116A-07PASS NC116A-08PASS NC116A-09PASS NC116A-10NC116A PRECISION TESTSPASS: 10FAIL: 00
La misma salida, hasta el byte, desde IBM i real y desde el Rust generado. 10 pasan · 0 fallan

44 programas NIST públicos corren byte-exact en IBM i real. NC116A es uno de ellos.

Un segundo sello, independiente: la prueba formal

NC116ADecimal.lean lean 
theorem qRound_within_half (N D : ℤ)    (hN : 0 < N) (hD : 0 < D) :    2 * |qRound N D * D - N| ≤ D := by …theorem qRound_ties_away (N D : ℤ)    (hN : 0 < N) (hD : 0 < D) (htie : 2 * qRem N D = D) :    qRound N D = qTrunc N D + 1 := by …-- #print axioms qRound_within_half'…qRound_within_half' depends on axioms: [propext, Quot.sound]

El núcleo decimal está máquina-verificado para todo operando en el régimen que NC116A usa: el ROUNDED generado es el entero escalado más cercano, y los empates rompen half-away-from-zero, no el round-half-to-even que un port ingenuo heredaría de Rust. 9 teoremas, 0 sorry, 0 suposiciones nuestras, los mismos axiomas estándar que la prueba bancaria de abajo.

reprodúcelo tú mismo 
axiom transpile NC116A.cbl --platform ibm-icargo run --release        # -> 10 PASS / 0 FAIL, byte-identical to IBM i

Así que NC116A está sellado dos veces, de forma independiente: la ejecución byte-idéntica en IBM i real, y esta prueba para todo operando de su núcleo decimal. No tiene estado de base de datos, así que aquí no hay bisimulación de base de datos, y el caso con signo general queda fuera de alcance porque sus tests no lo ejercen. Para la migración DB2 completa con bisimulación para toda entrada, mira el programa bancario de abajo.

Fidelidad, no papeleo

Cuando la referencia se equivocó, coincidimos con la máquina real

NC142A es otro test público de NIST. Su "salida esperada" commiteada dice que las ocho comprobaciones pasan. Córrelo en un IBM i V7R5 real y no pasan: en un MOVE de "54321" a un campo numérico, la máquina lanza un error de dato decimal y el trabajo abende tras el primer test. El Rust generado abende en el mismo punto, de la misma forma.

La respuesta commiteada de NIST PASS ×8 dice que pasa
IBM i V7R5 real, en vivo MCH1202 abend el comportamiento real
axiom-rt, el Rust generado MCH1202 abend coincide con el hierro real
NC142A · ambos, idéntico 
PASS NC142A-01MCH1202  Escape  sev-40  NC142A  *STMT  →  CEE9901, job abends

Esta es la prueba honesta de una herramienta de migración: reproducir la plataforma real, incluida su severidad y sus fallos, no una referencia indulgente. Coincidimos con la máquina byte a byte, incluso donde la respuesta publicada estaba mal. Enrutamos NC142A como una corrección de fidelidad del oráculo en el corpus público, no como un cambio en nuestra salida.

Ver la evidencia

Un programa, cada artefacto

No un diagrama. Un programa sellado real recorriendo todo el pipeline, cada etapa un fragmento literal del artefacto del que sale. Lee tú mismo el source, el Rust generado, el teorema y el resultado run-on-both.

BORROW_INT Drains open borrowings, accrues interest (principal × rate/daycount × days), and CALLs GL_POST to book a balanced double-entry journal. L2 BISIMILAR vs live IBM i V7R5
Ver la cadena completa de artefactos 7 etapas, de la fuente a un dosier re-verificable
  1. 01

    El programa

    input

    COBOL real. El núcleo del devengo: la tasa diaria, luego principal por tasa por días.

    borrow_int.sqlcblle cobol 
    COMPUTE-ACCR-AMOUNT.    IF DC-365       COMPUTE WS-RATE-DAILY = HV-BW-RATE / K-DAYCOUNT-365          ON SIZE ERROR SET STEP-FAIL TO TRUE EXIT PARAGRAPH    END-IF    COMPUTE WS-ACCR-RAW =            HV-BW-PRINCIPAL * WS-RATE-DAILY * WS-DAYS-TO-ACCRUE       ON SIZE ERROR          SET STEP-FAIL TO TRUE          MOVE RC-AMOUNT-OVERFLOW TO WS-OUT-RC    END-COMPUTE
    from projects-xl/bankdemo/src/borrow_int.sqlcblle:559
  2. 02

    Cada línea tiene origen

    generated

    El mapa de origen enlaza cada función Rust generada con la línea COBOL exacta de la que salió. Lee el código nuevo contra el viejo.

    borrow_int.map.json json
    COBOLparagraphRust
    :559COMPUTE-ACCR-AMOUNT:5542 · compute_accr_amount
    :535COMPUTE-DAYS-TO-ACCRUE:5460 · compute_days_to_accrue
    :454ACCR-SINGLE-BORROW:5204 · accr_single_borrow
    from .axiom/compiler/borrow_int.map.json
  3. 03

    El Rust generado

    generated

    La misma aritmética en Rust con memoria segura. La escala del decimal empaquetado se preserva exacta, calculada sobre enteros de 128 bits, nunca en coma flotante. Los nombres son la forma SSA del compilador; el mapa de arriba ata cada uno al COMPUTE.

    borrow_int.rs rust 
    pub fn compute_accr_amount(data: &mut ProgramData) {  let v298 = scaled_divide_i128_keep(v297, 6u8, v296 as i128, 0u8, 6u8);  let v330 = axiom_arith_mul_overflow_pic_i128(v328, v329, 38u8).0;  let v332 = axiom_arith_mul_overflow_pic_i128(v330, v331 as i128, 38u8).0;  store_packed_trunc(|b| data.set_field_107(b), v332.wrapping_div(100i128), 11usize, true, 21u32, false);}
    from .axiom/…/borrow_int.rs (regenerated at build)
  4. 04

    DB2 a PostgreSQL, regla por regla

    generated

    Cada expresión propia de DB2 se reescribe a PostgreSQL, y el rastro queda registrado sentencia a sentencia.

    borrow_int.sql-rewrites.jsonl diff
    CHAR(CURRENT DATE, ISO) TO_CHAR(CURRENT_DATE, 'YYYY-MM-DD') CHAR(x,ISO)→TO_CHAR, CURRENT-register
    DAYS(DATE(?)) - DAYS(DATE(?)) ((DATE(?) - DATE '0001-01-01')::int + 1) - … DAYS→date-arith
    from verify/dossier/sql-rewrites/borrow_int.sql-rewrites.jsonl
  5. 05

    El teorema, y su recibo

    proof-artifact + receipt

    Un teorema de bisimulación verificado por máquina: para toda entrada, la ejecución en DB2 y en PostgreSQL produce el mismo estado. El recibo es la lista literal de axiomas del núcleo. Descansa en un único axioma estándar de Lean y en ninguna suposición nuestra.

    BorrowIntMasterInstance.lean lean 
    theorem borrowInt_master :    ∀ (inputs …), db2Run inputs = pgRun inputs := by …-- #print axioms borrowInt_master'…borrowInt_master' depends on axioms: [propext]
    from lean4/Axiom/Bisim/BorrowIntMasterInstance.lean:185 + …MasterInstance.axioms.txt
  6. 06

    Ejecutado en ambos, comparado byte a byte

    verification

    El original se ejecutó en hardware IBM i V7R5 real; el Rust se ejecutó con las mismas entradas. El estado de negocio resultante coincidió, fila por fila.

    BORROWPF
    3/3 rows · ACCRINT 4980 / 5985 / 7500 (packed decimal, 6dp, truncated identically)
    GLJRN
    6/6 rows · double-entry balanced, sum DR = CR = 18465.00
    captured
    iron BANKDEMOXL via IBM i MCP, 2026-06-23
    from verify/bisim/oracles/borrow_int/{BORROWPF,GLJRN}.S1.json
  7. 07

    Un dosier que puedes re-verificar

    receipt

    Un solo comando re-verifica todo el registro de principio a fin, así nada se puede cambiar ni editar a posteriori.

    artifacts_checked
    21
    proof_artifacts_proven
    2
    dossier_digest
    61f950ee0cb024cd51d72ae391e268ed…
    codegen_sha256
    7ed16a32379e18ef…
    verdict
    COHERENT
    from axiom audit --json (fresh run, 2026-07-18)
Qué cubre esto, y qué no
  • The dossier manifest seals the .axiom/* artifacts; the emitted .rs is tracked with its own hash, not yet inside the manifest.
  • The run-on-both observational equivalence lives in the bisimulation registry, not inside the per-program dossier.
  • Here the equivalence proof is the Lean bisimulation theorem; the standalone Z3/CVC5 pass is a separate, more conservative overflow analysis.

Cómo lo audita un agente de IA

An AI agent drives the whole thing through the MCP server and re-checks the result itself.

agent · axiom MCP 
mcp__axiom__transpile(source, decouple=["DB2=postgresql"], audit=true)→ { rc: 0, result: { verify }, audit: { verdict: "COHERENT", artifacts_checked: 21, dossier_digest } }the agent re-verifies every SHA-256 in the manifest itself. trust nothing, check everything
transpileauditanalyzeplancodegen_provenanceverb_statusdoctor

--agent emits one JSON line; --fail-on gates the exit code (rc 3 = verification gate tripped); --progress ndjson streams phase events. A green exit cannot contradict the certificate.

Qué obtienes

Un workspace que es tuyo

Rust legible y un esquema PostgreSQL abierto sobre tu infraestructura. Después, el registro completo por programa: el árbol de sintaxis, las representaciones intermedias, las pruebas formales, las fórmulas SMT para re-verificar con tu propio Z3 o CVC5, y un mapa fuente→Rust línea a línea. Nada queda oculto entre tu COBOL y el Rust; tu equipo lee la matemática de la migración, no solo la salida. Sin dependencia de runtime, sin caja negra.

Mira cómo probamos la equivalencia