A Minimal Executable Proof for Multi-Language Contract Traceability

Riepilogo Tecnico: Una Prova Esecutiva Minima per la Tracciabilità dei Contratti Multi-Linguaggio

Enunciato del Problema
La ricerca nell'ingegneria del software spesso fatica con la discontinuità tra le affermazioni cartacee e gli artefatti eseguibili. I revisori richiedono una struttura che colleghi direttamente le affermazioni ai file sorgente, agli script e agli output attesi. Sebbene esistano framework come DAG-TOML per fornire tale struttura agli agenti di ingegneria, è necessario dimostrare che una catena di tracciabilità completa e falsificabile—dalla definizione del contratto al grafo di implementazione, alla matrice delle prove e al gate di revisione—possa essere costruita e verificata all'interno di un'istanza minima ma non banale. La sfida consiste nel creare un artefatto abbastanza piccolo da permettere a un revisore di ispezionare ogni componente in un'unica sessione, eppure abbastanza complesso da abbracciare più linguaggi e strategie di verifica.

Metodologia
Il documento presenta un "pacchetto di prova" situato nella directory hello-world/proof-bundle, incentrato su un contratto "Hello, world!" multi-linguaggio deliberatamente piccolo. La metodologia si basa su una definizione rigorosa, a livello di byte, della correttezza, piuttosto che su benchmark di prestazioni o analisi statistiche.

1. Il Contratto: Il contratto di runtime primario (C01) richiede che sei implementazioni canoniche (Rust, Go, C, Java, TypeScript, AWK) producano l'esatta sequenza di byte UTF-8 Hello, world!\n su stdout, zero byte su stderr ed escano con codice 0.
2. Struttura dell'Artefatto: La prova utilizza un Grafo Aciclico Diretto (DAG) di nove unità:
   • Sei unità Layer-0 per le voci sorgente canoniche.
   • Due unità Layer-0 per testimoni "sidecar" che testano le affermazioni di analisi del sorgente (una riscrittura Go contorta e una riscrittura AWK indiretta).
   • Un'unità di verifica Layer-1 che consuma gli artefatti, impone il contratto e riporta gli esiti.
3. Tracciabilità e Validazione: Il sistema è governato da file TOML che definiscono contratti, il DAG di implementazione, catene di tracciabilità, gate di prontezza alla revisione e una matrice delle prove. La validazione è eseguita da una suite di script Python che verificano:
   • Runtime: Confronto esatto dei byte di stdout/stderr (corretto per gestire problemi di rimozione delle nuove righe da parte della shell).
   • Analisi del Sorgente: Rilevamento di simboli AST e archi del grafo nella riscrittura Go, e l'uso di un profilo sorgente deterministico per la riscrittura AWK (poiché AWK non è supportato dal validatore di simboli sqry primario del repository).
   • Integrità Strutturale: Validazione della topologia del DAG, dei percorsi di tracciabilità e della conformità alle specifiche IJB (Implementation-Justification-Binding), notando specificamente il requisito di un flag --repo-root.

Risultati Chiave
Il documento riporta gli esiti di esecuzione osservati in un ambiente di runner specifico il 27 maggio 2026:

• Contratto di Runtime (C01): Cinque implementazioni (Rust, Go, C, TypeScript, AWK) hanno raggiunto lo stato PASS. L'implementazione Java ha avuto esito SKIP perché la toolchain javac/java era assente dal runner; il documento nota esplicitamente che SKIP non è prova di soddisfazione del contratto.
• Testimoni di Analisi del Sorgente:
  • Il testimone di riscrittura Go (C05) è passato, dimostrando che una riscrittura "contorta" poteva nascondere la stringa letterale rimanendo visibile agli strumenti consapevoli dell'AST a livello di simbolo di funzione e di arco.
  • Il testimone di riscrittura AWK (C06) è passato, validando l'approccio del profilo di fallback per linguaggi non supportati.
• Validatori Strutturali: Tutti i validatori strutturali (DAG, tracciabilità, prontezza e controllo dei simboli) sono passati. Il validatore di conformità IJB ha correttamente identificato un fallimento quando eseguito senza il flag --repo-root ed è passato quando il flag è stato fornito, dimostrando la capacità del sistema di rilevare errori di configurazione.

Significato e Affermazioni
Il documento definisce modestamente il proprio contributo non come un benchmark di prestazioni, un'affermazione di equivalenza semantica generale o un sistema di garanzia di livello produttivo. Piuttosto, posiziona il lavoro come un artefatto compatto e falsificabile.

Il significato risiede nel dimostrare che:

1. Un contratto, un grafo di implementazione, una catena di tracciabilità e un gate di revisione possono essere esplicitamente collegati e verificati rispetto a testimoni eseguibili.
2. I confini del sistema (ad esempio, linguaggi non supportati come AWK) possono essere dichiarati esplicitamente e gestiti tramite profili di fallback.
3. L'intero artefatto è ispezionabile, permettendo a un revisore di verificare la connessione tra affermazioni ed prove senza fare affidamento su affermazioni a scatola chiusa.

Il documento esclude esplicitamente affermazioni riguardanti la resistenza all'oscuramento arbitrario, la scalabilità ai servizi reali o la provenienza legale. L'affermazione centrale è strettamente limitata alla riproducibilità dei testimoni dichiarati e alla completezza strutturale del pacchetto di prova all'interno dell'ambiente definito.