proofs/grouped_source_witness.bend
stelliferous@0.0.3.0 · 86 lines · 0 definitions
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.
3import Base
4import stelliferous@0.0.3.0/traversal_grouped.bend as Grouped
5import stelliferous@0.0.3.0/traversal_loop.bend as Loop
6import stelliferous@0.0.3.0/proofs/traversal_witness.bend as Witness
7
8type StateEvidence<-Reader: Type,-Context: Data,-reader: Reader,-state: Grouped.State<Reader,Context>> is Data:
9 StateEvidence{-total: F32,position: Nat,context: Context,
10 equation: {state == Grouped.State{reader,context,position,total} : Grouped.State<Reader,Context>}}
11
12def advanced(~Reader: Type,~Context: Data,-reader: Reader,+context: Context,+position: Nat,-total: F32,-result: Reader & F32,
13 evidence: Witness.Sample<Reader,F32,reader,result>) ->
14 StateEvidence<Reader,Context,reader,Grouped.advanced(~Reader,~Context,context,position,total,result)>:
15 Witness.Sample{value,equation} = evidence
16 %Equal.sym(Reader & F32,result,(reader,value),equation) : StateEvidence<Reader,Context,reader,Grouped.advanced(~Reader,~Context,context,position,total,_)>
17 StateEvidence{(total + value : F32),1n+position,context,{==}}
18
19def 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<Reader,F32,reader,read(reader,context,position)>,
21 -reader: Reader,-state: Grouped.State<Reader,Context>,source: Evidence(reader),evidence: StateEvidence<Reader,Context,reader,state>) ->
22 StateEvidence<Reader,Context,reader,Grouped.step(~Reader,~Context,~read,state)>:
23 StateEvidence{total,+position,+context,equation} = evidence
24 %Equal.sym(Grouped.State<Reader,Context>,state,Grouped.State{reader,context,position,total},equation) : StateEvidence<Reader,Context,reader,Grouped.step(~Reader,~Context,~read,_)>
25 advanced(~Reader,~Context,reader,context,position,total,read(reader,context,position),preserves(reader,context,position,source))
26
27def 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<Reader,F32,reader,read(reader,context,position)>,
29 count: Nat,-reader: Reader,-state: Grouped.State<Reader,Context>,+source: Evidence(reader),evidence: StateEvidence<Reader,Context,reader,state>) ->
30 StateEvidence<Reader,Context,reader,Loop.run(~Grouped.State<Reader,Context>,~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
37def finished(~Reader: Type,~Context: Data,-reader: Reader,-state: Grouped.State<Reader,Context>,evidence: StateEvidence<Reader,Context,reader,state>) ->
38 Witness.Sample<Reader,F32,reader,Grouped.finished(~Reader,~Context,state)>:
39 StateEvidence{total,position,context,equation} = evidence
40 %Equal.sym(Grouped.State<Reader,Context>,state,Grouped.State{reader,context,position,total},equation) : Witness.Sample<Reader,F32,reader,Grouped.finished(~Reader,~Context,_)>
41 Witness.Sample{total,{==}}
42
43def 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<Reader,F32,reader,read(reader,context,position)>,
45 count: Nat,position: Nat,-reader: Reader,context: Context,source: Evidence(reader)) ->
46 Witness.Sample<Reader,F32,reader,Grouped.fold(~Reader,~Context,~read,count,position,reader,context)>:
47 finished(~Reader,~Context,reader,Loop.run(~Grouped.State<Reader,Context>,~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
50def prepended(~Reader: Type,-reader: Reader,-head: F32,-result: Reader & List<&2,F32>,evidence: Witness.Sample<Reader,List<&2,F32>,reader,result>) ->
51 Witness.Sample<Reader,List<&2,F32>,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,List<&2,F32>,reader,Grouped.prepend(~Reader,head,_)>
54 Witness.Sample{head <> tail,{==}}
55
56def 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<Reader,F32,reader,result>,tail_evidence: Witness.Sample<Reader,List<&2,F32>,reader,Grouped.fold_ranges(~Reader,~Context,~read,rest,reader,context)>) ->
59 Witness.Sample<Reader,List<&2,F32>,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,List<&2,F32>,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
65def 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<Reader,F32,reader,read(reader,context,position)>,
67 ranges: List<&2,Grouped.Range>,-reader: Reader,+context: Context,+source: Evidence(reader)) ->
68 Witness.Sample<Reader,List<&2,F32>,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
76def reduced(~Reader: Type,-reader: Reader,-result: Reader & List<&2,F32>,evidence: Witness.Sample<Reader,List<&2,F32>,reader,result>) ->
77 Witness.Sample<Reader,F32,reader,Grouped.reduced(~Reader,result)>:
78 Witness.Sample{values,equation} = evidence
79 %Equal.sym(Reader & List<&2,F32>,result,(reader,values),equation) : Witness.Sample<Reader,F32,reader,Grouped.reduced(~Reader,_)>
80 Witness.Sample{Grouped.tree(values),{==}}
81
82def 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<Reader,F32,reader,read(reader,context,position)>,
84 ranges: List<&2,Grouped.Range>,-reader: Reader,context: Context,source: Evidence(reader)) ->
85 Witness.Sample<Reader,F32,reader,Grouped.run(~Reader,~Context,~read,ranges,reader,context)>:
86 reduced(~Reader,reader,Grouped.fold_ranges(~Reader,~Context,~read,ranges,reader,context),groups(~Reader,~Context,~Evidence,~read,~preserves,ranges,reader,context,source))