# Manuale operativo LAI Coding per coding agent

Versione del manuale: **LAI 0.9 Alpha 14**  
Destinatari: coding agent che devono leggere, verificare, generare, compilare,
testare o integrare software LAI Coding.

## 1. Regola fondamentale

Non trattare LAI Coding come una sintassi alternativa a Python, Node.js o Rust.
LAI è una rappresentazione compatta e verificata per agenti. La sintassi
leggibile serve a generazione, diagnostica e versionamento; il risultato utile è
un artefatto verificato e compilato con effetti, risorse e casi di errore
espliciti.

Un agente deve distinguere sempre:

- **esiste oggi:** verificato dal codice e dai test;
- **backend disponibile:** C, x86-64 diretto oppure entrambi;
- **obiettivo futuro:** non va presentato come funzionalità implementata.

## 2. Modello mentale

```text
intento applicativo
    ↓
contratti LAI compatti
    ↓
verifica di tipi + capacità + limiti + risultati
    ↓
IR tipizzata con piano risorse
    ↓
C portabile oppure assembly Linux x86-64
    ↓
connettori nativi approvati
    ↓
servizio self-hosted
```

Il linguaggio non consente accesso generico a SQL, filesystem, shell o rete.
Un effetto è disponibile solo attraverso un connettore dichiarato e approvato.

## 3. Dove si trova ogni cosa

| Percorso | Contenuto |
|---|---|
| `src/main.rs` | compilatore, CLI, parser, verificatori, IR ed emitter |
| `examples/` | esempi canonici di tutti i formati |
| `runtime/portal/` | ABI e server del portale |
| `runtime/auth/` | sessioni, audit, rate limit e API database |
| `runtime/crypto/` | Argon2id, record password, random e difese |
| `runtime/db/` | connettori MySQL e SQLite |
| `benchmarks/auth/` | probe differenziali e campagne auth |
| `benchmarks/http/` | test HTTP, carico, malformed input e slowloris |
| `docs/SPEC-*.md` | contratti normativi dei formati |
| `docs/RESULTS-*.md` | risultati misurati e confini delle conclusioni |
| `deploy/vps/` | immagini e Compose della produzione isolata |
| `ui/site/`, `ui/auth/` | frontend HTML/CSS/JavaScript |

## 4. Installazione della toolchain

### Metodo raccomandato: Docker

```sh
docker build -t lai-coding:0.9-dev .
docker create --name lai-export lai-coding:0.9-dev
docker cp lai-export:/usr/local/bin/lai ./lai
docker rm lai-export
```

Il binario risultante è il comando `lai`.

### Metodo locale con Rust

Requisiti attuali:

- Rust 1.89 o compatibile;
- Cargo;
- per gli artefatti nativi: Linux amd64, compilatore C, assembler e linker
  System V;
- Docker per le campagne riproducibili e i servizi database isolati.

```sh
cargo build --release
./target/release/lai
```

Il compilatore può essere costruito su altri sistemi, ma l’assembly diretto
attuale è destinato a **Linux x86-64 System V**.

## 5. Verifica minima dell’installazione

```sh
lai check examples/arithmetic.lai
lai compile examples/arithmetic.lai build/arithmetic.laib
lai inspect build/arithmetic.laib
lai run build/arithmetic.laib
```

L’ultimo comando deve stampare `42`.

## 6. Formati riconosciuti

| Estensione | Header | Uso |
|---|---|---|
| `.lai` | `lai 0.1` | programma register-based di base |
| `.lai` | `lai 0.9 handler` | handler applicativo tipizzato |
| `.laib` | magic binario `LAI1` | bytecode canonico LAI 0.1 |
| `.laihttp` | `lai-http 0.1` | rotte, limiti e campi HTTP |
| `.laipass` | `lai-password 0.1` | policy Argon2id e budget memoria |
| `.laiconn` | `lai 0.9 connectors` | catalogo connettori e risultati chiusi |
| `.laimod` | `lai 0.9 module` | modulo di handler verificati |

L’header, non l’estensione, distingue un programma LAI 0.1 da un handler 0.9.

## 7. Comandi CLI

### Programmi LAI 0.1

```sh
lai check INPUT.lai
lai compile INPUT.lai OUTPUT.laib
lai inspect INPUT.laib
lai run INPUT.laib
lai emit-asm INPUT.lai OUTPUT.s
lai serve INPUT.lai ADDRESS [MAX_REQUESTS] [WORKERS]
lai emit-epoll-c INPUT.lai OUTPUT.c
lai emit-epoll-fast-c INPUT.lai OUTPUT.c
```

