Capacidades y seguridad

Etiquetas de flujo de información

Las capacidades responden ¿este programa puede tocar la red?. Las etiquetas responden ¿puede salir este valor? Marcás un valor como perteneciente a un principal, y el motor arrastra esa marca por cada operación — aritmética, texto, lectura de campos, json_encode, hashes, y las ramas que se tomaron por su causa — y se niega a dejarla llegar a un sumidero público hasta que digas, por escrito y en el registro, por qué puede publicarse.

Esto lo querés cuando el operador corre el código pero no debe leer el dato: un despliegue confidencial (TEE/enclave), un servicio multi-inquilino que no debe cruzar inquilinos, cualquier cosa donde "somos cuidadosos" no sea una respuesta aceptable.

Cómo se enciende§

Apagado por defecto. synsema run app.syn se comporta exactamente como siempre, hasta en el contador de pasos.

synsema run  --labels app.syn
synsema test --labels app.test.syn
synsema serve --labels app.syn
synsema serve --attested app.syn    # acá las etiquetas están SIEMPRE encendidas

Con las etiquetas apagadas, private(…) falla en el momento en que se lo llama — private: labels are off; run with --labels or serve --attested. Ojo: llamado, no cargado: synsema check pasa, y un private(…) dentro de una rama que nunca corre nunca dispara. Si el programa tiene que negarse a arrancar sin etiquetas, llamá una arriba de todo.

Dentro de un adaptador guest (Vela) también están siempre encendidas — ver Vela.

Los cuatro builtins§

let balance be private(1200, "app")        -- this belongs to the principal "app"
let doubled be balance * 2                 -- private(app) — every operation propagates
print(label_of(doubled))                   -- [private(app)]  ← redacted, see below
print(is_private(doubled))                 -- private(app)  ← redacted too
let code be declassify("insufficient", "the outcome code is public on-chain")
print(code)                                -- insufficient

• private(valor, "principal") — marca un valor. El principal es un literal de texto escrito en la llamada: un principal calculado se rechaza, porque elegir el principal a partir de un dato privado sería un canal en sí mismo. Sobre una lista o un map hace una copia privada, así que un alias público que alguien ya tenía sigue viendo el original público (desde el motor v0.6.29 las listas y los maps son valores en todos lados, así que es la misma copia-al-escribir que recibe cualquier let).
• declassify(valor, "motivo") — publicarlo, en el registro. El motivo es obligatorio y público. Cada declassify se loguea con su línea de origen y lo lista synsema code check --json antes de que corra nada, que es lo que lee un auditor.
• declassify(valor, "motivo", [...]) — acotar en vez de publicar. El tercer argumento tiene que ser un subconjunto de aquello a lo que el valor ya es privado, porque declassify sólo puede acotar. Un valor privado a ["app", "bank"] puede salir privado sólo a ["bank"]; pedirle ["bank"] a un valor privado a "app" es ensanchar, y el motor lo rechaza por su nombre (cannot widen a label — [bank] is not a subset of what this value is private to).
• label_of(v) → los principales, como lista de textos (["bank"]); is_private(v) → bool. Las dos respuestas son tan privadas como aquello que preguntaste. Si volvieran públicas serían un oráculo: un bit por pregunta, y la rama que tomes sobre la respuesta sería una rama pública sobre un dato privado. Usalas para decidir adentro del programa, no para reportar.

Acotar, en un ejemplo:

let joint be private(private(500, "app"), "bank")   -- private to both
let only_bank be declassify(joint, "the bank settles it", ["bank"])
print(declassify(label_of(only_bank), "probe"))   -- ["bank"]

Compará la lista, no su texto: desde el motor v0.6.29 un texto dentro de una lista se imprime entre comillas, así que text(label_of(only_bank)) es ["bank"], no [bank] — un test que comparaba contra la forma vieja ahora falla.

Estos nombres, más print, están protegidos: un programa no puede ligarlos a algo invocable. Redefinir uno desetiquetaría en silencio sus propias fuentes y engañaría al listado de auditoría.

