Safety, Relative Tightness and the Probabilistic Frame Rule

Titolo: Sicurezza, Strettezza Relativa e la Regola del Frame Probabilistica

1. Il Problema

La logica di separazione (Separation Logic) è un formalismo di successo per la verifica di programmi imperativi che manipolano la memoria, grazie alla sua regola del frame, che permette un ragionamento modulare. La Logica di Separazione Probabilistica (Probabilistic Separation Logic - PSL) ha adattato questo approccio ai programmi con casualità, utilizzando la congiunzione separante ($*$) per esprimere proprietà di indipendenza probabilistica.

Tuttavia, le formulazioni precedenti della PSL (in particolare quelle di [3, 2]) presentano limitazioni significative:

• Complessità della Regola del Frame: La regola del frame originale richiede tre condizioni laterali (side conditions) complesse per garantire la correttezza. Queste condizioni vincolano le variabili libere degli asserzioni e richiedono che il programma non modifichi certe variabili o che le variabili siano definite in modo specifico.
• Restrizioni sul Linguaggio: I framework esistenti impongono restrizioni artificiali, come la distinzione sintattica tra variabili deterministiche e probabilistiche, la necessità che i guardie dei cicli siano deterministiche e il limite al numero di iterazioni dei cicli (loop).
• Natura Intuizionistica: Le logiche probabilistiche esistenti sono spesso intrinsecamente intuizionistiche, il che può complicare il ragionamento classico.

L'obiettivo del paper è investigare se è possibile eliminare queste complicazioni e restrizioni, proponendo un framework che supporti un linguaggio imperativo probabilistico completo (senza restrizioni sui loop o sulla natura delle variabili) e che permetta una formulazione della regola del frame semplice ed elegante, priva di condizioni laterali aggiuntive.

2. Metodologia

Gli autori adottano un approccio semantico piuttosto che sintattico, costruendo la logica su concetti matematici rigorosi:

• Stato Random come Variabile Aleatoria: Invece di definire lo stato random come una distribuzione di probabilità sugli stati (approccio standard), gli autori lo definiscono come una variabile aleatoria a valori di stato ($\Sigma: \Omega \to State$), dove $\Omega$ è uno spazio campionario discreto. Questo permette un formalismo più intuitivo per l'operatore di congiunzione separante.
• Relazione di Soddisfacimento Parziale: Viene introdotta una relazione di soddisfazione $\Sigma \models \Phi$ che può essere non definita (undefined) se lo stato random $\Sigma$ non fornisce informazioni sufficienti per determinare la verità o falsità di $\Phi$. Questo gestisce naturalmente la parzialità degli stati (es. variabili non definite).
• Sicurezza (Safety) e Strettezza Relativa (Relative Tightness):
  • Sicurezza: Le specifiche Hoare $\{ \Phi \} C \{ \Psi \}$ includono una garanzia intrinseca di sicurezza: se lo stato soddisfa la precondizione, l'esecuzione non genera errori di memoria (fault).
  • Strettezza Relativa: Derivata dalla sicurezza, questa proprietà afferma che la parte dello stato finale rilevante per la postcondizione $\Psi$ dipende solo dalla parte dello stato iniziale rilevante per la precondizione $\Phi$. Formalmente, ciò si traduce in una proprietà di indipendenza condizionale: lo stato finale (limitato alle variabili di $\Psi$) è condizionalmente indipendente dallo stato di ingresso completo, dato lo stato di ingresso limitato alle variabili di $\Phi$.
• Linguaggio Pwhile: Viene utilizzato il linguaggio imperativo probabilistico completo pwhile, che supporta assegnazioni deterministiche, campionamenti da distribuzioni, cicli while illimitati e strutture di controllo condizionali, senza restrizioni sintattiche sulle variabili.

3. Contributi Chiave