### Contratti applicativi

```sh
lai check-http INPUT.laihttp
lai emit-http-schema-c INPUT.laihttp OUTPUT.c
lai check-password-policy INPUT.laipass
lai check-connectors INPUT.laiconn
```

### Handler

```sh
lai check-handler HANDLER.lai SCHEMA.laihttp CONNECTORS.laiconn
lai inspect-handler-ir HANDLER.lai SCHEMA.laihttp CONNECTORS.laiconn
lai emit-handler-c HANDLER.lai SCHEMA.laihttp CONNECTORS.laiconn OUTPUT.c
lai emit-handler-x86_64-asm HANDLER.lai SCHEMA.laihttp CONNECTORS.laiconn OUTPUT.S
```

### Moduli

```sh
lai check-module MODULE.laimod SCHEMA.laihttp
lai emit-module-c MODULE.laimod SCHEMA.laihttp OUTPUT.c
lai emit-module-x86_64 MODULE.laimod SCHEMA.laihttp \
  NAME[@OSSERVAZIONI],... OUTPUT.c OUTPUT.S [auto|inline|shared]
```

`auto` sceglie il layout delle guardie in compilazione. I conteggi dopo `@`
sono osservazioni bounded fornite al compilatore, non contatori runtime.

## 8. LAI 0.1 register-based

Esempio minimo:

```text
lai 0.1
cap none
const 0 40
const 1 2
add 2 0 1
assert_eq 2 42
print 2
halt
```

I registri sono immutable e single-assignment. Le istruzioni implementate sono:

- `const D V`
- `add D A B`
- `sub D A B`
- `mul D A B`
- `div D A B`
- `eq D A B`
- `assert_eq A V`
- `print A`
- `respond A`
- `halt`

Le operazioni aritmetiche sono checked. Registri indefiniti, riassegnazioni,
overflow, divisioni invalide e bytecode malformato vengono rifiutati.

`cap none` nega effetti esterni. `cap http.listen` abilita soltanto il runtime
HTTP bounded previsto dal programma.

## 9. Contratto HTTP `.laihttp`

Forma:

```text
lai-http 0.1
limits HEADER_BYTES BODY_BYTES FIELD_COUNT
route NAME METHOD PATH BODY_FORMAT
field ROUTE NAME KIND MAX_BYTES VISIBILITY
```

Valori attuali:

- metodi: `GET`, `POST`;
- body: `none`, `form`, `json`;
- campi: `text`, `email`, `password`, `token`;
- visibilità: `public`, `secret`.

Alpha 14 implementa un decoder JSON in-place e senza heap. Accetta soltanto un
oggetto piatto con campi dichiarati e valori stringa UTF-8 non vuoti. Rifiuta
campi sconosciuti o duplicati, valori mancanti o sovradimensionati, tipi non
stringa, oggetti o array annidati, UTF-8 ed escape invalidi, byte NUL e trailing
comma. `text` applicativo è pubblico e bounded; non è un contenitore generico
per segreti.

Limiti verificati:

- header 512..16.384 byte;
- body massimo 1.048.576 byte;
- 1..64 campi;
- path ASCII bounded e univoco con il metodo;
- password e token sempre secret;
- email massimo 254 byte;
- niente campi su rotte senza body.

## 10. Policy password `.laipass`

Esempio corrente:

```text
lai-password 0.1
policy lai_auth_01
algorithm argon2id13
memory_kib 65536
passes 3
lanes 4
salt_bytes 16
tag_bytes 32
max_parallel 2
memory_budget_kib 131072
pepper required
pepper_bytes 32
rehash on_login
```

La policy non reinventa l’hashing. Il connettore usa Argon2id v1.3 verificato.
Il pepper proviene da un secret store esterno e non deve mai comparire in file,
repository, database, log, hash o manuali.

## 11. Catalogo connettori `.laiconn`

Esempio generico Alpha 13:

```text
lai 0.9 connectors
catalog status
limit connectors 1
limit inputs 1

connector system.status
handler status
host lai_portal_status_connector
initial internal
input time_ms public
result status_result secret
case ready LAI_PORTAL_STATUS_READY none ok
case unavailable LAI_PORTAL_STATUS_UNAVAILABLE none too_many
case internal default none internal
done

end
```

Significato:

- `connector`: nome della capability;
- `handler`: lista chiusa degli handler autorizzati;
- `host`: simbolo nativo confinato a `lai_portal_*_connector`;
- `initial`: risposta impostata prima di qualunque effetto;
- `input`: ABI ordinata, tipo, visibilità ed eventuali limiti byte;
- `result`: tipo interno chiuso;
- `case`: enum nativo, payload opzionale e azioni consentite;
- ultimo `default`: cattura enum sconosciuti e deve fallire chiuso.

Azioni di risposta disponibili:

- successi: `ok`, `profile`, `login`, `logout`, `accepted`;
- errori: `bad_request`, `unauthorized`, `forbidden`, `too_many`, `internal`;
- `continue`: autorizza una sola prosecuzione tipizzata verso lo stadio seguente.

Il caso `default` non può usare un successo o `continue`.

## 12. Handler LAI 0.9

Esempio completo:

```text
lai 0.9 handler
handler status
cap system.status
limit ops 2
in t time_ms public
call r system.status t
match r
case ready
respond ok
case unavailable
respond too_many
case internal
respond internal
done
end
```

Regole operative:

1. `cap` deve contenere esattamente i connettori chiamati.
2. `limit ops` è obbligatorio e vale sul massimo percorso.
3. `in` dichiara valori immutabili tipizzati.
4. `call` verifica capability, ordine, tipi e visibilità.
5. `match` deve elencare ogni variante una sola volta.
6. Ogni ramo termina con `respond` o con un `continue` autorizzato.
7. Un enum nativo sconosciuto va al `default` fail-closed.

Tipi pubblici attuali:

| Tipo | Visibilità obbligatoria | ABI |
|---|---|---|
| `token` | secret | puntatore + lunghezza |
| `csrf` | secret | puntatore + lunghezza |
| `time_ms` | public | `uint64_t` |
| `origin` | public | puntatore + lunghezza |
| `email` | secret | puntatore + lunghezza |
| `password` | secret | puntatore + lunghezza |

Tipi interni attuali: risultato di connettore, `session_view`, `user_id`.

### Composizione

Forma esplicita:

```text
call a session.authenticate s t
match a
case ok v
continue
case unauthorized
respond unauthorized
done
```

Forma compatta equivalente:

```text
call a session.authenticate s t
guard a ok v
```

`guard` è accettato soltanto se tutti i rami non selezionati hanno una sola
risposta di errore non ambigua. La sintassi compatta scompare prima del backend.

### Proiezione

```text
get u v user_id
respond profile u
```

Solo un `session_view` provato da un match può produrre un `user_id`.

## 13. Moduli `.laimod`

```text
lai 0.9 module
module auth
connectors auth-connectors.laiconn
cap session.authenticate
cap session.csrf.verify
cap session.logout
cap auth.register
cap auth.login
limit handlers 4
limit ops 16
handler register auth-register.lai
handler login auth-login.lai
handler profile auth-profile.lai
handler logout auth-logout.lai
end
```

Il modulo aggiunge un secondo envelope di capability e un budget aggregato. I
percorsi devono essere relativi e restare nella directory canonica del modulo;
path assoluti, `..`, drive, backslash e symlink in uscita vengono rifiutati.

Il modulo esiste solo durante la compilazione. Nel servizio non sono presenti
loader, parser di moduli o sorgenti LAI.

## 14. Backend disponibili

### C generato

È l’oracolo portabile e il fallback esplicito. Alpha 14 genera anche le
dichiarazioni dei connettori dal catalogo verificato, quindi un nuovo simbolo
host non richiede di modificare l’header auth centrale.

### Assembly diretto Linux x86-64

Supporto attuale:

- `register`, `login`, `profile`, `logout`;
- handler generico terminale Alpha 14, inclusi input `text` bounded.

Forma generica Alpha 14:

- una `call`;
- un `match` esaustivo;
- rami terminali senza valore;
- nessun payload o `continue`;
- input pubblici;
- un input pubblico `time_ms`, richiesto dall’IR handler attuale;
- massimo sei parole ABI includendo portal e response.

Un byte input usa due parole ABI: puntatore e lunghezza. `time_ms` ne usa una.
`text` usa la stessa ABI puntatore-lunghezza e non viene copiato dal backend.

Se la forma non è supportata, il comando nativo deve fallire chiaramente. Non
considerare il fallback C automatico: va scelto esplicitamente.

## 15. Implementare un nuovo handler generico