Se llaman por su nombre, en ningún otro lado (motor v0.6.46+, breaking)§

declassify y private sólo se pueden llamar por su nombre. Leer cualquiera de los dos como valor es un error de carga — el programa no arranca, ni siquiera su primera línea:

let d be declassify                -- an alias
let xs be [declassify]             -- a list entry
let m be {"k": declassify}         -- a map entry
f(declassify, x)                   -- an argument
task g()
    give private                   -- a returned value
call(declassify, {"value": x})     -- also through call()
let m be {private: 1}              -- a BARE key evaluates the name, so this is one too

Runtime error: app.syn:1:10: 'declassify' is read as a value here (an alias, a list or map entry, an argument): it can only be called by its name, `declassify(…)`, so that every call is in the review (`synsema code check`)

Antes de v0.6.46 cada una de esas formas publicaba de verdad mientras synsema code check --json no listaba ninguna, así que la revisión no veía la llamada. Ahora no hay declassify que el inventario no vea, y su campo declassify_static_only desapareció (una herramienta que lo leía tiene que dejar de hacerlo). Cada entrada es {file, line, column, reason, to, constant}, con to = null para la forma de dos argumentos y la lista destino para la forma que estrecha. Un programa que lee declassify como valor da "ok": false, el error de carga en errors y una lista declassify vacía.

• Arreglo: llamalo por su nombre, declassify(x, "por qué"). El pipe x |> declassify("por qué") es una llamada por nombre y sigue andando.
• Una clave de mapa que se escribe como uno de ellos va entre comillas: {"private": 1}. Una clave desnuda se evalúa (v0.6.45 imprimía {builtin:private: 1}).
• Ligar el nombre a un valor sigue cargando (let private be 5, un parámetro llamado private): ahí el nombre es ese valor.
• El error salta con o sin --labels, en synsema run, synsema test (como falla de <setup>) y synsema code check. El chequeo de parseo, synsema check, no lo reporta.

-- Doc example: information-flow labels. Runs under `synsema test --labels` ONLY —
-- with labels off `private(...)` is a load error, which is the point: a program that
-- needs the second wall says so, instead of silently running without it.
intent: "doc example: information-flow labels"
-- v0.6.46: whose private data this program may send to a model the HOST allows
-- (`--cap-set "llm=customers@<provider host>"`). It also covers calls with public data.
require llm("customers")

let BALANCE be private(1200, "app")

task doubled()
    -- Every operation carries the union of its operands' labels.
    give BALANCE * 2

task marking_a_list_copies_it()
    -- `private` over a container gives a PRIVATE COPY: the public alias keeps
    -- seeing the public original, so marking cannot retroactively hide what
    -- someone else already holds.
    let public_rows be [1, 2, 3]
    let secret_rows be private(public_rows, "app")
    give public_rows[0]

task parse_untrusted(payload)
    -- An error CAUSED by private data is not catchable (whether an operation
    -- failed is exactly the bit labels exist to hide), so `try`/`recover` is not
    -- the answer for input an enclave receives from anyone. The total variant is:
    -- no error, so no bit.
    let d be json_decode(payload, nothing)
    when d == nothing
        give "malformed"
    give "ok"

task published()
    -- The only way out is on the record: the reason is mandatory and public, and
    -- `synsema code check --json` lists every declassify before anything runs.
    give declassify(BALANCE > 0, "whether the account is open is public")

test "labels propagate through arithmetic"
    assert(is_private(doubled()))
    assert_eq(text(declassify(doubled(), "doc example")), "2400")

test "the answer about a private value is as private as the value"
    -- `is_private`/`label_of` are NOT public oracles: one bit per question would
    -- be a channel of its own.
    assert(is_private(is_private(BALANCE)))
    assert(is_private(label_of(BALANCE)))

test "marking a container copies it"
    assert_eq(marking_a_list_copies_it(), 1)

