Refactor packet parsing to use seq[byte] views instead of slice permissions#423

Draft

jcp19 wants to merge 36 commits into

claude/byte-slice-parsing-refactor-rpfg0c

Commits on Jul 5, 2026

Commits on Jul 6, 2026

Hide the elementwise characterization of View behind a lemma
claude
committed
Prove slice-lemma view relations by recursion instead of elementwise quantifiers
claude
committed
Return the quantified wildcard permissions from the ViewAux lemmas
claude
committed
Bind the slice-overlap facts in ViewAuxReslice's postcondition
claude
committed
Make ViewAux opaque and unroll it with reveal in the recursion lemmas
claude
committed
Fix permission accounting and value framing in the slices lemmas
claude
committed
Keep ViewAux transparent and make ViewElems preserve views and bytes
claude
committed
Merge branch 'master' into claude/byte-slice-parsing-refactor-rpfg0c
jcp19
authored
Carry value preservation through the ViewAux lemmas' contracts
claude
committed
Keep ViewAux well-defined at the fold boundaries and pin views in slayers
claude
committed
Slice the view postcondition of CombineRange_Bytes into separate clauses
claude
committed
Split ViewAuxSplit's preservation facts across two lemmas
claude
committed
Pin predicate snapshots across ViewElems calls by retaining a fraction
claude
committed

Commits on Jul 8, 2026

Commits on Jul 10, 2026

Raise the path/scion verification timeout to 45m as a diagnostic
claude
committed

Commits on Jul 12, 2026

Trigger CI on the raised path/scion timeout
claude
committed