FullAgenticStack: Semantic Behavior Type: LinearAutoDestroy

Existe uma classe inteira de bugs e falhas de segurança que nasce de uma suposição errada: a de que o programador sempre vai lembrar de destruir, invalidar, limpar, revogar ou consumir corretamente um valor sensível depois do seu uso.

Essa suposição é fraca.

Na minha concepção, uma linguagem não deveria depender do programador escrever manualmente todo o código necessário para que um comportamento obrigatório de um tipo aconteça. Se um valor possui uma regra semântica obrigatória, essa regra não deveria viver espalhada em finally, defer, drop, close, destroy, ack, delete, expire, cleanup, revoke ou em qualquer outro ritual manual. Essa regra deveria pertencer ao próprio tipo.

É exatamente essa a motivação do LinearAutoDestroy.

LinearAutoDestroy é um Semantic Behavior Type: um tipo cujo objetivo não é apenas descrever a forma de um valor, mas obrigar a execução de um comportamento semântico associado a esse valor.

Indo na contramão do baixo nível tradicional

Linguagens de baixo nível normalmente partem da ideia de que todo comportamento relevante deve estar explicitamente escrito no código. O programador aloca, move, usa, libera, fecha, destrói, revoga, limpa memória, remove arquivo, apaga segredo, confirma mensagem, descarta payload e assim por diante.

Essa abordagem dá controle máximo, mas também transfere responsabilidade demais para o humano.

O problema não é a linguagem permitir controle. O problema é uma linguagem permitir que comportamentos obrigatórios sejam opcionais na prática.

Se um valor precisa ser destruído após uso, isso não deveria depender da disciplina do programador. Se uma mensagem só pode ser consumida uma vez, isso não deveria depender de um ack manual bem posicionado. Se uma chave efêmera não pode sobreviver depois de um handshake, isso não deveria ser uma convenção de equipe. Se um token de uso único já foi lido, ele deveria carregar no próprio tipo a impossibilidade de continuar existindo como valor válido.

A minha visão vai na direção oposta: transformar o comportamento obrigatório em tipo semântico.

O programador não escreve “destrua isso depois”. O programador escolhe um tipo que já significa “isso será destruído depois do uso”.

Quanto mais simples for declarar esse comportamento, menor a chance de alguém errar. A linguagem, o runtime ou a biblioteca devem executar as ações de baixo nível de forma transparente, porque esse comportamento não é uma escolha estética. É uma propriedade de segurança.

O que é um Semantic Behavior Type

Um Semantic Type tradicional descreve a semântica de uma propriedade.

Por exemplo:

PersonCPF

UserEmail

WhatsAppNumber

PaymentToken

SessionId

Esses tipos dizem: “este valor não é apenas uma string, ele representa algo com significado específico”.

Mas LinearAutoDestroy não é apenas isso.

Ele não é um Semantic Type de propriedade. Ele é um Semantic QuarkBehavior Type.

Isso significa que ele representa um comportamento semântico reutilizável, mínimo e obrigatório.

Um QuarkBehavior é a menor unidade semântica de comportamento. Ele deve ser pequeno, reaproveitável, determinístico e específico o suficiente para ser composto em comportamentos maiores.

No caso de LinearAutoDestroy, o comportamento não existe para transformar dados de negócio, validar CPF, normalizar telefone ou calcular preço. Ele existe para impor uma regra sobre a vida útil de um valor.

A semântica é:

um valor LinearAutoDestroy pode ser usado uma vez;

depois do uso, ele deve ser destruído, invalidado ou tornado inacessível.

Ou seja, o comportamento altera o tipo efetivo do valor ao longo do tempo.

Antes do uso, o valor está disponível.

Depois do uso, ele não deveria mais ser tratável como o mesmo valor. Ele deveria virar algo como:

Consumed

Destroyed

Revoked

Invalidated

Unusable

Essa transição não deveria ser informal. Ela deveria ser parte do modelo de tipos.

O tipo não descreve apenas o que o valor é. Ele descreve o que deve acontecer com ele.

A ideia central é simples:

Value<T> + LinearAutoDestroy => Value<T, usable_once>

Depois do consumo:

Value<T, usable_once> -> Destroyed<T>

Na prática, isso significa que o tipo carrega uma obrigação de runtime.

O valor não é apenas T.

Ele é T com uma política semântica de destruição.

Exemplo conceitual:

LinearAutoDestroy<DPoPNonce>

LinearAutoDestroy<OneTimeToken>

LinearAutoDestroy<QueueMessage>

