src/ez/sorted.bend checks

raw source on the hub · import 0x886223f5c47e4983fe57d887c034bc7f/src/ez/sorted.bend as Sorted

ez/sorted: strings in order, sorted by a walk the termination check can read.

Base's List.sort takes its comparison as an erased (~) argument and is a fuelled bottom-up merge sort besides. Bend cannot show either terminates, so every def whose closure reaches it falls outside the proof guarantees and is counted unsafe. An insertion shrinks its list at every step and costs nothing, and the lists here are a handful of hashes.

1 import

import Base

Definitions

def sort.ins.put source · line 13 · raw

@le:Bool -> @+item:String -> @head:String -> @tail:List<&2, String> -> @rest:List<&2, String> -> List<&2, String>

where one string belongs in a list already sorted, once the rest of that list has been placed. The recursion is done before the choice, because a def may not call itself inside a branch.

def sort.ins source · line 27 · raw

@+item:String -> @ss:List<&2, String> -> List<&2, String>

one string dropped into a sorted list

def sort source · line 37 · raw

@ss:List<&2, String> -> List<&2, String>

the strings in order. Base's List.sort takes its comparison as an erased argument and is fuelled besides, so nothing downstream of it can be proved; an insertion shrinks its list every step and stays inside the check.