1. Formulazione Semantica della Logica:

   • Definizione di asserzioni semantiche come funzioni parziali dagli stati random ai valori di verità $\{tt, ff\}$.
   • Integrazione della logica classica (evitando l'intuizionismo) grazie alla gestione esplicita degli stati "non definiti".
   • Definizione della congiunzione separante $\Phi * \Psi$ basata sull'indipendenza delle proiezioni degli stati random sulle variabili coinvolte, permettendo la condivisione di variabili deterministiche senza bisogno di classi sintattiche separate.

2. La Regola del Frame Semplificata:

   • Gli autori dimostrano che, grazie alla proprietà di sicurezza e strettezza relativa, la regola del frame può essere formulata esattamente come nella logica di separazione classica per la memoria, senza condizioni laterali complesse:
     $$\frac{\{ \Phi \} C \{ \Psi \} \quad FV(\Theta) \cap MV(C) = \emptyset}{\{ \Phi * \Theta \} C \{ \Psi * \Theta \}}$$
     Dove $MV(C)$ è l'insieme delle variabili modificate dal programma. L'unica condizione richiesta è che le variabili nel "frame" ($\Theta$) non siano modificate dal programma.

3. Dimostrazione di Correttezza (Soundness):

   • Teorema 6.3 (Strettezza Relativa): Viene provato che per ogni specifica parzialmente corretta, lo stato finale è condizionalmente indipendente dallo stato iniziale rispetto alla proiezione sulla precondizione.
   • Corollario 6.4: La correttezza della regola del frame segue direttamente dalla strettezza relativa e dalle proprietà generali dell'indipendenza condizionale.

4. Analisi delle Restrizioni:

   • Viene dimostrato tramite controesempi che se la garanzia di sicurezza viene rimossa, la strettezza relativa e la correttezza della regola del frame falliscono. Questo sottolinea l'importanza cruciale della gestione degli errori (faults) nel framework.

4. Risultati

• Generalità: Il framework supporta il linguaggio pwhile completo, inclusi cicli while non limitati e variabili che possono essere sia deterministiche che probabilistiche senza distinzione sintattica.
• Semplicità: La regola del frame è stata ridotta alla sua forma più semplice e intuitiva, eliminando le tre condizioni laterali presenti nella letteratura precedente.
• Equivalenza: Sebbene l'approccio basato su variabili aleatorie sia diverso da quello basato su distribuzioni, i due sono dimostrati equivalenti.
• Validazione: Gli autori hanno verificato che gli esempi di verifica di protocolli crittografici presenti nella letteratura precedente possono essere trasferiti nel loro framework semantico, mantenendo le restrizioni originali, ma con la prospettiva di rimuoverle in futuro.

5. Significato e Prospettive Future

Questo lavoro rappresenta un passo fondamentale verso una Logica di Separazione Probabilistica più robusta e applicabile.

• Impatto Teorico: Dimostra che la complessità delle regole laterali nelle versioni precedenti non era necessaria, ma era un artefatto di scelte di progettazione specifiche (come la distinzione sintattica delle variabili). La sicurezza e la strettezza relativa sono le proprietà fondamentali che abilitano il ragionamento modulare.
• Impatto Pratico: Rimuovere le restrizioni sui loop e sulle variabili rende la logica potenzialmente applicabile a una gamma molto più ampia di programmi reali, inclusi quelli con cicli probabilistici complessi.
• Lavori Futuri: Gli autori intendono sviluppare un sistema di prova completo per il linguaggio pwhile illimitato. Propongono già regole provvisorie per i cicli while (basate sulla chiusura topologica degli invarianti) e l'integrazione di modalità di condizionamento ($C_E \Phi$) con le strutture condizionali del linguaggio. Un'altra direzione di ricerca è l'estensione della logica per includere l'implicazione separante ("magic wand").

In sintesi, il paper offre una fondazione semantica solida che semplifica drasticamente il ragionamento sulla correttezza dei programmi probabilistici, rendendo la regola del frame uno strumento potente e privo di vincoli artificiali.