Ruling needed: what satisfies "must hold for generic type T (no monomorphization)" #734

Activity

1. feliperodri commented on Oct 21, 2026

   

   feliperodri

   on Oct 21, 2026

   MemberAuthor

   More actions

   any thoughts? @btj @patricklam @tautschnig @rajath-mk @HuStmpHrrr @celinval @remi-delmas-3000 @rahulku @rafaelsamenezes @lucasccordeiro @dkcumming @DiuDiu777
2. feliperodri

   added

   QuestionUse for any clarification or general question about the contestUse for any clarification or general question about the contest

   on Oct 21, 2026
3. feliperodri

   added the

   Task

   issue type on Oct 21, 2026
4. DiuDiu777 commented on Oct 22, 2026

   

   DiuDiu777

   on Oct 22, 2026

   More actions

   Hi, @feliperodri.

   I’d recommend A “representative types plus a clear argument for why the results generalize.“ Covering every size_of / align_of branch is a useful baseline, but we still need to explain why other types can’t introduce new safety issues. Capacity arithmetic, pointer offsets, and trait behavior can vary even within the same branch.

   For code that mainly depends on type layout, one approach is to make size and alignment symbolic. RawVec already puts much of its logic in RawVecInner, which takes a Layout parameter. A harness could start with:

   let size: usize = kani::any();
   let align: usize = kani::any();
   
   let Ok(layout) = Layout::from_size_align(size, align) else {
       return;
   };
   kani::assume(size % align == 0);
   
   // Pass layout and a symbolic capacity to the actual
   // implementation, then check the target properties.

   This would need two pieces: Kani checks the internal implementation for all allowed layouts and states, and a separate argument shows that the generic wrapper passes the right layout and preserves the required invariants for any T. Drop, Clone, and value validity would still need their own contracts and reasoning in other ways (maybe with explicit assumptions)
5. patricklam commented on Oct 22, 2026

   

   patricklam

   on Oct 22, 2026

   More actions

   This is kind of a placeholder comment, but I am actually interested into looking into this in more depth and figuring out what would be needed to have Kani support this. (In particular I am looking for projects for graduate students). I see that @DiuDiu777 touched on what is needed in the above comment.
6. feliperodri commented on Oct 22, 2026

   

   feliperodri

   on Oct 22, 2026

   MemberAuthor

   More actions

   @patricklam I tried a small experiment for a 3rd route: prove the property once for every T with Charon → Aeneas → Lean, and check the same property on concrete types with Kani (see this https://github.com/feliperodri/kani/blob/charon-type-invariant/experiments/charon-type-invariant/WALKTHROUGH.md).

   The example is a generic Slots<T> (two Option<T> slots and a len: u8) with new, push and pop, and the type invariant "len counts the occupied slots, and b is used only if a is".

   • Charon translates it without monomorphizing, and Aeneas turns it into a Lean model that is generic in T. In Lean, new establishes the invariant and push/pop preserve it and never overflow len, for every T. The proofs use only Lean's standard axioms.
   • Kani checks the same invariant for u8, u64, char, (u16, bool), [i32; 3], Option<u32> and String; all pass.
   • Breaking push (incrementing len when both slots are full) fails both the Lean proof and the Kani harnesses.

   Compared with Verus and VeriFast: all three verify a generic function once rather than per instance. They differ in where the spec lives and what code they reach.

   • VeriFast: separation-logic annotations in comments in the Rust source, checked by symbolic execution one function at a time. It targets unsafe code, and for non-unsafe functions it generates the spec from the types (RustBelt's semantic well-typedness), which is why it fits RawVec and LinkedList. (@btj can correct me if I got this wrong)
   • Verus: specs and proof code in Rust syntax next to the code, discharged by Z3. It covers a subset of Rust; raw pointers are partially supported through vstd::raw_ptr, where each access needs a ghost PointsTo permission. Others stdlib functions are trusted through assume_specification. (@elanortang can correct me here if I got this wrong)
   • Charon → Aeneas → Lean: the Rust code carries no annotations, and the spec and proof sit in a separate Lean file, proved with tactics. Safe Rust only. What the other two don't have is the Kani half, which checks the same invariant on the code rustc compiles for concrete types.

   The experiment shows only that the two halves can share one invariant and that both reject the same mutant. Each covers a gap in the other. Kani runs the compiled code for a concrete T, checks for undefined behaviour and layout-dependent bugs, and returns a concrete counterexample without anyone writing a proof. The Lean proof covers every T, which no list of instances does (the 2 KiB case in the issue description). I haven't tried it, but the two could feed each other in an agent loop: propose an invariant, let Kani find a counterexample on some instance, refine, and attempt the Lean proof once the instances pass; or use an unsolved Lean goal to choose the next instance to check. I don't know whether that converges faster than either tool alone, and I'd like to hear from anyone who has tried something similar with Verus or VeriFast. @patricklam perhps this could be the direction for a graduate student to explore.

   What it doesn't settle for this issue: Aeneas works on safe Rust, and the challenges here are mostly unsafe code over raw pointers (RawVec, Vec, VecDeque, LinkedList), so this route doesn't reach them as written. For VecDeque, the index arithmetic would fit, but it doesn't depend on T; the parts that do are the unsafe ones. With trait bounds, a proof for every T is also only as good as the trait specs each concrete impl has to meet... So for these challenges I still think something like @DiuDiu777's split is the practical answer (check the layout-dependent core for all layouts, and argue separately about the wrapper), and this route is for safe generic code.
7. Tiramisu-Cake

   added a commit that references this issue on Oct 24, 2026

   docs(ch8): fix working requirements interpretation from organizer sta…

   ...

   8924fdf