test "untrusted input is parsed without exceptions"
    assert_eq(parse_untrusted("{\"a\": 1}"), "ok")
    assert_eq(parse_untrusted("not json at all"), "malformed")

test "declassify is the only way out, and it is on the record"
    assert_eq(published(), true)

test "text() does not sanitise: it is still the value, and still private"
    -- The redaction happens at the SINK, not in the conversion. Passing a private value through
    -- `text()` does not make it safe to hand around.
    assert_eq(declassify(is_private(text(BALANCE)), "doc example"), true)
    assert_eq(declassify(text(BALANCE), "doc example"), "1200")

test "a private value inside a concatenation takes the WHOLE string with it"
    -- At a public sink the entire line is replaced by `private(app)` — the prefix goes too.
    let line be "balance: " + text(BALANCE)
    assert_eq(declassify(is_private(line), "doc example"), true)
    assert_eq(declassify(line, "doc example"), "balance: 1200")

test "the third argument of declassify narrows WITHIN the value's own principals"
    let joint be private(private(500, "app"), "bank")
    let only_bank be declassify(joint, "the bank settles it", ["bank"])
    -- label_of gives the principals as a list of texts (itself private, so declassify to compare)
    assert_eq(declassify(label_of(only_bank), "doc example"), ["bank"])
    -- and `text` of that list quotes each principal, like any text inside a list
    assert_eq(declassify(text(label_of(only_bank)), "doc example"), "[\"bank\"]")

-- v0.6.46: a map key spelled like a protected name is written quoted. A bare key evaluates the
-- name, and reading `private` or `declassify` as a value is a load error.
test "a key named like a protected builtin is quoted"
    let m be {"private": 1, "declassify": 2}
    assert_eq(m["private"] + m["declassify"], 3)

-- v0.6.46: `sandbox under` can delegate `declassify` for some principals to one block.
test "sandbox under delegates declassify for the principals it names"
    let r be 0
    sandbox under {"declassify": "app"}
        set r to declassify(BALANCE, "the balance is shown to its owner")
    assert_eq(r, 1200)

-- v0.6.46: what receipt() publishes after private data does not depend on it.
test "receipt(): steps is nothing, declassified[].from is the declared set"
    let pub be declassify(private(7, "bank"), "probe")
    let r be receipt().credentialSubject
    assert_eq(r.steps, nothing)
    let last be r.declassified[length(r.declassified) - 1]
    assert_eq(last.reason, "probe")
    assert_eq(last.from, ["app", "bank"])   -- every principal the program declares, not the value's own
    assert_eq(last.to, [])

test "a declassify inside a private branch is left out of the receipt"
    let before be length(receipt().credentialSubject.declassified)
    let shown be private(0, "app")
    when BALANCE > 1000
        set shown to declassify(BALANCE, "inside a private branch")
    assert_eq(length(receipt().credentialSubject.declassified), before)

-- v0.6.46: `require llm("P")` also covers the calls with public data (it used to break them).
test "require llm(principal) still allows calls with public data"
    when not llm_available()
        assert(starts_with(reason about "the weather", "[reasoning about"))

-- v0.6.55: a mask keeps the label and never branches; an array is private as a whole.
let SCORES be private(array([1, 5, 2, 8]), "app")

task index_one()
    give 1

test "masks over a private array give private results, without a cut (engine v0.6.55+)"
    let m be SCORES > 2
    assert(is_private(sum(m)))
    assert_eq(declassify(sum(m), "doc example"), 2)
    assert_eq(to_list(declassify(where(SCORES, m), "doc example")), [5, 8])
    assert_eq(to_list(declassify(apply(SCORES, (v) => v * 10), "doc example")), [10, 50, 20, 80])

