Agentes y coordinación

Observabilidad

-- Doc example: observability. `log` is real; `trace`/`measure`/`checkpoint` are
-- decorative markers — they RUN their body but don't persist timing/snapshots.
intent: "doc example: observability"
require file.write("./_doctest_outputs/**")   -- what the run writes lands in the receipt (v0.6.46+)

let answer be 0
measure "demo"
    set answer to 41 + 1
print("measure ran → answer = " + text(answer))

test "measure runs its body (the timing instrumentation is decorative)"
    let x be 0
    measure "compute"
        set x to 41 + 1
    assert_eq(x, 42)

-- Lineage (v0.6.29+): the engine records every input the program reads. parquet_read is pure,
-- so it shows the shape with no capability: a file passed as bytes is recorded by its SIZE,
-- never its content, and the hash covers the rows as canonical JSON ("jcs").
test "lineage() lists each input with a hash anyone can recompute"
    assert_eq(lineage(), [])
    let rows be parquet_read(parquet_write([{"sku": "a-1", "qty": 3}]))
    let e be lineage()[0]
    assert_eq(e.source, "parquet_read")
    assert(starts_with(e.what, "bytes "))
    assert_eq(e.encoding, "jcs")
    assert_eq("0x" + e.sha256, hex(sha256(canonical_json(rows))))
    assert_eq(e.bytes, length(bytes(canonical_json(rows))))

-- Outputs (v0.6.46+): the receipt also names what the run WROTE, in order, with the sha256 of
-- the bytes that reached the disk. append_file records the appended chunk, edit_file the file
-- as it was left. The hash has no salt: anyone holding the file recomputes it.
test "receipt() lists each write in credentialSubject.outputs"
    write_file("./_doctest_outputs/model.txt", "weights v1")
    append_file("./_doctest_outputs/model.txt", " +bias")
    let outs be receipt().credentialSubject.outputs
    assert_eq(length(outs), 2)
    assert_eq(outs[0].source, "write_file")
    assert_eq(outs[0].what, "./_doctest_outputs/model.txt")
    assert_eq(outs[0].encoding, "text")
    assert_eq("0x" + outs[0].sha256, hex(sha256(bytes("weights v1", "utf8"))))
    assert_eq(outs[1].source, "append_file")
    assert_eq(outs[1].bytes, 6)
    assert_eq("0x" + outs[1].sha256, hex(sha256(bytes(" +bias", "utf8"))))

test "a write is an output, not an input"
    write_file("./_doctest_outputs/report.bin", bytes([1, 2, 3]))
    let cs be receipt().credentialSubject
    let last be cs.outputs[length(cs.outputs) - 1]
    assert_eq(last.what, "./_doctest_outputs/report.bin")
    assert_eq(last.encoding, "bytes")
    assert_eq(last.bytes, 3)
    assert_eq(length(where(cs.inputs, (e) => e.what == "./_doctest_outputs/report.bin")), 0)
    assert_eq(get(cs, "outputs_truncated"), nothing)

Logging (real)§

log toma una expresión completa y la escribe en stdout como [LOG] …. Bajo synsema run, print, log y show se escriben a medida que ocurren, línea por línea y en el orden del programa (v0.6.29+; antes, print se retenía hasta que el programa terminaba). Bajo serve, log/print llegan a la terminal con prefijo [serve].

log "Processing order " + order_id

log es una sentencia, no una función — ni una expresión. log "msg" funciona; log("msg") pasa check pero falla al correr con Undefined variable: 'log', y let x be log "msg" no parsea.

Logs bajo serve (logging de requests)§

serve no escribe un access log por vos — por defecto la terminal está callada, lo que dificulta el desarrollo. Agregá un log en tus handlers para ver el tráfico en vivo:

route "GET /:lang/:version/:slug"
    log "GET " + (path of request)
    give render_page(...)