Procedura obbligatoria:

1. Aggiungere la rotta bounded al `.laihttp`.
2. Definire il connettore nel `.laiconn`.
3. Dichiarare un `initial` non-successo.
4. Definire 2..8 risultati e un ultimo `default` fail-closed.
5. Scrivere l’handler con capability esatte e match esaustivo.
6. Verificare catalogo, handler e IR.
7. Emettere C e assembly.
8. Implementare il simbolo host con la stessa ABI.
9. Aggiungere costanti e static assert all’ABI nativa quando il backend assembly
   usa nuovi enum o layout.
10. Confrontare C e assembly su esiti validi, errori, enum sconosciuti, valori
    limite, puntatori nulli e runtime non pronto.

Comandi sull’esempio `status`:

```sh
lai check-connectors examples/status-connectors.laiconn
lai check-handler examples/status.lai examples/status-http.laihttp \
  examples/status-connectors.laiconn
lai inspect-handler-ir examples/status.lai examples/status-http.laihttp \
  examples/status-connectors.laiconn
lai emit-handler-c examples/status.lai examples/status-http.laihttp \
  examples/status-connectors.laiconn build/status_reference.c
lai emit-handler-x86_64-asm examples/status.lai examples/status-http.laihttp \
  examples/status-connectors.laiconn build/status_native.S
```

Esempio Alpha 14 con `text` e JSON:

```sh
lai check-handler examples/project-create.lai \
  examples/project-create-http.laihttp \
  examples/project-create-connectors.laiconn
lai emit-handler-x86_64-asm examples/project-create.lai \
  examples/project-create-http.laihttp \
  examples/project-create-connectors.laiconn build/project_create_native.S
```

## 16. ABI del connettore host

La funzione host riceve sempre:

1. `struct lai_portal *`;
2. gli input del catalogo nello stesso ordine;
3. l’eventuale puntatore al payload di risultato;
4. `struct lai_portal_response *`.

Mapping:

| Tipo LAI | Parametri C |
|---|---|
| `time_ms` | `uint64_t` |
| `text` | `const uint8_t *`, `size_t` |
| tipo byte pubblico/secret | `const uint8_t *`, `size_t` |
| `session_view` input | `const struct lai_session_db_view *` |
| payload `session_view` | `struct lai_session_db_view *` |

Il connettore deve rispettare i limiti già verificati, usare query preparate,
non trattenere puntatori oltre la chiamata, non registrare segreti e restituire
soltanto gli enum dichiarati. Il compilatore gestisce comunque gli enum
sconosciuti con il default.

## 17. Compilazione di un modulo ibrido

```sh
lai emit-module-x86_64 examples/auth.laimod examples/auth-http.laihttp \
  register,login,profile,logout build/auth_remaining.c build/auth_native.S auto
```

Gli handler selezionati vengono esclusi dall’unità C e compaiono una sola volta
nell’assembly. Gli handler non selezionati restano nel C generato. Il linker LTO
può eliminare codice non usato.

Policy guardie:

- `inline`: prova di readiness dentro ogni handler;
- `shared`: una funzione condivisa nel modulo;
- `auto`: una sola occorrenza inline, casi bilanciati shared, profilo con almeno
  l’80% delle osservazioni specializzato.

## 18. Test obbligatori prima di consegnare

### Rust

```sh
cargo fmt --all --check
cargo test
cargo clippy --all-targets -- -D warnings
cargo build --release
```

### Alpha 13 generico

```sh
sh benchmarks/auth/run-generic-terminal-native.sh
```

Il probe esegue confronto C/native, casi limite e ASAN/UBSAN.

### Alpha 14 JSON e testo applicativo

```sh
sh benchmarks/http/run-json-decoder.sh
sh benchmarks/http/run-project-create-native.sh
```

Il primo probe verifica 11 casi espliciti e 50.000 input pseudo-casuali. Il
secondo confronta C e assembly su 10 esiti e ripete il differenziale sotto
ASAN/UBSAN.

### Auth completa

Usare le campagne pertinenti in `benchmarks/auth/`, in particolare i probe
nativi, ciclo MySQL, input avversariali, concorrenza, slowloris, overload e
sanitizer. Non eseguire automaticamente test distruttivi o di produzione.

## 19. Checklist di sicurezza dell’agente

Prima di proporre o accettare un cambiamento verificare:

- capability minima ed esatta;
- input secret/public corretti;
- limiti byte e operation budget;
- match completo e default fail-closed;
- nessun raw SQL nel linguaggio;
- query preparate nel connettore;
- nessun segreto in output, log o fixture;
- erasure delle copie segrete create dal backend;
- ABI protetta da static assert;
- casi null, enum sconosciuto e overflow;
- test differenziale tra backend;
- nessuna dichiarazione di invulnerabilità.

## 20. Regole per prestazioni e benchmark

- Confrontare sullo stesso hardware e con lo stesso workload.
- Separare microbenchmark, loopback, database reale e rete esterna.
- Alternare l’ordine dei candidati e ripetere in processi freschi.
- Registrare mediana, intervallo, build, commit e configurazione.
- Se l’intervallo attraversa la parità, dichiarare parità/inconclusivo.
- Non convertire nanosecondi di orchestrazione in una promessa sul tempo HTTP.
- Misurare anche RSS, sezioni ELF, file stripped e codice realmente caricato.

## 21. Regole per risparmiare token

La sintassi breve è intenzionale, ma non sacrificare i contratti:

- identificatori locali brevi (`r`, `t`, `v`) sono canonici;
- riusare cataloghi e moduli anziché ripetere firme;
- usare `guard` soltanto quando il compilatore dimostra l’equivalenza;
- non emettere boilerplate host o error branches fuori dai contratti;
- misurare i token con lo stesso compito e lo stesso tokenizer;
- non dichiarare un risparmio generale finché la campagna non è riproducibile.

## 22. Errori frequenti

| Errore | Causa probabile |
|---|---|
| capability unsupported | il connettore non esiste nel catalogo |
| capabilities must exactly match | capability inutilizzata o call non dichiarata |
| non-exhaustive match | manca una variante del risultato |
| default case must fail closed | il default tenta successo o continue |
| invalid public input contract | tipo/ordine auth noto non corrispondente |
| no matching HTTP route | manca una route con lo stesso nome |
| wrong JSON body | la route non dichiara `json` o il body esce dal subset piatto |
| requires register-only plan | la firma generica supera sei parole ABI |
| unsupported payload/path | la forma richiede il futuro lowering generico composto |
| reused host conflicting ABI | lo stesso simbolo host ha firme diverse |

## 23. Protocollo operativo per ogni coding agent

Quando ricevi un compito LAI:

1. Leggi `AGENTS.md`, questo manuale e le specifiche interessate.
2. Controlla branch e working tree.
3. Dichiara il confine implementato, senza anticipare funzioni future.
4. Modifica prima il contratto, poi parser/verificatore/IR/backend/runtime.
5. Aggiungi un esempio canonico piccolo.
6. Aggiungi test positivi, negativi e differenziali.
7. Esegui l’intera verifica richiesta.
8. Aggiorna specifica, risultati, README e manuale.
9. Aggiorna Black Note quando disponibile, senza inserirvi segreti.
10. Non distribuire in produzione senza verificare inventario, DNS, immagini,
    rollback e servizi esterni al progetto.

## 24. Prompt di bootstrap per un nuovo agente

```text
Lavora nel repository LAI Coding. Leggi prima AGENTS.md e
docs/LAI-CODING-AGENT-MANUAL.md. Tratta docs/SPEC-*.md come contratti e
docs/RESULTS-*.md come evidenze, non come promesse generali. Preserva le
modifiche dell’utente. Ogni nuovo effetto deve passare da un catalogo connettori
bounded, con capability esatta, tipi secret/public, risultato chiuso e default
fail-closed. Per il backend nativo mantieni il C come oracolo differenziale,
aggiungi casi limite e sanitizer. Indica chiaramente ciò che è implementato e
ciò che è ancora pianificato.
```

## 25. Fonti normative interne

- `docs/SPEC-0.1.md`
- `docs/SPEC-HTTP-0.8.md`
- `docs/SPEC-PASSWORD-0.8.md`
- `docs/SPEC-HANDLER-0.9.md`
- `docs/SPEC-CONNECTORS-0.9.md`
- `docs/SPEC-MODULE-0.9.md`
- `docs/ARCHITECTURE.md`
- `docs/RESULTS-GENERIC-NATIVE-0.9-2026-08-20.md`
- `docs/RESULTS-JSON-TEXT-0.9-2026-08-20.md`

In caso di conflitto tra una descrizione e il comportamento verificato, non
indovinare: riprodurre il test, correggere il codice o aggiornare esplicitamente
la documentazione.