test "a private array takes private values; an index that runs code cannot write inside a list (engine v0.6.55+)"
    let q be private(zeros(3), "app")
    set q[0] to private(5, "app")
    assert_eq(to_list(declassify(q, "doc example")), [5, 0, 0])
    let L be [zeros(3)]
    let said be ""
    try
        set L[0][index_one()] to 2
    recover e
        set said to e
    assert(contains(said, "an index that runs code writes into an array inside a list or map"))
    let i be index_one()
    set L[0][i] to 2
    assert_eq(to_list(L[0]), [0, 2, 0])

Qué es un sumidero§

Cada operación lleva la unión de las etiquetas de sus operandos. Un sumidero público es cualquier lugar donde un valor sale de la memoria del propio programa: la respuesta HTTP y todo stream, el resultado on-chain de un guest, un archivo, una petición saliente, otro intérprete (parallel_map, run_program, cron, el bus, el enjambre). Un valor privado en un sumidero es un label_violation — el request falla, y el mensaje nombra el camino que recorrió el valor, jamás el valor.

Dos que sorprenden:

• Ramificar sobre un valor privado vuelve privada la rama. Todo lo que la rama haga lleva la etiqueta, porque cuál rama corrió es el secreto. print/show/log adentro de una rama privada se rechazan: stdout es público y la cantidad de líneas no se redacta, así que una línea por iteración deletrea el dato.
• Imprimir un valor privado está bien — sale como private(app). La redacción es la respuesta; el rechazo es para la rama.
• text(v) no sanea. La redacción ocurre en el sumidero y en ningún otro lado: text devuelve el contenido real, todavía privado. is_private(text(v)) da true, y declassify(text(v), …) devuelve el valor entero — pasar un valor por text no lo vuelve seguro para andar dándolo por ahí.
• Un privado adentro de una concatenación se lleva toda la cadena. print("saldo: " + text(v)) imprime private(app), no saldo: private(app): el prefijo ahora es parte de un texto privado, y el sumidero reemplaza todo junto.
• Una plantilla escribe un valor privado como su valor, y el HTML lleva su etiqueta (motor v0.6.50+). Con <p>{c.name} {upper(c.name)}</p> y un c privado, render da <p>Ana ANA</p> con la etiqueta [private(customers)]: el sumidero (la respuesta, print) redacta o rechaza la página entera, nunca un hueco. Hasta v0.6.49 la llamada escribía el marcador (<p>Ana private(customers)</p>) mientras el campo simple escribía el valor. Un valor privado que la plantilla lee de otro lado — escrito, o decidiendo un { when } — también etiqueta el HTML.

Tres que tocan capacidades y el log de auditoría (motor v0.6.45+):