LinearAutoDestroy<EphemeralPrivateKey>

LinearAutoDestroy<PasswordResetLink>

LinearAutoDestroy<HandshakeCertificate>

LinearAutoDestroy<FileHandle>

LinearAutoDestroy<TemporaryCredential>

Nesses casos, permitir que o valor continue disponível depois do uso cria superfície de ataque.

LinearAutoDestroy existe para fechar essa superfície.

Valores que deveriam existir como LinearAutoDestroy

Alguns valores não deveriam ser tratados como valores comuns. Eles deveriam nascer com prazo semântico de vida extremamente curto.

Exemplos:

one-time password

password reset token

magic link

DPoP nonce

challenge WebAuthn

mTLS ephemeral certificate

private key efêmera

session bootstrap token

queue message com consumo exclusivo

temporary file handle

signed upload URL

signed download URL

refresh token rotacionável

idempotency claim de uso único

ack secret

decryption key temporária

Todos esses valores possuem uma característica comum: continuar existindo depois do uso é perigoso.

Em sistemas tradicionais, o programador precisa lembrar de invalidar esses valores. Em sistemas orientados por Semantic Behavior Types, o programador escolhe um tipo que já contém essa regra.

A diferença é brutal.

No modelo tradicional:

usar valor

lembrar de destruir

esperar que ninguém esqueça

esperar que nenhum erro pule o cleanup

esperar que nenhum retry reutilize o valor

esperar que nenhum log grave o segredo

esperar que nenhuma fila entregue de novo indevidamente

No modelo com LinearAutoDestroy:

declarar valor como LinearAutoDestroy

usar valor

o próprio tipo obriga a destruição

Classes de brechas que esse tipo elimina ou reduz drasticamente

LinearAutoDestroy elimina ou reduz classes inteiras de falhas relacionadas à vida útil incorreta de valores sensíveis.

A primeira é o reuso indevido.

Tokens, nonces, mensagens e certificados temporários não deveriam ser reaproveitados. Se o tipo permite múltiplos usos, ele permite replay. Se o tipo é linear e autodestrutivo, o segundo uso deixa de ser uma operação válida.

A segunda é o vazamento por retenção acidental.

Muitas falhas não acontecem porque o valor foi roubado no momento do uso. Elas acontecem porque o valor continuou existindo em memória, cache, fila, log, storage temporário, arquivo intermediário ou estrutura auxiliar depois que já deveria ter desaparecido.

A terceira é o bug de cleanup incompleto.

Todo sistema que depende de cleanup manual eventualmente terá um caminho de execução onde o cleanup falha: exceção, panic, timeout, cancelamento de contexto, retry parcial, race condition, dead letter, processo morto ou deploy interrompido.

A quarta é o replay.

Se uma mensagem de fila, token ou credencial efêmera pode ser reapresentada, o sistema precisa verificar manualmente se ela já foi usada. Com LinearAutoDestroy, o próprio tipo expressa a regra: depois do primeiro uso, a identidade operacional daquele valor não existe mais como valor válido.

A quinta é a duplicidade de consumo em sistemas distribuídos.

Filas, workers, consumers e brokers frequentemente precisam lidar com mensagens entregues mais de uma vez, consumers concorrentes e confirmações parciais. Um valor semanticamente linear deve ser consumido por apenas um caminho válido. Os demais caminhos precisam receber destruição, invalidação ou rejeição semântica.

A sexta é a falsa confiança em convenção.

Comentários, documentação e boas práticas não impedem bug. Tipo impede bug. Runtime impede bug. Protocolo impede bug. Contrato formal impede bug.

LinearAutoDestroy transforma uma recomendação em uma obrigação executável.

Por que isso é um QuarkBehavior Type

O ponto mais importante é que LinearAutoDestroy não processa dados.

Ele não normaliza.

Ele não valida formato.

Ele não calcula.

Ele não enriquece payload.

Ele não converte string.

Ele não faz parsing.

Ele impõe comportamento.

Por isso ele é um Semantic QuarkBehavior Type.

Ele é um quark porque representa uma unidade mínima de comportamento semântico.

Ele é behavior porque executa uma ação obrigatória.

Ele é type porque modifica a forma como o valor pode ser usado pelo programa.

Ele é semantic porque o motivo da existência dele não é técnico-acidental, mas conceitual: aquele valor só faz sentido se for usado uma vez e destruído depois.

Essa é a diferença entre escrever uma função destroyAfterUse(value) e declarar:

