1 import Base 2 import ../tensor_indexed.bend as Indexed 3 import ../traversal_array.bend as Traversal 4 import ../traversal_loop.bend as Loop 5 import ./storage_tree_model.bend as Tree 6 import ./storage_certificate.bend as Certificate 7 import ./storage_witness.bend as Witness 8 import ./traversal_witness.bend as TraversalWitness 9 import ./traversal_certificate.bend as TraversalCertificate 10 11 def sample(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element, 12 -input: Array,+context: Context,+position: U32,-result: Array & Element, 13 evidence: TraversalWitness.Sample,Element,input,result>) -> 14 TraversalWitness.Sample,Element,input,Indexed.value(~Element,~Context,~index,~operation,context,position,result)>: 15 match evidence: 16 case TraversalWitness.Sample{value,equation}: 17 %Equal.sym(Array & Element,result,(input,value),equation) : 18 TraversalWitness.Sample,Element,input,Indexed.value(~Element,~Context,~index,~operation,context,position,_)> 19 TraversalWitness.Sample{operation(index(context,position),value),{==}} 20 21 def read(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element, 22 -input: Array,context: Context,position: U32,evidence: Witness.ArrayWitness) -> 23 TraversalWitness.Sample,Element,input,Indexed.read(~Element,~Context,~index,~operation,input,context,position)>: 24 +position = position 25 sample(~Element,~Context,~index,~operation,input,context,position,Array.get(Element,input,position), 26 TraversalWitness.array_sample(~Element,input,Array.get(Element,input,position),Witness.observed(Element,input,position,evidence))) 27 28 def preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element, 29 +depth: Nat,call: Indexed.Call,-input: Array,-output: Array,input_certificate: Certificate.Certificate, 30 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array}) -> 31 TraversalWitness.ResultEvidence,Element,input,depth,Indexed.run(~Element,~Context,~index,~operation,call,input,output)>: 32 Indexed.Call{count,context} = call 33 TraversalCertificate.completed(~Array,~Element,~Context,~TraversalWitness.array_evidence(~Element), 34 ~Traversal.run(~Array,~Element,~Context,~Indexed.read(~Element,~Context,~index,~operation),~Indexed.destination(~Context)), 35 ~TraversalWitness.run(~Array,~Element,~Context,~TraversalWitness.array_evidence(~Element),~Indexed.read(~Element,~Context,~index,~operation), 36 ~Indexed.destination(~Context),~read(~Element,~Context,~index,~operation)), 37 count,0,context,input,output,Certificate.witness(Element,input,input_certificate),depth,equation) 38 39 def next_block(~Element: Data,~Context: Data,+depth: Nat,block: U32,size: U32,context: Context,-input: Array,-state: Traversal.State<&1,&1,Array,Array,Indexed.Block>, 40 evidence: TraversalWitness.StateEvidence,Element,Indexed.Block,input,depth,state>) -> 41 TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth,Indexed.next_block(~Element,~Context,block,size,context,state)>: 42 match evidence: 43 case TraversalWitness.StateEvidence{output,position,inner,equation,output_evidence}: 44 %Equal.sym(Traversal.State<&1,&1,Array,Array,Indexed.Block>,state,Traversal.State{input,output,position,inner},equation) : 45 TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth,Indexed.next_block(~Element,~Context,block,size,context,_)> 46 TraversalWitness.StateEvidence{output,position,Indexed.Blocks{(block + 1 : U32),size,context},{==},output_evidence} 47 48 def block_step(~Element: Data,~Context: Data,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element,+depth: Nat,-input: Array,-state: Traversal.State<&1,&1,Array,Array,Indexed.Blocks>, 49 +input_evidence: Witness.ArrayWitness,evidence: TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth,state>) -> 50 TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth,Indexed.block_step(~Element,~Context,~base,~operation,state)>: 51 match evidence: 52 case TraversalWitness.StateEvidence{output,+position,Indexed.Blocks{+block,+size,+context},equation,output_evidence}: 53 %Equal.sym(Traversal.State<&1,&1,Array,Array,Indexed.Blocks>,state,Traversal.State{input,output,position,Indexed.Blocks{block,size,context}},equation) : 54 TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth,Indexed.block_step(~Element,~Context,~base,~operation,_)> 55 next_block(~Element,~Context,depth,block,size,context,input, 56 Traversal.run(~Array,~Element,~Indexed.Block,~Indexed.read(~Element,~Indexed.Block,~Indexed.block_index,~operation),~Indexed.destination(~Indexed.Block),U32.to_nat(size), 57 Traversal.State{input,output,position,Indexed.Block{base(context,block),position}}), 58 TraversalWitness.run(~Array,~Element,~Indexed.Block,~TraversalWitness.array_evidence(~Element),~Indexed.read(~Element,~Indexed.Block,~Indexed.block_index,~operation), 59 ~Indexed.destination(~Indexed.Block),~read(~Element,~Indexed.Block,~Indexed.block_index,~operation),depth,U32.to_nat(size),input, 60 Traversal.State{input,output,position,Indexed.Block{base(context,block),position}},input_evidence, 61 TraversalWitness.StateEvidence{output,position,Indexed.Block{base(context,block),position},{==},output_evidence})) 62 63 def block_loop(~Element: Data,~Context: Data,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element,+depth: Nat,count: Nat,-input: Array,-state: Traversal.State<&1,&1,Array,Array,Indexed.Blocks>, 64 +input_evidence: Witness.ArrayWitness,evidence: TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth,state>) -> 65 TraversalWitness.StateEvidence,Element,Indexed.Blocks,input,depth, 66 Loop.run(~Traversal.State<&1,&1,Array,Array,Indexed.Blocks>,~Indexed.block_step(~Element,~Context,~base,~operation),count,state)>: 67 match count: 68 case 0n: evidence 69 case 1n+rest: 70 block_loop(~Element,~Context,~base,~operation,depth,rest,input,Indexed.block_step(~Element,~Context,~base,~operation,state),input_evidence, 71 block_step(~Element,~Context,~base,~operation,depth,input,state,input_evidence,evidence)) 72 73 type Tiling<-Context: Data> is Data: 74 Tiling{total: U32,context: Context} 75 76 def tiled_operation(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element, 77 tiling: Tiling,input: Array,output: Array) -> Array & Array: 78 Tiling{total,context} = tiling 79 Indexed.run_tiled(~Element,~Context,~index,~base,~blocks,~size,~operation,total,context,input,output) 80 81 def whole_preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element, 82 +depth: Nat,whole: Bool,blocks: U32,size: U32,total: U32,context: Context,-input: Array,-output: Array,input_certificate: Certificate.Certificate, 83 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array}) -> 84 TraversalWitness.ResultEvidence,Element,input,depth,Indexed.run_whole(~Element,~Context,~index,~base,~operation,whole,blocks,size,total,context,input,output)>: 85 match whole: 86 case True{}: 87 TraversalCertificate.completed(~Array,~Element,~Indexed.Blocks,~TraversalWitness.array_evidence(~Element), 88 ~Loop.run(~Traversal.State<&1,&1,Array,Array,Indexed.Blocks>,~Indexed.block_step(~Element,~Context,~base,~operation)),~block_loop(~Element,~Context,~base,~operation), 89 U32.to_nat(blocks),0,Indexed.Blocks{0,size,context},input,output,Certificate.witness(Element,input,input_certificate),depth,equation) 90 case False{}: 91 preserves(~Element,~Context,~index,~operation,depth,Indexed.Call{U32.to_nat(total),context},input,output,input_certificate,equation) 92 93 def tiled_preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element, 94 +depth: Nat,tiling: Tiling,-input: Array,-output: Array,input_certificate: Certificate.Certificate, 95 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array}) -> 96 TraversalWitness.ResultEvidence,Element,input,depth,tiled_operation(~Element,~Context,~index,~base,~blocks,~size,~operation,tiling,input,output)>: 97 Tiling{+total,+context} = tiling 98 whole_preserves(~Element,~Context,~index,~base,~operation,depth,U32.is_le(total,Indexed.block_limit()) && Nat.is_eq(Nat.mul(U32.to_nat(blocks(context)),U32.to_nat(size(context))),U32.to_nat(total)), 99 blocks(context),size(context),total,context,input,output,input_certificate,equation) 100 101 def tiled_certificates(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element, 102 +total: U32,+context: Context,-input: Array,-output: Array,input_certificate: Certificate.Certificate, 103 output_certificate: Certificate.Certificate) -> 104 TraversalCertificate.Certificates,Element,Certificate.family(~Element),Indexed.run_tiled(~Element,~Context,~index,~base,~blocks,~size,~operation,total,context,input,output)>: 105 Certificate.Certificate{+depth,+equation} = input_certificate 106 TraversalCertificate.operation(~Array,~Element,~Tiling,~Certificate.family(~Element), 107 ~tiled_operation(~Element,~Context,~index,~base,~blocks,~size,~operation),~tiled_preserves(~Element,~Context,~index,~base,~blocks,~size,~operation), 108 Tiling{total,context},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)