proofs/tensor_cursor_witness.bend
stelliferous@0.0.3.0 · 32 lines · 0 definitions
1import Base
2import stelliferous@0.0.3.0/tensor_cursor.bend as Cursor
3import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
4import stelliferous@0.0.3.0/proofs/traversal_visit_witness.bend as VisitWitness
5
6def read_value(~Element: Data,axes: Cursor.Levels(),address: U32,-storage: Array<Element>,-result: Array<Element> & Element,
7 observed: Witness.Read<Element,storage,result>) ->
8 VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read_value(~Element,axes,address,result)>:
9 match observed:
10 case Witness.Read{value,equation}:
11 %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
12 VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read_value(~Element,axes,address,_)>
13 VisitWitness.Sample{Cursor.advance(axes,address),value,{==}}
14
15def read(~Element: Data,-storage: Array<Element>,cursor: Cursor.Cursor,evidence: Witness.ArrayWitness<Element,storage>) ->
16 VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read(~Element,storage,cursor)>:
17 Cursor.Cursor{axes,+address} = cursor
18 read_value(~Element,axes,address,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))
19
20def stride_value(~Element: Data,address: U32,+stride: U32,-storage: Array<Element>,-result: Array<Element> & Element,
21 observed: Witness.Read<Element,storage,result>) ->
22 VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.stride_value(~Element,address,stride,result)>:
23 match observed:
24 case Witness.Read{value,equation}:
25 %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
26 VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.stride_value(~Element,address,stride,_)>
27 VisitWitness.Sample{Cursor.Stride{(address + stride : U32),stride},value,{==}}
28
29def read_stride(~Element: Data,-storage: Array<Element>,cursor: Cursor.Stride,evidence: Witness.ArrayWitness<Element,storage>) ->
30 VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.read_stride(~Element,storage,cursor)>:
31 Cursor.Stride{+address,+stride} = cursor
32 stride_value(~Element,address,stride,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))