proofs/paired_read_refinement.bend

stelliferous@0.0.3.0 · 41 lines · 0 definitions

1import Base
2import stelliferous@0.0.3.0/kernel_block.bend as Block
3
4def read_at_refines(
5  ~Native: Type,~Context: Data,~Element: Data,~Index: Data,
6  ~read: Native -> Context -> Index -> Native & Element,
7  -source: Native,+context: Context,+first: Index,+second: Index,+left: Element,+right: Element,
8  first_read: {read(source,context,first) == (source,left) : Native & Element},
9  second_read: {read(source,context,second) == (source,right) : Native & Element}
10) -> {Block.read_at(~Native,~Context,~Element,~Index,~read,source,context,first,second) ==
11  (source,Block.Twin{left,right}) : Native & Block.Twin<Element>}:
12  %Equal.sym(Native & Element,read(source,context,first),(source,left),first_read) :
13    {Block.read_second(~Native,~Context,~Element,~Index,~read,_,context,second) ==
14      (source,Block.Twin{left,right}) : Native & Block.Twin<Element>}
15  %Equal.sym(Native & Element,read(source,context,second),(source,right),second_read) :
16    {Block.finish_pair(~Native,~Element,left,_) == (source,Block.Twin{left,right}) : Native & Block.Twin<Element>}
17  {==}
18
19# Pair composition is independent of element shape and block width.
20def pair_sample(
21  ~Model: Data,~Context: Data,~Element: Data,
22  ~sample: Model -> Context -> Nat -> Element,~stride: Nat,
23  model: Model,context: Context,index: Nat
24) -> Block.Twin<Element>:
25  +model = model
26  +context = context
27  +index = index
28  Block.Twin{sample(model,context,index),sample(model,context,Nat.add(index,stride))}
29
30def read_pair_refines(
31  ~Native: Type,~Model: Data,~Context: Data,~Element: Data,
32  ~pack: Model -> Native,
33  ~read: Native -> Context -> Nat -> Native & Element,
34  ~sample: Model -> Context -> Nat -> Element,
35  ~stride: Nat,+model: Model,+context: Context,+index: Nat,
36  first_read: {read(pack(model),context,index) == (pack(model),sample(model,context,index)) : Native & Element},
37  second_read: {read(pack(model),context,Nat.add(index,stride)) == (pack(model),sample(model,context,Nat.add(index,stride))) : Native & Element}
38) -> {Block.read_pair(~Native,~Context,~Element,~read,~stride,pack(model),context,index) == (pack(model),pair_sample(~Model,~Context,
39    ~Element,~sample,~stride,model,context,index)) : Native & Block.Twin<Element>}:
40  read_at_refines(~Native,~Context,~Element,~Nat,~read,pack(model),context,index,Nat.add(index,stride),
41    sample(model,context,index),sample(model,context,Nat.add(index,stride)),first_read,second_read)