value: LinearAutoDestroy<T>

No primeiro caso, você escreveu uma intenção.

No segundo, você alterou o contrato semântico do valor.

Modelo conceitual

Um LinearAutoDestroy<T> pode ser entendido como uma máquina de estados mínima:

Created -> Armed -> Consumed -> Destroyed

Ou, de forma mais rigorosa:

Created<T>

  -> Available<T>

  -> Used<T>

  -> Destroyed<T>

A operação principal é consume.

consume(LinearAutoDestroy<T>) -> T

Mas essa operação também dispara um efeito obrigatório:

after consume:

  destroy(original_reference)

  invalidate(identity)

  revoke(capability)

  remove_from_store_if_needed

  emit_receipt

O retorno pode entregar o valor para uso imediato, mas a referência original não pode continuar válida.

Em uma linguagem com suporte nativo a tipos lineares, isso poderia ser verificado em compile-time. Em linguagens sem esse suporte, a biblioteca pode aproximar o comportamento usando ownership, wrappers, guards, runtime checks, finalizers, weak references, locks, atomic state, capability tokens ou handles opacos.

O ideal é que cada linguagem implemente o máximo possível dessa garantia de acordo com suas capacidades.

Exemplo simplificado

Em pseudocódigo:

token = LinearAutoDestroy<Token>.create(raw_token)



token.consume(use_token)



token.consume(use_token_again) // erro semântico: token já destruído

O segundo uso não deveria ser tratado como erro comum de aplicação. Ele representa violação de contrato semântico.

A mensagem correta não é apenas:

invalid token

A mensagem correta é algo como:

LinearAutoDestroyViolation:

  value was already consumed and destroyed

Isso permite rastreabilidade, auditoria e prova de que o sistema bloqueou o segundo uso.

Implementação em filas: NATS como exemplo

Um dos primeiros lugares onde esse tipo faz sentido é em sistemas de filas.

Em NATS, uma mensagem pode representar uma intenção, uma entrega de evento, um comando, uma confirmação ou uma unidade de trabalho. Em arquiteturas distribuídas, é comum existir concorrência entre consumers, retries e redelivery.

Quando uma mensagem representa algo que só pode ser consumido uma vez, ela deveria ser tratada como LinearAutoDestroy.

Conceitualmente:

QueueMessage<T> + LinearAutoDestroy

Isso significa:

a mensagem pode ser entregue;

um consumer válido pode consumir;

após o consumo, a mensagem deve ser confirmada, invalidada ou destruída;

qualquer tentativa posterior deve falhar semanticamente.

O fluxo fica assim:

NATS message received

  -> wrap as LinearAutoDestroy<NatsMessage>

  -> consumer attempts consume

  -> payload is processed

  -> ack is emitted

  -> internal handle is destroyed

  -> receipt is generated

Em caso de erro:

NATS message received

  -> wrap as LinearAutoDestroy<NatsMessage>

  -> consumer attempts consume

  -> processing fails

  -> policy decides retry, nak, term or dead-letter

  -> handle is still invalidated according to the semantic rule

O ponto é que o consumer não deve ficar livre para manter aquele handle vivo indefinidamente.

Se a mensagem foi consumida, o wrapper semântico precisa impedir uso posterior.

LinearAutoDestroy no NATS com ACK semântico

Um exemplo prático é tratar o ack não como uma chamada solta, mas como parte do comportamento do tipo.

Modelo tradicional:

msg = sub.next()

process(msg.data)

msg.ack()

Esse modelo depende do programador lembrar de chamar ack.

Modelo semântico:

msg = LinearAutoDestroy<NatsMessage>.from(sub.next())



msg.consume(process)

O consume executa o processamento e amarra a política de destruição:

consume:

  lock message

  expose payload once

  run handler

  ack/nak/term according to policy

  clear payload reference

  invalidate message handle

  emit receipt

O programador não recebe uma mensagem crua. Ele recebe um valor semanticamente armado para autodestruição.

Esse detalhe muda a arquitetura.

A fila deixa de entregar apenas bytes. Ela passa a entregar uma capability de uso único.

Por que isso é replicável para outras filas

O conceito não depende do NATS.

NATS é apenas uma primeira implementação natural porque o modelo de mensagens, subjects, consumers, acknowledgements e redelivery combina muito bem com a ideia de consumo linear.

Mas a mesma semântica pode ser aplicada em:

Redis Streams

Kafka

RedPanda

BullMQ

RabbitMQ

SQS

Pulsar

filesystem queues

in-memory queues

