Partial spec lemmas simplified by simp + some library application#4
Partial spec lemmas simplified by simp + some library application#4abentkamp wants to merge 14 commits into
simp + some library application#4Conversation
clementblaudeau
left a comment
clementblaudeau
left a comment
There was a problem hiding this comment.
A couple of style questions that have several occurences: should we replace
(fun e => e = .arrayOutOfBounds ∧ i.val ≥ v.length)with
(fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)?
| theorem Array.index_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) : | ||
| spec_partial (v.index_usize i) | ||
| (fun x => ∃ _ : i.val < v.length, x = v.val[i.val]) | ||
| (fun e => e = .arrayOutOfBounds ∧ i.val ≥ v.length) |
There was a problem hiding this comment.
| (fun e => e = .arrayOutOfBounds ∧ i.val ≥ v.length) | |
| (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False) |
There was a problem hiding this comment.
How about direct matching there ?
There was a problem hiding this comment.
There are three other occurences
There was a problem hiding this comment.
The e = .arrayOutOfBounds ∧ -form is what Son already agreed to, so that's why I'd like to leave it that way.
See: #Cryspen > mvcgen specs
The match-syntax looks nicer, but is also slightly harder to deal with when generating the spec-lemmas. Still, if Son agrees, I'd be happy to switch to matching.
| (fun s => | ||
| s.val = a.val.slice r.start.val r.end.val ∧ | ||
| (∀ i, i + r.start.val < r.end.val → s.val[i]! = a.val[r.start.val + i]!)) | ||
| (fun e => e = .panic ∧ ¬ (r.start.val < r.end.val ∧ r.end.val ≤ a.val.length)) |
There was a problem hiding this comment.
Should it be panic or Array out of bounds here ? And same style question as above
There was a problem hiding this comment.
Further up in that file, subslice is defined to throw .panic, so unless we change that definition, we'll have to use .panic here as well. Is there a clear distinction in Rust between out-of-bounds and other panics? How do we make these distinctions?
| (∀ i, i < r.start.val → na[i]! = a[i]!) ∧ | ||
| (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = s[i - r.start.val]!) ∧ | ||
| (∀ i, r.end.val ≤ i → i < n.val → na[i]! = a[i]!)) | ||
| (fun e => e = .panic ∧ |
| (fun (s : Slice T) => | ||
| s.val = a.val.slice r.start r.end ∧ | ||
| s.length = r.end.val - r.start.val) | ||
| (fun e => e = .panic ∧ ¬ (r.start ≤ r.end ∧ r.end ≤ N)) |
| z.val = x.val + y.val ∧ | ||
| z.bv = x.bv + y.bv | ||
| | fail _ => ¬ (UScalar.inBounds ty (x.val + y.val)) | ||
| | fail e => e = .integerOverflow ∧ ¬ (UScalar.inBounds ty (x.val + y.val)) |
There was a problem hiding this comment.
| | fail e => e = .integerOverflow ∧ ¬ (UScalar.inBounds ty (x.val + y.val)) | |
| | fail .integerOverflow => ¬ (UScalar.inBounds ty (x.val + y.val)) |
| z.val = x.val + y.val ∧ | ||
| z.bv = x.bv + y.bv | ||
| | fail _ => ¬ (IScalar.inBounds ty (x.val + y.val)) | ||
| | fail e => e = .integerOverflow ∧ ¬ (IScalar.inBounds ty (x.val + y.val)) |
| (∃ y, m = ok y ∧ P y) → spec m P := by | ||
| exact (spec_equiv_exists m P).2 | ||
|
|
||
| /-- Partial-correctness variant of `spec`. |
There was a problem hiding this comment.
Should the base branch be spec_partial instead of dev ?
There was a problem hiding this comment.
Oh no! The spec_partial-PR has already been merged, but it had the wrong target branch when I merged it. So it's all a mess now. Maybe we can just merge everything with this PR?
3 participants
This PR changes the mechanism for simplifying hypotheses in the lemmas generated by partial @[step] lemmas. It uses Lean's
simpnow.Moreover, this PR puts the new
spec_partialpredicate to use: It converts the oldspeclemmas intospec_partiallemmas for arithmetic and array/slice operations.Claude generated most of this PR, but it has been carefully reviewed and hand-edited.