JSONAssemblyProof.atom_roundtrip: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as JSONAssemblyProof
Lines 72-94 of qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&start_line=72&end_line=94

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

def atom_roundtrip(+value: J.Value,
                   +mode: Mode,
                   -tail: List<J.Token>,
                   +acc: List<&2, J.Value>,
                   +fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, +kont: J.ParserKont, +text: String, started: {start(value, mode, acc, fields, kont) == J.NeedValue{kont} : J.Assembly}, completed_value: {completed(value, mode, acc, fields) == value : J.Value}, tokenized: {tokens(value, mode, tail) == J.Atom{J.decode_payload(text)} <> tail : List<J.Token>}, decoded: {J.decode_payload(text) == Done{value} : Result<&1, &1, J.Error, J.Value>}) -> {J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)) == J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))) : R()}:
    Equal.trans(R(),
        J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)),
        J.assemble(J.Atom{Done{value}} <> tail, J.NeedValue{kont}),
        J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))),
        Equal.trans(R(),
            J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)),
            J.assemble(tokens(value, mode, tail), J.NeedValue{kont}),
            J.assemble(J.Atom{Done{value}} <> tail, J.NeedValue{kont}),
            Equal.cong(J.Assembly, R(), state => J.assemble(tokens(value, mode, tail), state),
                start(value, mode, acc, fields, kont), J.NeedValue{kont}, started),
            Equal.cong(List<J.Token>, R(), stream => J.assemble(stream, J.NeedValue{kont}),
                tokens(value, mode, tail), J.Atom{Done{value}} <> tail,
                Equal.trans(List<J.Token>, tokens(value, mode, tail), J.Atom{J.decode_payload(text)} <> tail,
                    J.Atom{Done{value}} <> tail, tokenized,
                    Equal.cong(Result<&1, &1, J.Error, J.Value>, List<J.Token>, result => J.Atom{result} <> tail,
                        J.decode_payload(text), Done{value}, decoded)))),
        Equal.cong(J.Value, R(), item => J.assemble(tail, J.assembly_resume(kont, item)),
            value, completed(value, mode, acc, fields), Equal.sym(J.Value, completed(value, mode, acc, fields), value, completed_value)))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Assembly
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=ParserKont
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Token
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=assemble
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=assembly_resume
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=decode_payload
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=Mode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=completed
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=start
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=tokens