Cada backend terá uma implementação diferente de destruição, confirmação ou invalidação, mas o contrato semântico permanece o mesmo.

A interface conceitual é:

LinearAutoDestroy<QueueMessage<T>>

A implementação específica decide como destruir:

NATS: ack, nak, term, drain, delete consumer state

Kafka: commit offset, transactional consume, tombstone auxiliar

Redis Streams: xack, xdel, claim control

BullMQ: complete job, remove job, fail with policy

RabbitMQ: ack, reject, nack, dead-letter

O tipo semântico não precisa saber todos os detalhes do backend. Ele precisa declarar a obrigação. O adapter executa a obrigação de acordo com o sistema de fila.

Arquivos também deveriam usar esse modelo

Filas são apenas o começo.

Arquivos temporários, handles de upload, buffers criptográficos, certificados efêmeros e chaves temporárias também deveriam ser tratados como LinearAutoDestroy.

Exemplo:

LinearAutoDestroy<TempFile>

LinearAutoDestroy<UploadHandle>

LinearAutoDestroy<PrivateKeyBuffer>

LinearAutoDestroy<DecryptionKey>

LinearAutoDestroy<SignedFileURL>

O uso de arquivos tem várias brechas clássicas:

arquivo temporário esquecido no disco

buffer sensível não zerado

descritor de arquivo mantido aberto

upload URL reutilizada

arquivo descriptografado mantido em cache

conteúdo sensível salvo em pasta temporária

processo morre antes de apagar o arquivo

Um proxy de arquivos baseado em LinearAutoDestroy pode resolver isso no nível correto: não como disciplina de código, mas como contrato semântico de uso.

O programador não deveria abrir um arquivo sensível cru.

Ele deveria receber:

LinearAutoDestroy<FileHandle>

E a única forma de acessar o conteúdo deveria passar pelo comportamento semântico do tipo.

O repositório

A proposta deste repositório é facilitar a adoção prática desse padrão.

A ideia é entregar implementações de LinearAutoDestroy em diversas linguagens, com exemplos diretos de uso, para que qualquer pessoa consiga copiar, colar e aplicar imediatamente nos pontos mais críticos do sistema.

O foco não é criar uma abstração bonita.

O foco é eliminar classes reais de falhas causadas por valores que continuam existindo depois que deveriam ter sido consumidos, destruídos ou invalidados.

O repositório contém implementações e exemplos para diferentes estilos de linguagem:

linguagens com ownership forte

linguagens com garbage collector

linguagens funcionais

linguagens orientadas a objeto

linguagens de scripting

runtimes assíncronos

sistemas de fila

wrappers para arquivos

Cada implementação respeita as limitações da linguagem alvo. Algumas conseguem garantir mais em compile-time. Outras dependem de runtime checks. Outras usam wrappers, estados atômicos e handles opacos.

Mas todas seguem a mesma regra semântica:

um valor LinearAutoDestroy não pode continuar existindo como valor válido após seu consumo.

O que vem depois

A primeira implementação prática usa NATS como exemplo de fila.

A próxima etapa é liberar implementações equivalentes para:

Redis

Kafka

RedPanda

BullMQ

Também vou implementar o mesmo conceito como proxy para manuseio de arquivos, permitindo que arquivos temporários, handles sensíveis e buffers críticos sejam tratados como valores de uso único com destruição obrigatória.

A longo prazo, LinearAutoDestroy não deveria ser apenas uma biblioteca.

Ele deveria ser um padrão de modelagem.

Sempre que um valor tiver uma vida útil semanticamente curta, ele não deveria depender da boa vontade do programador para morrer.

Ele deveria nascer com o seu fim definido no próprio tipo.

Conclusão

LinearAutoDestroy é uma tentativa de mover uma responsabilidade crítica do programador para o tipo.

Em vez de escrever código manual para lembrar de destruir valores sensíveis, declaramos que aquele valor pertence a uma classe semântica cujo comportamento obrigatório é a autodestruição linear.

Isso reduz a superfície de ataque, impede reuso indevido, dificulta replay, diminui vazamento por retenção acidental e remove uma fonte enorme de bugs causada por cleanup manual.

O ponto central é este:

comportamento obrigatório não deveria ser convenção;

comportamento obrigatório deveria ser tipo.

Se um valor só pode ser usado uma vez, o sistema de tipos, o runtime e o adapter de infraestrutura deveriam saber disso.

O programador deveria apenas declarar a intenção semântica correta.

O resto deveria acontecer de forma inevitável.