Cada request entonces aparece en la terminal del server como [serve] [LOG] GET /…. print también funciona ahí (mismo prefijo [serve]). (Este sitio de docs loguea sus propios requests así.)

Marcadores — trace / measure / checkpoint (decorativos)§

trace y measure corren su cuerpo pero la instrumentación de timing hoy es un stub; checkpoint es una sola línea sin cuerpo. Ninguno persiste nada. trace/measure toman un nombre literal; checkpoint toma una expresión (checkpoint "step_" + text(i)).

measure "db_query"
    run_query(sql)

Para crash-resume / tracking de pasos real, usá los builtins de progress, no checkpoint — ver Memoria y estado.

Audit de capabilities (--audit json)§

Cada chequeo de capability que hace el runtime — concedido o denegado — se puede streamear como JSON, una línea por chequeo, en run/test/conform/serve (engine v0.6.14+):

synsema run --audit json        program.syn   # a stderr
synsema run --audit ./audit.jsonl program.syn # a un archivo
synsema run --audit fd:3        program.syn   # a un file descriptor (solo Unix)
synsema run --audit unix:/run/audit.sock program.syn   # a un socket Unix donde alguien escucha (solo Unix; falla ruidoso si nadie escucha, v0.6.20+)
SYNSEMA_AUDIT=json ./app                        # los mismos valores desde el entorno — sin flag; funciona en un binario de synsema build (v0.6.20+)

Cada línea es {ts, context, capability, granted, source, reason, origin, file, line}:

• context — qué CapabilitySet (program, agent, request, worker, un frame sandbox:/tool:).
• origin — "program" (un require o una llamada que hizo el código) o "runtime" (un grant ambiente: stdout/time/llm, o serve desde --port).
• reason — Granted by <grant>, No matching grant found, above host ceiling (--sandbox/--cap-set), Explicitly denied by …, auto-granted by the runtime (un grant ambiente que tuvo éxito ahora deja rastro), o bundled asset (part of the program) (una lectura desde un bundle de synsema build).
• source — el builtin que disparó el chequeo (read_file(), run(), …), o ceiling/ambient/secret-builtin.
• file/line — dónde en el programa (o null).

Qué grant nombra Granted by … (motor v0.6.47+): siempre el más angosto que cubre el uso. Antes, con dos grants que cubrían el mismo uso, el audit nombraba uno al azar (una semilla nueva por corrida). Ahora los grants se guardan en un orden fijo, primero el que cubre menos:

• con scope antes que sin scope; sin comodín (*, ?) antes que con comodín; más caracteres