• Un require no puede depender de un dato privado. Un require adentro de una rama decidida por un valor privado, o con un scope privado (require net(host_privado)), es un label_violation: `require net runs in a branch decided by a private value (or its scope is private); what is granted cannot depend on private data`. Declará las capacidades arriba de todo del programa. Lo mismo vale para un require adentro de un task — es el techo de la herramienta en call_tool — así que un task cuyo require tiene un scope privado, o que está definido en una rama privada, es un label_violation`.
• Lo que escribe el log de auditoría no corre en una rama privada. sign y los builtins de firma, spend, reveal y las operaciones de wallet escriben una entrada en su log de auditoría, y que esa entrada exista le dice al operador para qué lado fue la rama. Llamados bajo una rama privada fallan con label_violation y no escriben nada. Decidí con un valor público, o hacé declassify de la condición antes — eso deja su propio registro:

require secret("API_KEY")
require reveal("API_KEY")
let key be secret("API_KEY", "demo")
let balance be private(1200, "app")
let big be declassify(balance > 1000, "whether the balance is over 1000 is public")
when big                                    -- a public branch: reveal may run here
    let plain be reveal(key)

• Un chequeo de capacidad adentro de una rama privada no deja entrada de auditoría (en --audit y en @synsema/wasm): cuántas entradas hubo diría para qué lado fue la rama, o cuántas veces corrió un loop privado. Desde el motor v0.6.46 una operación de LLM o de juez en una rama privada se rechaza antes de su chequeo de capacidad, así que tampoco deja una entrada "granted llm".
• Con un auditor (motor v0.6.46+) el host puede dejar correr esas operaciones: synsema run --labels --auditor <clave pública X25519> --receipt <ruta> app.syn corre un reveal, un sign o una operación de wallet adentro de una rama privada y pone su línea de auditoría en un recibo sellado que sólo el auditor puede abrir. Sin --auditor se rechazan como arriba. Ver Atestación.

declassify es una capacidad: el programa la declara, el host la acota (motor v0.6.46+, v0.6.49+)§

declassify es el único lugar por donde sale un dato privado. Sin techo no cambia nada: el runtime la concede, como unsafe en tu propio crate de Rust — explícita, con su razón obligatoria, y listada entera por synsema code check --json. Bajo un techo (motor v0.6.49+) funciona como require net: el programa publica sólo los principales que declara con require declassify("<principal>"), y sólo los que el techo del host también permite. Nada se concede del ambiente.

synsema run --labels --cap-set "stdout,declassify=customers" app.syn

require declassify("customers")                 -- under a ceiling, what the program publishes
let c be private(3, "customers")
sandbox under {"declassify": "customers"}       -- delegate it to this block only
    print(declassify(c, "the count is public"))

• Lo que se chequea es lo que la llamada saca. declassify(v, "por qué") saca todos los principales de v. La forma que estrecha saca el resto: bajo declassify=app, un valor privado de ["app", "bank"] se puede estrechar a ["bank"]. Un declassify de un valor que no es privado no saca nada y siempre pasa.
• El require pasa por el techo como cualquier otro. Bajo declassify=customers, un require declassify("billing") se rechaza, y también uno desnudo (require declassify: es más ancho que el techo y se rechaza entero, como require net bajo net=api.example.com). Uno desnudo sólo lo permite un techo desnudo (declassify o declassify=*), y avisa al arrancar: `synsema: warning: bare require declassify permits publishing data private to ANY principal; scope it with require declassify("principal") (the principal the call removes)`.
• Dónde va la línea. En el preámbulo del programa, para el código del programa. Un agente declara las suyas: el require del programa no lo alcanza, así que un declassify adentro de un agente necesita require declassify("customers") en el cuerpo de ese agente (un agente lanzado por otro también declara las suyas), y un parallel_map adentro del agente hereda las del agente. Una task de confianza la declara en su propio cuerpo, acotada por --trusted-cap-set.
• Breaking (v0.6.46, y después v0.6.49). Desde v0.6.46 un programa que desclasifica con --labels bajo --cap-set, --sandbox o --deterministic necesita declassify=<principal> en el --cap-set (--sandbox y --deterministic nunca la conceden: pasá a un --cap-set explícito como --cap-set "stdout,time,declassify=app"). Desde v0.6.49 además necesita require declassify("<principal>") en el programa, el agente o la task de confianza que desclasifica; antes decidía sólo el techo.
• Un rechazo es un label_violation que try/recover no atrapa — si pasa o no depende de la etiqueta real del valor, así que un rechazo atrapable sería un oráculo. Como todo label violation termina la corrida y retiene la salida en buffer. Un rechazo sólo ocurre bajo un techo, así que el programa ve el texto fijo (Qué muestra un corte, y a quién); el detalle del operador (el recibo sellado con --auditor) dice dónde va la línea:

app.syn:3:17: label_violation: declassify is not granted for what this value is private to (customers). With a ceiling the program declares what it publishes (`require declassify("<principal>")` in the program's preamble, or in the body of the agent that runs this code: an agent declares its own, also for its `parallel_map`) and the host's ceiling has to allow it too (`--cap-set declassify=<principal>`); inside a `sandbox` only a `sandbox under` that delegates `declassify` allows it

• El detalle nombra el lugar que corresponde: adentro de un agente, ese agente (… add require declassify("<principal>") to the body of agent Sub …); adentro de un módulo de confianza, la task exportada y --trusted-cap-set (Módulos de confianza).
• El conjunto entre paréntesis es el conjunto declarado del programa — todos los principales que marca en algún lado — nunca la etiqueta real del valor, que diría qué valor era. La línea de log [INF] declassify: … (from […] to […]) también nombra el conjunto declarado ([…] cuando el programa no declara ningún principal).
• Sin --labels no se chequea nada: private(…) falla (las etiquetas están apagadas) y declassify es la identidad.
• El guest de Vela corre su app bajo stdout,declassify=app: su único principal es app, y la app declara require declassify("app") y publica ella misma sus códigos de resultado y sus recibos de retiro (Vela).

Qué publica receipt() después de un dato privado (motor v0.6.46+)§

Con --labels, receipt() ya no lleva lo que dependió de un valor privado. Cada uno era una fuga con el contador de programa público y sin label_violation:

• steps es nothing una vez que se vio un valor privado (era la cuenta cruda: un loop sobre un n privado daba su tamaño). Antes del primer valor privado es el número.
• declassified[] lista {reason, from, to, line}, y from es el conjunto declarado, no la etiqueta real del valor (["a", "b", "c"] aunque el valor fuera privado sólo de a y c). Un declassify adentro de una rama privada queda fuera de la lista, y su línea [INF] declassify no se escribe: cuántos hubo decía qué rama corrió.
• inputs: una lectura adentro de una rama privada (read_file, env, …) se rechaza como sumidero (read_file called under private control flow …), así que nunca llega a la lista.

read_line, flush y el orden de la salida (motor v0.6.46+)§

• El prompt de read_line(prompt) es un sumidero público, como print. Un prompt privado, o un prompt adentro de una rama privada, es un label_violation, y cada uno dice cuál (motor v0.6.49+; antes los dos decían "control flow"): `the read_line prompt is private (to a) and the prompt goes to stdout, which is public … y read_line prompt under private control flow (pc = [a]); stdout is public …. read_line()` sin prompt adentro de una rama privada está permitido.
• Con --labels, flush() y read_line no escriben en vivo la salida pendiente. print ya la guardaba hasta el final; ahora los prompts salen primero y las líneas impresas al final — print("one"), flush(), read_line("> ") muestra > one. Cuántas líneas salían antes de un prompt podía depender de una rama privada. Sin --labels no cambia nada.

Datos privados a un modelo, herramientas que escribió una persona (motor v0.6.46+)§

Dos formas en que un dato privado ahora puede hacer trabajo útil sin que el programa lo publique:

• Un modelo que eligió el host. Con require llm("customers") en el programa y --cap-set "llm=customers@api.anthropic.com" en el techo del host, reason, generate, llm_step… pueden llevarle datos privados de customers a ese proveedor, y la respuesta sigue privada. Las reglas están en Primitivas LLM; el juez tiene su propio ítem, judge=customers@… (Juez).
• Herramientas de confianza. Bajo un techo sin declassify, el código que escribió un modelo no puede publicar nada privado, pero el host le puede dar herramientas que escribió una persona, cuya propia política desclasifica: synsema run --labels --cap-set stdout --trusted tools=./tools.syn app.syn, y después use "trusted:tools" as t. Ver Módulos § Módulos de confianza.

Arrays (motor v0.6.55+)§

Las máscaras conservan la etiqueta y nunca ramifican. Una comparación sobre un array privado da una máscara privada, y sum(m), where(a, m), some(m), if_else(m, x, y) y apply dan resultados privados — sin corte, porque nada corrió bajo una condición privada. Por eso la máscara es el camino nativo para datos privados.

require declassify("x")
let p be private(array([1, 5, 2, 8]), "x")
let m be p > 2
print(declassify(sum(m), "x"))         -- 2
print(declassify(where(p, m), "x"))    -- [5, 8]

• Un array es privado entero, no elemento por elemento. Escribir un valor privado en un array público corta la corrida: label_violation: cannot write a value private to x into the array 'pub' (public): an array is private as a whole, not element by element — bind it as private(…, "<principal>") first, or declassify the value. El chequeo es contra la variable desde la que se llega al array, no contra los contenedores del medio: set m.a[0] to v se chequea contra m. Un índice privado en un array público también es una violación.
• Escribir en un array adentro de una lista o un map pide índices que no corren código: set L[0][f()] to 2 → label_violation: an index that runs code writes into an array inside a list or map — compute the index into a variable first.
• Un error de set que depende de un dato privado no es atrapable — un índice privado fuera de rango (set xs[secret]), el largo de una lista o un array privado recorrido con un índice público, la forma o el tipo de un valor privado. Corta la corrida con private(x) y el lugar, como el mismo error en una lectura. (Antes de v0.6.55 un try lo atrapaba, y su texto mostraba el dato.)
• Un try cuyo cuerpo escribió en una lista, un map o un array privado corre su recover bajo ese contexto privado, como si lo hubiera leído (breaking). Un recover que después asigna una variable pública corta la corrida (cannot assign to 'fails' (public) under private control flow …): sacá la escritura del try, o hacé privado el contador (let fails be private(0, "x")).
• Cuando la sentencia tocó datos privados, los errores de la escritura le llegan al operador como diagnóstico, y el programa ve el texto fijo del corte (§ Qué muestra un corte, y a quién).

Errores que no se pueden atrapar§

Un error nacido bajo una rama privada, o causado por un dato privado, no es atrapable: try/recover lo re-propaga y assert_error no lo absorbe. Que una operación haya fallado es exactamente el bit que las etiquetas existen para esconder — xs[indice_privado], 1 / (secreto - i) — y un recover que se lo tragara dejaría que el bucle anterior deje el secreto en una variable pública.

¿Entonces cómo validás input no confiable, que es lo que un enclave recibe de cualquiera? No fallando. Las operaciones que parsean entrada externa tienen una forma total que devuelve un reemplazo:

let d be json_decode(payload, nothing)              -- no error, so no bit
let n be number(field, nothing)
let clear be aes_gcm_decrypt(k, nonce, ct, aad, nothing)

También decimal, float, toml_parse, abi_decode, bech32_decode, rlp_decode. El reemplazo se evalúa siempre (un efecto adentro dispara también en el camino feliz) y nunca se traga una violación de etiquetas — eso sería un try/recover encubierto.

Qué muestra un corte, y a quién (motor v0.6.47+)§

Un corte del chequeo de flujo — cualquier label_violation — le decía al programa dónde cayó: el builtin, el argumento, la línea. Eso era un canal en sí mismo, porque un valor privado puede elegir cuál de N sitios falla, y en un loop de agente el error vuelve al modelo. Ahora lo que ve el programa lo decide quien lo corre:

En todos los casos, la salida que se imprimió antes del corte se reemplaza por una sola línea:

private(labels): the run was stopped by the flow checker; its output is withheld because the NUMBER of lines before the stop depends on private data

y el error fijo es:

Runtime error: label_violation: the flow checker stopped the run (private to customers); what failed, where and how to fix it go to the operator, not to the program

El conjunto entre paréntesis es el conjunto declarado del programa, una constante del programa, nunca la etiqueta del valor que falló. Medido en v0.6.47 con el mismo programa: synsema run --labels cut.syn imprime cut.syn:4:10: label_violation: print called under private control flow (pc = [customers]) …, y synsema run --labels --cap-set stdout cut.syn imprime el error fijo de arriba. Para depurar un corte, corrélo vos sin techo, leé operator_detail en WebAssembly o abrí el recibo como auditor (Observabilidad). Los mensajes que citan otras páginas (fetch(argument 0) is private to …, declassify is not granted …, reason would send data private to …) son ese detalle.

• Un corte en un agente corta la corrida a la que pertenece. Bajo run es el programa entero: termina con el mismo error fijo (sin techo, el detalle empieza con agent Leaky_0: …). Bajo serve --labels es el request o el tick que lanzó al agente. Desde ese momento falla cada sumidero de esa corrida.
• Bajo serve --labels, cada request, tick de cron y handler de socket es su propia corrida. Su stdout y su stderr se retienen y se escriben cuando termina, o se reemplazan por la línea fija si la cortaron; lo que imprimen los agentes no se escribe. El servidor lo avisa al arrancar: [serve] labels: request and cron output is logged when each one ends, and not at all if a label cut stopped it; agent output is not logged (which agent stopped would be the private data). Para ver el log en vivo mientras desarrollás, corré sin --labels. agents() y agent_stop ven sólo los agentes de la misma corrida.
• Bajo serve --labels, lo que una corrida escribe en el blackboard y las señales entra todo junto o nada. Una corrida — el request, o el preámbulo, con cada agente que lanzó — se confirma cuando termina entera sin corte, y se deshace si alguna parte se corta, incluido lo que sus agentes escribieron después de que el request respondió. Medido: una ruta que hace share "should be undone" as "b" y después cae en un corte responde 500, y el observe "b" de un request posterior da nothing, mientras que el share de una ruta limpia queda. Lo que otras corridas leyeron mientras estaba abierta, y las señales ya consumidas, quedan — como cualquier efecto antes de un corte.

Qué sale del proceso§

Un error redactado dice private(app) y nada más — ni archivo:línea:columna. Si el secreto elige cuál de N sitios falla, la ubicación vale log₂(N) bits. Los principales que nombra son los que el programa declara, jamás los de ese valor en particular: nombrar los propios era un canal, porque en un despliegue multi-inquilino el principal es el inquilino.

El auditor igual se entera de por qué (motor v0.6.50+). Un error cuyo texto se redactó porque tocó datos privados — when c.name == "Ana" y después 1 / 0 da Runtime error: b.syn:3:16: private(customers) sin techo — pone su texto real en el recibo sellado, que sólo abre el auditor, con o sin techo: synsema receipt open muestra una entrada {"sealed": true, "entry": {"kind": "label_violation", "detail": "b.syn:3:16: Division by zero"}}. Con techo el programa sigue viendo el mismo texto fijo, y el detalle del operador (un log) sigue redactado, con su ubicación. Mirá Observabilidad.

Una violación de etiquetas además termina toda la corrida de synsema test --labels, con un solo veredicto que la nombra, en vez de un ✗ en ese bloque y la suite siguiendo — ocho bloques sondeando un bit cada uno y la columna de ✓/✗ deletrea el byte. Una falla ordinaria sigue siendo veredicto por bloque.

Límites, dichos§

• La terminación es un bit por corrida, y bajo un servidor una corrida es un request. Una corrida que el chequeador cortó le dice a un observador que se cortó. Bajo serve quien llama elige cuántas corridas hacer, así que es un bit por request, sin techo: ocho requests públicos recuperan un valor por búsqueda binaria. Si el resultado de un request no debe depender de un dato privado, no dejes que una rama privada decida si falla.
• Progreso. Los efectos hechos antes del corte ocurrieron. El motor retiene la salida en buffer y revierte lo que el request escribió en el store compartido state_* y, desde v0.6.47 bajo serve --labels, en el blackboard y la cola de señales — todo vive en su propia memoria — pero un archivo o una llamada saliente no los puede deshacer.
• Tiempo y uso de recursos no se modelan en absoluto.
• Cruzar a otro intérprete rechaza, a propósito: el canal sí lleva etiquetas, pero qué puede hacer un worker con un valor privado todavía no está especificado, y la alternativa que reemplazó era peor (el worker recibía el valor ya despojado y hacía el efecto en claro mientras el resultado volvía etiquetado, así que la fuga parecía rastreada).

Sigue§

Las etiquetas mantienen el dato adentro. La attestation es la otra mitad: probarle a un tercero remoto qué código lo está sosteniendo.