def read_hit_inspect

bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:59

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

59def read_hit_inspect(+depth: Nat, +length: Nat, +index: U32, +property: Totality.Property, array: Array<F32>,
60  balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
61  InspectionModel<storage_inspect(property, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
62    array_inspect(depth, length, property, array)>:
63  match property:
64    case Totality.Dimensions{}:
65      InspectionModel{finish_read_inspect(depth, length, array, index, Totality.Dimensions{}, Array.get(F32, array, index), {==}, balanced, valid)}
66    case Totality.Checked{+other}:
67      InspectionModel{Equal.trans(Totality.Inspection,
68        storage_inspect(Totality.Checked{other}, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
69        array_inspect(depth, length, Totality.Checked{other}, Refinement.first(F32, Array.get(F32, array, index))),
70        array_inspect(depth, length, Totality.Checked{other}, array),
71        finish_read_inspect(depth, length, array, index, Totality.Checked{other}, Array.get(F32, array, index), {==}, balanced, valid),
72        Equal.cong(Array<F32>, Totality.Inspection, a => array_inspect(depth, length, Totality.Checked{other}, a),
73          Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}
74    case Totality.Raw{+other}:
75      InspectionModel{Equal.trans(Totality.Inspection,
76        storage_inspect(Totality.Raw{other}, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
77        array_inspect(depth, length, Totality.Raw{other}, Refinement.first(F32, Array.get(F32, array, index))),
78        array_inspect(depth, length, Totality.Raw{other}, array),
79        finish_read_inspect(depth, length, array, index, Totality.Raw{other}, Array.get(F32, array, index), {==}, balanced, valid),
80        Equal.cong(Array<F32>, Totality.Inspection, a => array_inspect(depth, length, Totality.Raw{other}, a),
81          Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}