literales antes que menos ([ es un carácter literal, no un comodín);

• net: un host o IP exacto antes que un CIDR, un prefijo más largo antes que uno más corto

(net("10.1.2.3") → net("10.1.0.0/16") → net("10.0.0.0/8")), y un puerto lo angosta (net("10.0.0.0/8:9") antes que net("10.0.0.0/8"));

• secret: uno atado a hosts (secret("k") for net("*.x.com")) antes que el que no lo está;
• llm/judge: el scope nombra de quién son los datos privados que se pueden mandar, así que el

grant sin scope cubre sólo datos públicos y es el más angosto. La entrada de la operación (source: "llm operation") nombra llm en toda llamada; una llamada con datos privados de P deja además una entrada con source: "llm-data" cuyo capability es el grant que dejó salir el dato (llm("P@<proveedor>"));

• los empates se rompen por tipo y después por scope. El orden se lee del texto, así que una ruta

relativa contra una absoluta se compara por largo.

Con require net("*.example.com"), require net("api.example.com") y require net, una llamada a api.example.com loguea "reason":"Granted by net(\"api.example.com\")" en cada corrida; con require llm y require llm("customers"), un generate público loguea "reason":"Granted by llm". El mismo orden elige el deny que nombran el audit y el error.

Una línea final resume: {"summary": {"granted": N, "denied": M, "exit": code}}. Los valores de secretos nunca aparecen — los scopes de capability son nombres (secret("STRIPE_KEY")), nunca el valor. Este es el mismo audit que el run() de WebAssembly devuelve como r.audit (campos en la página WASM); el stream nativo solo agrega ts/context/file/line. run_program devuelve el audit de su hijo como r["audit"] — un valor, no un log para parsear.

synsema build … --audit json|<path>|unix:<path> hornea el sink en el binario (engine v0.6.20+); SYNSEMA_AUDIT en el entorno lo activa para cualquier binario, horneado o no, y el flag gana sobre la variable. En Windows fd:N y unix: se rechazan con exit 2 — usá json o una ruta.

Contador de pasos — steps() (engine v0.6.20+)§

steps() → la cantidad de sentencias que el intérprete ejecutó hasta ahora en este programa. Cuenta nodos, no tiempo, así que el mismo programa da el mismo número en cada corrida — una medida determinista de trabajo para medir, testear y poner límites tipo combustible en un host que corre programas ajenos. Sin capacidad (introspección, como llm_usage()), disponible en todos los perfiles. synsema run --format json reporta el total como steps, al lado de llm_tokens.

Bajo etiquetas (engine v0.6.24+, --labels / serve --attested — ver Etiquetas) el contador no es neutral: es lineal en lo que el programa recorrió, así que después de una rama tomada sobre un valor privado es el secreto. Por eso steps() vuelve cargando la unión de lo que la corrida tocó, y el host deja de publicarlo — run --format json y run --attest reportan "steps": null para esa corrida. declassify(steps(), "<por qué>") si lo querés publicar. Bajo serve el contador es por request, no por proceso: el servidor reusa el intérprete entre requests y un acumulado filtraría el trabajo del llamador anterior.

let before be steps()
process(batch)
log "cost: " + text(steps() - before) + " steps"

Linaje — qué entradas produjeron un resultado (v0.6.29+)§

El engine, no tu programa, registra cada dato que el programa lee de afuera, en orden: archivos y listados de directorio, grep, Parquet, stdin (read_line), HTTP, lecturas de SQL/Mongo/Redis, recall, nodos de cadenas (EVM, Solana, Algorand, Bitcoin), sockets y procesos, lo que devuelven run/run_program, y la respuesta de un modelo real a reason/analyze/generate. No podés agregar, editar ni sacar una entrada. lineage() las lista hasta el momento:

let rows be parquet_read(parquet_write([{"sku": "a-1", "qty": 3}]))
let e be lineage()[0]
print(e.source + " " + e.what)                                    -- parquet_read bytes <file size>
print("0x" + e.sha256 == hex(sha256(canonical_json(rows))))       -- true

No se registra nada más como entrada: ni lo que el programa escribe (eso es una salida, más abajo), ni env/secret, ni el blackboard, ni un placeholder offline del LLM, ni una lectura que nunca llegó, ni el archivo que edit_file lee antes de editar. receipt() publica la misma lista como credentialSubject.inputs (sin las sales), junto al sha del programa, el engine, el audit de capabilities, las salidas y el resultado que declarás — firmado, prueba qué entradas, qué programa, qué archivos escritos y qué salida. Los recibos y sus firmas: Identidad de agentes.

La lista se corta en 10.000 entradas. inputs_truncated: true aparece en el recibo solo cuando de verdad se descartó una entrada (engine v0.6.46+; antes ya era true con exactamente 10.000); lineage() se queda en 10.000. Bajo serve, lineage() y los inputs del recibo son los de la request (engine v0.6.46+; antes también listaban lo que habían leído requests anteriores del mismo worker, que podían ser de otro usuario).

Salidas — lo que la corrida escribió (engine v0.6.46+)§

receipt().credentialSubject.outputs lista cada archivo que escribió la corrida, en orden, con los mismos campos que una entrada:

• write_file registra el contenido entero; append_file registra solo el pedazo agregado;

edit_file registra el archivo como quedó; zip_extract/tar_extract registran una entrada por archivo extraído.

• Un modelo entrenado, un reporte o una exportación escritos a disco quedan en el recibo firmado sin

hashearlos a mano: quien tiene el archivo recalcula sha256 y compara.

• parallel_map: lo que lee y escribe cada worker se incluye, en el orden de los ítems (antes

de v0.6.46 también faltaban sus inputs), aun cuando un ítem falla — lo que los workers leyeron y escribieron hasta ahí queda.

• Bajo serve, los outputs son los de la request.
• El mismo tope que inputs: 10.000 entradas, después outputs_truncated: true (el campo no

aparece mientras no se descartó nada).

• El sha256 no lleva sal, igual que en inputs: después de un declassify, el hash de un

valor corto (un PIN, un sí/no, un número chico) se adivina hasheando cada candidato. No escribas a disco un secreto corto en una corrida cuyo recibo publicás.

• Con etiquetas, una escritura bajo un contexto privado se rechaza (escribir es un sumidero

público), así que una rama privada nunca llega a outputs.

• Un append_file que falla a mitad de camino puede dejar en disco bytes que no se listan.
• print/log no son salidas acá: esa es la salida del programa, la que hashea run --attest.

require file.write("./out/**")

write_file("./out/model.txt", "weights v1")
append_file("./out/model.txt", " +bias")
let outs be receipt().credentialSubject.outputs
print(outs[0].source + " " + outs[0].what + " " + text(outs[0].bytes))   -- write_file ./out/model.txt 10
print(outs[1].source + " " + text(outs[1].bytes))                        -- append_file 6
print("0x" + outs[0].sha256 == hex(sha256(bytes("weights v1", "utf8"))))  -- true

Con un auditor (sección siguiente), cada escritura va además al recibo sellado como una entrada con kind: "output", en el orden en que pasó: para los workers de parallel_map, el orden en que se hicieron, no el de los ítems (igual que sus entradas capability). receipt() conserva el orden de los ítems.

Recibos sellados para un auditor (engine v0.6.46+)§

Con etiquetas, un builtin que deja rastro de auditoría (reveal, sign y los builtins de firma, las operaciones de wallet) se rechaza en una rama decidida por un valor privado: que exista su línea de auditoría le dice al operador por dónde fue la rama. Un recibo sellado la deja correr: el host designa un auditor con una clave pública X25519, y lo que la corrida deja en esa rama va a un sobre que solo el auditor puede abrir. Cualquier otro igual puede comprobar que el recibo está entero y firmado.

synsema receipt keygen --out auditor.key                                   # the auditor, once
synsema run --labels --auditor <public> --receipt run.json program.syn     # the host
synsema receipt verify run.json                                            # anyone
synsema receipt open run.json --key @auditor.key > opened.json             # the auditor
synsema run --labels --replay opened.json program.syn                      # the auditor, again

Las claves del auditor — synsema receipt keygen§

• synsema receipt keygen imprime {"private": "<base64url>", "public": "<base64url>"} en stdout:

un par X25519 nuevo, 32 bytes cada una, en base64url sin padding.

• synsema receipt keygen --out auditor.key escribe la privada en un archivo nuevo e imprime

en stdout solo {"public": "…", "private_in": "auditor.key"}, más una pista en stderr: open receipts with: synsema receipt open <receipt.json> --key @auditor.key. El archivo no tiene que existir: synsema receipt keygen: cannot create auditor.key (it must not exist): <error del SO> (exit 1); el mismo mensaje cuando no existe su carpeta.

• La pública es la que recibe el host; la privada nunca sale del auditor.

Cómo se prende — --auditor / SYNSEMA_AUDITOR_KEY§

synsema run --auditor <pública> y synsema serve --auditor <pública>, o SYNSEMA_AUDITOR_KEY en el entorno o en .env (gana la bandera; synsema init la lista, comentada, en .env.example). Un binario hecho con synsema build también lee SYNSEMA_AUDITOR_KEY. En @synsema/wasm es la opción auditor: ver WebAssembly. synsema test no tiene --auditor (e ignora la variable).

La clave se comprueba antes de que corra el programa (exit 2):

Un auditor sin --labels también funciona: no hay nada privado, así que toda entrada es pública, pero la corrida igual obtiene un registro firmado, una semilla grabada y lecturas de reloj grabadas para --replay.

El tamaño del sobre — SYNSEMA_RECEIPT_SEALED_BYTES§

El sobre es HPKE (RFC 9180: X25519, HKDF-SHA256, AES-128-GCM) de un texto plano de tamaño fijo: SYNSEMA_RECEIPT_SEALED_BYTES, 65536 por defecto, entre 4096 y 16777216. Así el recibo mide lo mismo después de 0 entradas selladas que después de 50: su largo no dice nada de la rama. Con el default un recibo pesa unos 89 KB (el sobre es 32 + N + 16 bytes, en base64url); solo la parte pública le cambia el largo. Lo fija el host (entorno o .env), nunca el programa.

• SYNSEMA_RECEIPT_SEALED_BYTES must be between 4096 and 16777216, got N / `… must be a number

of bytes, got "abc"` — exit 2 antes de que corra el programa.

• Lo que no entra se corta adentro y se cuenta: primero las lecturas de reloj (que igual ocupan

como mucho un cuarto del sobre, ver abajo), después las últimas entradas. truncated en el recibo abierto cuenta las entradas selladas descartadas; la cadena cubre las que quedaron. Si ves truncated mayor que 0, subí el tamaño.

La forma de un recibo§

Una línea JSON:

{"synsema_receipt": 1,
 "header": {"v": 1, "suite": "HPKE-Base-X25519-SHA256-AES128GCM", "engine": "v0.6.46",
            "program_sha": "<hex>", "config_sha": null, "started": "2026-10-23T07:36:04Z",
            "run_key": {"alg": "Ed25519", "public": "<base64url>", "identity": "ephemeral"},
            "auditor": "<base64url>", "seed_sha256": "<hex>", "public_entries": 8,
            "sealed_bytes": 65536},
 "public": [{"kind": "capability", "context": "program", "capability": "stdout", "granted": true, "…": "…"},
            {"kind": "input", "source": "read_file", "what": "in.txt", "sha256": "<hex>", "bytes": 4, "encoding": "text"},
            {"kind": "output", "source": "write_file", "what": "./out/a.txt", "sha256": "<hex>", "bytes": 3, "encoding": "text"}],
 "sealed": "<base64url: enc ‖ ciphertext>",
 "root": "<hex>",
 "signature": "<base64url>"}

• program_sha es el mismo que dan synsema code sha y receipt(). config_sha es null salvo

bajo run --attest y serve --attested, donde es el de la configuración atestada. started está en UTC, al segundo. seed_sha256 es el sha256 de los bytes de la semilla (la semilla misma va en el sobre). public_entries cuenta la parte pública.

• public guarda las entradas hechas con el contador de programa público, en orden de corrida:

capability (la línea del audit de capabilities de --audit json, sin ts), input (una entrada de linaje) y output. La parte sellada guarda lo que pasó en una rama privada: entradas capability (con ts) y entradas op, {"kind": "op", "line": "<la línea de auditoría>", "log": "reveal.log"}. La línea de auditoría de una operación sellada va al sobre en lugar de ~/.synsema/audit/reveal.log (o sign.log, wallet.log): el log en disco le diría al operador lo que el sobre esconde.

• root es el final de una cadena de hashes sobre todas las entradas, públicas y selladas, en

orden de corrida: h0 = sha256("synsema-receipt-v1" ‖ jcs(header)), hi = sha256(hi-1 ‖ "P" o "S" ‖ jcs(entrada)). jcs es canonical_json. La parte pública no lleva posiciones (un número de secuencia diría cuántas selladas hubo antes), así que solo el auditor puede recalcular la cadena.

• signature es la firma de la clave de la corrida sobre `"synsema-receipt-v1" ‖

sha256(jcs(header)) ‖ sha256(jcs(public)) ‖ sha256(bytes del sobre) ‖ bytes de root. El sobre también está atado al header (su AAD es sha256(jcs(header))): cambiá cualquier cosa del header, aunque sea solo para refirmarlo con otra clave, y el open del auditor falla con the envelope does not open with this key …`.

synsema receipt verify y synsema receipt open hacen estos chequeos por vos; este programa los hace a mano, que es lo que tiene que repetir un verificador escrito en otro lenguaje:

require file.read("run.json")
require file.read("opened.json")

let r be json_decode(read_file("run.json"))
let o be json_decode(read_file("opened.json"))
let D be bytes("synsema-receipt-v1", "utf8")
let h be r["header"]

task digest(v)
    give sha256(bytes(canonical_json(v), "utf8"))

-- anyone: the signature (an Ed25519 run key; a P-256 one is ECDSA, r ‖ s)
let msg be D + digest(h) + digest(r["public"]) + sha256(bytes(r["sealed"], "base64url")) + bytes(r["root"], "hex")
print(ed25519_verify(msg, bytes(r["signature"], "base64url"), bytes(h["run_key"]["public"], "base64url")))   -- true

-- the auditor: the chain, over the opened entries in run order
let x be sha256(D + bytes(canonical_json(h), "utf8"))
each e in o["entries"]
    let tag be "P"
    when e["sealed"]
        set tag to "S"
    set x to sha256(x + bytes(tag, "utf8") + bytes(canonical_json(e["entry"]), "utf8"))
print(slice(hex(x), 2) == r["root"])                                                                         -- true

Quién lo firma — run_key.identity§

Cuándo sale — antes de la salida§

• synsema run escribe el recibo en stderr, o en --receipt <ruta>, y recién después

imprime. Con un auditor, print, flush() y el prompt de read_line no salen en vivo: la salida viene después del recibo. eprint sí sale mientras corre (es un sumidero, en stderr).

• --receipt <ruta> reemplaza el archivo en cada corrida. Una ruta que no se puede escribir es

--receipt: cannot write <ruta>: <error del SO> (exit 2) antes de que corra el programa, y un recibo que ya estaba en ese archivo queda hasta que una corrida escriba el suyo. Una corrida que falla (un error de parseo, un error de runtime) igual escribe su recibo, y sale con 1.

• --receipt fd:N escribe en un descriptor que dejó abierto el padre, y es solo Unix. En Windows:

--receipt fd:3: a file descriptor is only available on Unix; pass a path (exit 2).

• synsema run --format json pone el recibo primero, como receipt, antes de ok, output

(que entonces también trae los prompts de read_line) y steps; además lo escribe en --receipt si se pasó.

Bajo serve — un recibo por request§

synsema serve --auditor <pública> [--receipt <ruta|fd:N>] escribe un recibo por cada request que corre código del programa, antes de la respuesta: en stderr, o agregado a --receipt (uno por línea; reiniciar el server agrega al mismo archivo). Una request que no corre ningún handler — un 404, /openapi.json — no tiene.

Una ruta stream o socket es un error de carga con un auditor, porque su body sale mientras corre, antes de que exista el recibo (para una ruta socket el mensaje dice is a socket route). Servilas desde otro server sin auditor:

Runtime error: serve --auditor: route `GET /events` is a stream route: its body leaves while it runs, before the request's sealed receipt exists

• inputs/outputs son los de la request.
• Un job de cron o un agente fuera de una request no tiene recibo, así que una operación auditada en

una rama privada ahí sigue siendo un label_violation ([serve] [cron] job 'job' failed: label_violation: reveal called under private control flow …).

• El archivo de --receipt se abre cuando arranca el server. Borrarlo mientras el server corre no

hace que el server lo reabra: las requests siguen respondiendo 200 y sus recibos van al archivo borrado, así que se pierden. Rotalo reiniciando.

• El resto de --receipt (ruta mala, fd:N en Windows, sin auditor) falla al arrancar igual que

bajo run.

Qué corre en una rama privada, y qué sigue sin correr§

La semilla y el reloj§

• random() y random_int() salen de una semilla grabada en el sobre (el header lleva

seed_sha256, su compromiso). Cada ítem de un parallel_map tiene su propio flujo, también bajo --replay. Las claves y los tokens (random_bytes, token, la generación de claves) siguen saliendo del SO y no se reproducen.

• Cada lectura de now() se graba, como texto ("1792711237.7256045"), así vuelve bit a bit. Las

lecturas ocupan como mucho un cuarto del sobre; pasado eso se cuentan (clock_truncated en el recibo abierto) y nunca empujan afuera una entrada.

• Con etiquetas el reloj está cercado: now() da la hora del último momento público — una

lectura de afuera (read_file) o un builtin con efecto (write_file) que corrió con el contador de programa público. El cómputo puro, print y eprint no lo mueven, así que dos now() alrededor de una rama privada (o de cualquier cómputo) leen la misma hora y su diferencia no mide cuánto tardó la rama. Sin etiquetas el reloj es el real, solo grabado.

-- Doc example: a sealed receipt for an auditor (engine v0.6.46+).
-- Runs ONLY with `--labels --auditor <public key>`: without an auditor, the `reveal`
-- inside a branch decided by a private value is a label_violation (its audit line
-- would tell which way the branch went). With one, it runs and its audit line goes
-- into the envelope only the auditor opens. `synsema test` has no --auditor, so this
-- tree is run, verified, opened and replayed (see the CI step that runs it).
intent: "doc example: sealed receipt"
require secret("DEMO_TOKEN")
require reveal("DEMO_TOKEN")
require random
require time

let token be secret("DEMO_TOKEN", "not-a-real-token")   -- outside the branch: secret() is a sink too
let tier be private(7, "app")

when tier > 5
    let plain be reveal(token)                           -- audited into the envelope, not reveal.log

-- The seed of random() is recorded in the envelope, and so is each clock reading:
-- `synsema run --replay <opened receipt>` gives these same numbers back.
let draw be random_int(1, 1000000)
print("draw: " + text(draw))
print("started at: " + text(now()))

Abrir y verificar — synsema receipt open / verify§

• synsema receipt verify <archivo> comprueba la firma. Un recibo: imprime `{"ok": true,

"header": {…}}, exit 0; uno malo imprime el motivo en stderr, exit 1 (the receipt's signature does not verify (the header, the public part, the envelope or the root was changed)). Un archivo de serve --receipt (un recibo por línea): los comprueba todos e imprime {"ok": false, "receipts": 3, "bad": [{"line": 2, "error": "…"}]} (exit 1 si alguno está mal), nombrando también una línea que empieza como un recibo y no lo es (the line names a sealed receipt but is not one (cut or changed)). Cada recibo vale por sí solo: un recibo borrado entero del archivo, o cortado antes de su primera clave, no se nota. Un archivo sin nada que parezca un recibo (o con un único recibo cortado): <archivo> has no sealed receipt`, exit 1.

synsema receipt open <archivo> --key <privada | @archivo> [--line N] (el auditor) comprueba la firma, abre el sobre y comprueba la cadena. verify solo comprueba la firma; open además comprueba la cadena, así que una entrada sacada de la parte pública se detecta ahí aunque quien tiene la clave de firma haya refirmado el recibo. Imprime una línea JSON:

{"header": {…},
 "entries": [{"seq": 0, "sealed": false, "entry": {…}},
             {"seq": 5, "sealed": true, "entry": {"kind": "capability", "capability": "reveal(\"TOK\")", "…": "…"}},
             {"seq": 6, "sealed": true, "entry": {"kind": "op", "line": "… reveal result=granted name=TOK at=p.syn:10 …", "log": "reveal.log"}}],
 "seed": "<hex>", "clock": ["1792740972.0779805"], "truncated": 0}

• entries es la corrida entera en orden, públicas y selladas; clock_truncated aparece solo

cuando se descartaron lecturas.

• --key toma la privada misma o @archivo. En un archivo con varios recibos, --line N

(1, 2, …) elige uno; sin él: <archivo> has 2 sealed receipts (lines 1, 2): pick one with --line N.

• Errores, todos exit 1 salvo que se indique: los errores de firma de verify; `the envelope does

not open with this key (wrong key, or the envelope or the header was changed); the chain does not verify: the entries are not the ones the run signed; --key is not base64url: …; line 5 of <archivo> is not a sealed receipt; --key <auditor private key> is required (exit 2); --line takes a line number (1, 2, …) (exit 2); cannot read <archivo>: <error del SO>`.

Correrlo de nuevo — synsema run --replay <recibo abierto>§

synsema run --replay opened.json program.syn vuelve a correr el programa con la semilla grabada y las lecturas de reloj grabadas, y compara cada entrada que lee, en orden, con la que leyó la corrida grabada (source y sha256). En la primera que difiere se corta, nombrándola:

Runtime error: p.syn:5:19: replay: input #1 differs from the recorded run — read_file returned sha256 27dd…, the recorded run read read_file with sha256 2c8b…

Al terminar escribe una línea en stderr: replay: the 1 inputs match the recorded run (same seed, same clock readings) (exit 0), o replay: the run read 0 of the 1 inputs of the recorded run (exit 1).

• Toma el recibo abierto: `--replay: run.json is not an opened receipt (run synsema receipt

open <receipt> --key <private> first) (exit 2). Pasá --labels` si la corrida lo tenía.

• No se combina con --auditor, --explain, --format json ni --attest: `--replay runs the

program again against an opened receipt; drop --auditor/--explain/--format json/--attest (exit 2). serve no tiene --replay`.

• No comprueba el programa: reproduce el archivo que le des. Compará antes header.program_sha

con synsema code sha program.syn.

• Los efectos son reales: el programa vuelve a correr de verdad, así que un replay vuelve a

escribir sus archivos. Hacé el replay donde sus efectos no dañen.

• Las lecturas de now() más allá de las grabadas (un programa que lee el reloj más veces, o

lecturas que el sobre cortó) salen del reloj real, sin aviso, y la línea final igual dice same clock readings. Cuando el sobre cortó algo, avisa antes: synsema run --replay: warning: the recorded run truncated N sealed entries; the comparison covers what the envelope kept.

Lo que no esconde§

• Que la corrida tocó datos privados: steps ya es null (en run --format json, en

run --attest).

• La hora de la corrida: started está en el header, y cualquiera ve cuándo salió el recibo.

(Para wasm, ver WebAssembly.)

• Si se cortó por un error o un límite: el exit code y la respuesta son públicos, y una corrida

con error igual escribe su recibo. Un bit por corrida, o por request.

• El recibo sellado no es receipt(): ese es la Verifiable Credential de

Identidad de agentes, que el programa pide y publica él mismo.

Diagnósticos de error (opt-in)§

El run plano imprime una línea estable (Runtime error: file:line:col: msg). Para un reporte rico — contexto de fuente, call stack, variables visibles, clasificación, sugerencias — optá por:

synsema run --explain program.syn                # legible, en stderr
synsema run --explain --format json program.syn  # estructurado, para tools/agentes

El exit code no cambia (1 al fallar, 0 al tener éxito) en cualquier caso.