1 # Erased affine owner evidence for the same grouped traversal. Unlike the 2 # value model, this certificate proof never reflects an owner into live Data. 3 import Base 4 import ../traversal_grouped.bend as Grouped 5 import ../traversal_loop.bend as Loop 6 import ./traversal_witness.bend as Witness 7 8 type StateEvidence<-Reader: Type,-Context: Data,-reader: Reader,-state: Grouped.State> is Data: 9 StateEvidence{-total: F32,position: Nat,context: Context, 10 equation: {state == Grouped.State{reader,context,position,total} : Grouped.State}} 11 12 def advanced(~Reader: Type,~Context: Data,-reader: Reader,+context: Context,+position: Nat,-total: F32,-result: Reader & F32, 13 evidence: Witness.Sample) -> 14 StateEvidence: 15 Witness.Sample{value,equation} = evidence 16 %Equal.sym(Reader & F32,result,(reader,value),equation) : StateEvidence 17 StateEvidence{(total + value : F32),1n+position,context,{==}} 18 19 def step(~Reader: Type,~Context: Data,~Evidence: @-reader: Reader -> Data,~read: Reader -> Context -> Nat -> Reader & F32, 20 ~preserves: @-reader: Reader -> @context: Context -> @position: Nat -> Evidence(reader) -> Witness.Sample, 21 -reader: Reader,-state: Grouped.State,source: Evidence(reader),evidence: StateEvidence) -> 22 StateEvidence: 23 StateEvidence{total,+position,+context,equation} = evidence 24 %Equal.sym(Grouped.State,state,Grouped.State{reader,context,position,total},equation) : StateEvidence 25 advanced(~Reader,~Context,reader,context,position,total,read(reader,context,position),preserves(reader,context,position,source)) 26 27 def loop(~Reader: Type,~Context: Data,~Evidence: @-reader: Reader -> Data,~read: Reader -> Context -> Nat -> Reader & F32, 28 ~preserves: @-reader: Reader -> @context: Context -> @position: Nat -> Evidence(reader) -> Witness.Sample, 29 count: Nat,-reader: Reader,-state: Grouped.State,+source: Evidence(reader),evidence: StateEvidence) -> 30 StateEvidence,~Grouped.step(~Reader,~Context,~read),count,state)>: 31 match count: 32 case 0n: evidence 33 case 1n+rest: 34 loop(~Reader,~Context,~Evidence,~read,~preserves,rest,reader,Grouped.step(~Reader,~Context,~read,state),source, 35 step(~Reader,~Context,~Evidence,~read,~preserves,reader,state,source,evidence)) 36 37 def finished(~Reader: Type,~Context: Data,-reader: Reader,-state: Grouped.State,evidence: StateEvidence) -> 38 Witness.Sample: 39 StateEvidence{total,position,context,equation} = evidence 40 %Equal.sym(Grouped.State,state,Grouped.State{reader,context,position,total},equation) : Witness.Sample 41 Witness.Sample{total,{==}} 42 43 def fold(~Reader: Type,~Context: Data,~Evidence: @-reader: Reader -> Data,~read: Reader -> Context -> Nat -> Reader & F32, 44 ~preserves: @-reader: Reader -> @context: Context -> @position: Nat -> Evidence(reader) -> Witness.Sample, 45 count: Nat,position: Nat,-reader: Reader,context: Context,source: Evidence(reader)) -> 46 Witness.Sample: 47 finished(~Reader,~Context,reader,Loop.run(~Grouped.State,~Grouped.step(~Reader,~Context,~read),count,Grouped.State{reader,context,position,0.0}), 48 loop(~Reader,~Context,~Evidence,~read,~preserves,count,reader,Grouped.State{reader,context,position,0.0},source,StateEvidence{0.0,position,context,{==}})) 49 50 def prepended(~Reader: Type,-reader: Reader,-head: F32,-result: Reader & List<&2,F32>,evidence: Witness.Sample,reader,result>) -> 51 Witness.Sample,reader,Grouped.prepend(~Reader,head,result)>: 52 Witness.Sample{tail,equation} = evidence 53 %Equal.sym(Reader & List<&2,F32>,result,(reader,tail),equation) : Witness.Sample,reader,Grouped.prepend(~Reader,head,_)> 54 Witness.Sample{head <> tail,{==}} 55 56 def group_tail(~Reader: Type,~Context: Data,~read: Reader -> Context -> Nat -> Reader & F32, 57 -reader: Reader,+context: Context,+rest: List<&2,Grouped.Range>,-result: Reader & F32, 58 evidence: Witness.Sample,tail_evidence: Witness.Sample,reader,Grouped.fold_ranges(~Reader,~Context,~read,rest,reader,context)>) -> 59 Witness.Sample,reader,Grouped.grouped_tail(~Reader,result,reader => Grouped.fold_ranges(~Reader,~Context,~read,rest,reader,context))>: 60 Witness.Sample{head,equation} = evidence 61 %Equal.sym(Reader & F32,result,(reader,head),equation) : 62 Witness.Sample,reader,Grouped.grouped_tail(~Reader,_,reader => Grouped.fold_ranges(~Reader,~Context,~read,rest,reader,context))> 63 prepended(~Reader,reader,head,Grouped.fold_ranges(~Reader,~Context,~read,rest,reader,context),tail_evidence) 64 65 def groups(~Reader: Type,~Context: Data,~Evidence: @-reader: Reader -> Data,~read: Reader -> Context -> Nat -> Reader & F32, 66 ~preserves: @-reader: Reader -> @context: Context -> @position: Nat -> Evidence(reader) -> Witness.Sample, 67 ranges: List<&2,Grouped.Range>,-reader: Reader,+context: Context,+source: Evidence(reader)) -> 68 Witness.Sample,reader,Grouped.fold_ranges(~Reader,~Context,~read,ranges,reader,context)>: 69 match ranges: 70 case []: Witness.Sample{[],{==}} 71 case Grouped.Range{first,count} <> +rest: 72 group_tail(~Reader,~Context,~read,reader,context,rest,Grouped.fold(~Reader,~Context,~read,count,first,reader,context), 73 fold(~Reader,~Context,~Evidence,~read,~preserves,count,first,reader,context,source), 74 groups(~Reader,~Context,~Evidence,~read,~preserves,rest,reader,context,source)) 75 76 def reduced(~Reader: Type,-reader: Reader,-result: Reader & List<&2,F32>,evidence: Witness.Sample,reader,result>) -> 77 Witness.Sample: 78 Witness.Sample{values,equation} = evidence 79 %Equal.sym(Reader & List<&2,F32>,result,(reader,values),equation) : Witness.Sample 80 Witness.Sample{Grouped.tree(values),{==}} 81 82 def run(~Reader: Type,~Context: Data,~Evidence: @-reader: Reader -> Data,~read: Reader -> Context -> Nat -> Reader & F32, 83 ~preserves: @-reader: Reader -> @context: Context -> @position: Nat -> Evidence(reader) -> Witness.Sample, 84 ranges: List<&2,Grouped.Range>,-reader: Reader,context: Context,source: Evidence(reader)) -> 85 Witness.Sample: 86 reduced(~Reader,reader,Grouped.fold_ranges(~Reader,~Context,~read,ranges,reader,context),groups(~Reader,~Context,~Evidence,~read,~preserves,ranges,reader,context,source))