Ghost to Pure promotion doesn't seem to work with conditionals

Metriche repository

Star

3068 star (3068 star)

Metriche merge PR

Metriche PR in attesa (Metriche PR in attesa)

Descrizione

module Test

assume val f : int -> GTot bool

let works (unit) : Tot int = 
  let _ = 
     let y = f 0 in 
     assert (y ==> 0=0);
     assert (not y ==> 1=1) in
  0

let fails (unit) : Tot int = 
  let _ = 
     let y = f 0 in 
     if y
     then assert (0=0)
     else assert (1=1) in
  0

Guida contributor

Direzione di ricerca

Indagare sulla promozione da Ghost a Pure nel type checker di F* quando vengono utilizzate espressioni condizionali (if then else). Il test fallito mostra che l'assert diretto funziona ma if else fallisce, suggerendo che la logica di promozione degli effetti potrebbe non gestire correttamente i condizionali. Esaminare il type checking delle espressioni 'if' nel codice sorgente di F*, concentrandosi su come vengono calcolati e promossi gli effetti.

Tech stack

Nessuno

Dominio

compilers

Tipo issue

Bug

DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.

3

Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.

Mezza giornata

Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.

Attiva

ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.

Chiara

Prerequisiti

F* programmingproof assistant concepts

Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.

30