~/jendhub

src/storage/certificates.bend

bendtorch-core@0.1.0.0 · 31 lines · 4 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
4import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
5
6def get_result(-T: Data, +d: Nat, original: Array<T>, +i: U32, -result: Array<T> & T,
7  equal: {result == Array.get(T, original, i) : Array<T> & T},
8  valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, Refinement.first(T, result)):
9  %Equal.sym(Array<T> & T, result, Array.get(T, original, i), equal) :
10    Model.Balanced(T, d, Refinement.first(T, _))
11  Refinement.law_get_balanced(T, d, original, i, valid)
12
13def set_result(-T: Data, +d: Nat, original: Array<T>, +i: U32, +value: T, -result: Array<T>,
14  equal: {result == Array.set(T, original, i, value) : Array<T>},
15  valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, result):
16  %Equal.sym(Array<T>, result, Array.set(T, original, i, value), equal) : Model.Balanced(T, d, _)
17  Refinement.law_set_balanced(T, d, original, i, value, valid)
18
19def clone_first(-T: Data, +d: Nat, original: Array<T>, -result: Array<T> & Array<T>,
20  equal: {result == Array.clone(T, original) : Array<T> & Array<T>},
21  valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, Pair.fst(Array<T>, Array<T>, result)):
22  %Equal.sym(Array<T> & Array<T>, result, Array.clone(T, original), equal) :
23    Model.Balanced(T, d, Pair.fst(Array<T>, Array<T>, _))
24  Clone.first_balanced(T, d, original, Clone.certify(T, d, original, valid))
25
26def clone_second(-T: Data, +d: Nat, original: Array<T>, -result: Array<T> & Array<T>,
27  equal: {result == Array.clone(T, original) : Array<T> & Array<T>},
28  valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, result)):
29  %Equal.sym(Array<T> & Array<T>, result, Array.clone(T, original), equal) :
30    Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, _))
31  Clone.second_balanced(T, d, original, Clone.certify(T, d, original, valid))