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

仓库指标

Star

3,068 star (3,068 star)

PR 合并指标

PR 指标待抓取 (PR 指标待抓取)

描述

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

贡献者指南

研究方向

调查F*类型检查器中条件表达式（if then else）的Ghost到Pure提升问题。失败的测试表明直接断言有效但if else失败，这表明效果提升逻辑可能无法正确处理条件表达式。查看F*源代码中'if'表达式的类型检查，重点关注效果的计算和提升方式。

技术栈

无

领域

compilers

议题类型

缺陷

难度面向新贡献者的预计实现难度，1 表示很小改动，5 表示专家级工作。

3

预计时间有经验贡献者完成调查、实现、测试并准备 pull request 的粗略时间范围。

半天

活动状态议题当前的可参与程度：新鲜、活跃、陈旧、阻塞或等待维护者输入。

活跃

清晰度议题是否清楚说明期望改动、验收标准和下一步。

清晰

前置要求

F* programmingproof assistant concepts

新手友好度1-100 的估计分数，表示该议题对首次贡献者的友好程度。

30