Exact Codecsconcept:exact-codecs

type-metadata-exactclaim:type-metadata-exact

Structural TypeScript metadata retains the exact stored Ty declaration

The two directions of the proposed type-metadata-exact claim, with no source restriction.

Module

Effect4.Laws.Codegen.Metadata

And
  (∀ (t : Effect4.Program.Ty),
    Eq (Effect4.Codegen.Metadata.readTy (Effect4.Codegen.Metadata.writeTy t)) (Option.some t))
  (∀ (e : TypeScript.Expr) (t : Effect4.Program.Ty),
    Eq (Effect4.Codegen.Metadata.readTy e) (Option.some t) →
      Eq (Effect4.Codegen.Metadata.writeTy t) e)

decode-iffclaim:decode-iff

Exactness of JSON decoding modulo normJ

The JSON pair is an exact embedding modulo N_J (decisions row 128; AGENTS.md's exact embedding with the normaliser Codec.normJ): a JSON decodes to a value exactly when it is that value's encoding up to the order of object entries.

Module

Effect4.Laws.Schema.Codec

Literature

RendelOstermann2010, audit P32 (definitionUsed)

∀ {t : Effect4.Program.Ty} {j : Effect4.Json} {v : Effect4.Machine.Val},
  Iff (Eq (Effect4.Schema.decode t j) (Option.some v))
    (Exists fun j' =>
      And (Eq (Effect4.Schema.encode t v) (Option.some j'))
        (Eq (Effect4.Schema.Codec.normJ j') (Effect4.Schema.Codec.normJ j)))

decode-encodeclaim:decode-encode

Retraction of JSON encoding on canonical types

S-3 round trip without an arbitrary default JSON inhabitant or a failing get!.

Module

Effect4.Laws.Schema.Codec

Literature

FosterEtAl2007, audit P11 (adaptedResult)

∀ {t : Effect4.Program.CTy} {v : Effect4.Machine.Val},
  Eq (Effect4.Program.Val.hasTy v t.toRaw) Bool.true →
    Eq (t.toRaw.isCodecValue v) Bool.true →
      Eq ((Effect4.Schema.encode t.toRaw v).bind (Effect4.Schema.decode t.toRaw)) (Option.some v)

of-schema-exactclaim:of-schema-exact

Exactness of Schema reader modulo normS

Exactness of the reader, modulo N_S (decisions row 128): a representation ofSchema reads is the read type's schema up to the annotation entries that change no decoding. By fun_induction ofSchema: one case per arm and branch of the reader, the refusing ones closed by nomatch.

Module

Effect4.Schema.Bridge

Literature

RendelOstermann2010, audit P32 (adaptedResult)

∀ (r : Effect4.Representation) (t : Effect4.Program.Ty),
  Eq (Effect4.Schema.Bridge.ofSchema r) (Option.some t) →
    Eq (Effect4.Schema.Bridge.normS r) (Effect4.Schema.Bridge.schema t)

of-schema-schemaclaim:of-schema-schema

Retraction of Schema generation on reserved-free types

Raw Schema retraction on the closed exact profile. The profile excludes unsupported forms, nonstring map keys, two-item tuples, and the reserved handle id.

Module

Effect4.Schema.Bridge

∀ (t : Effect4.Program.Ty),
  Eq t.closed Bool.true →
    Eq (Effect4.Schema.Bridge.reservedFree t) Bool.true →
      Eq (Effect4.Schema.Bridge.ofSchema (Effect4.Schema.Bridge.schema t)) (Option.some t)

collection-term-print-readclaim:collection-term-print-read

Every scoped term reconstructs after structural printing, including records, payload class constructions under classes that cover them (decisions row 120), and every static tuple index

The term round trip (collection-term-print-read): a scoped term whose class constructions the classes cover reads back from its printing. Since decisions row 120, part E2, a class construction prints as new Tag({ … }) and reads back from the module's classes, with _tag restored first (Classes.classTag?); placed at R8 (translation-simulation) as a step of read_print, and at R3 as the record terms' printed form.

Module

Effect4.Laws.Codegen.ReadLeaf

∀ {classes : Effect4.Codegen.Classes.Classes} {n : Nat} (t : Effect4.Program.Term),
  Eq (Effect4.Program.Term.scoped n t) Bool.true →
    Eq (Effect4.Program.Term.covers classes t) Bool.true →
      Eq t.unannotated Bool.true →
        Eq (Effect4.Program.readTerm classes n (Effect4.Program.printTerm n t)) (Except.ok t)

record-codec-layoutclaim:record-codec-layout

Record JSON decoding is exact under normJ; named record values retain optional presence

The JSON pair is an exact embedding modulo N_J (decisions row 128; AGENTS.md's exact embedding with the normaliser Codec.normJ): a JSON decodes to a value exactly when it is that value's encoding up to the order of object entries.

Module

Effect4.Laws.Schema.Codec

∀ {t : Effect4.Program.Ty} {j : Effect4.Json} {v : Effect4.Machine.Val},
  Iff (Eq (Effect4.Schema.decode t j) (Option.some v))
    (Exists fun j' =>
      And (Eq (Effect4.Schema.encode t v) (Option.some j'))
        (Eq (Effect4.Schema.Codec.normJ j') (Effect4.Schema.Codec.normJ j)))

service-identifier-injectiveclaim:service-identifier-injective

At one signature's scope key, distinct service keys print distinct target Identifier types

At one fixed signature's scope identity, different keys have different target Identifier syntax, independently of their carriers. This is a syntax theorem; the pinned TypeScript assignment controls separately test the target interpretation.

Module

Effect4.Laws.Codegen.ReadLeaf

∀ (scopeKey : Effect4.ServiceKey), Function.Injective (Effect4.Program.keyIdentifier scopeKey)

error-payload-exactclaim:error-payload-exact

A typed failure's record payload reads back exactly through the error image: errOf inverts valOfErr at every represented error, the handle-free record frame included (decisions row 120)

A value read out of the error alphabet rebuilds the same error (errOf on the left inverse of valOfErr). boom has no image, so it is excluded by the hypothesis rather than by a side condition. A payload rebuilds through the last arm (errOf_payload).

Module

Effect4.Laws.Program.Admit

∀ (e : Effect4.Machine.Err) (v : Effect4.Machine.Val),
  Eq (Effect4.Program.valOfErr e) (Option.some v) → Eq (Effect4.Program.errOf v) e

payload-class-decl-exactclaim:payload-class-decl-exact

An admitted module's payload class declarations are exactly the ones the printer writes for the program it reads to (decisions row 120, part E2)

The envelope admits exactly the printed class declarations (decisions row 120, part E2): an admitted module's leading class declarations are the ones the printer writes for the program it reads to (ClassTable.moduleClasses), in order. Concept exact-codecs, claim payload-class-decl-exact (R3); with ModuleEmission.admit, the class section's exact embedding at the boundary.

Module

Effect4.Laws.Codegen.Admit

∀ {table : Effect4.Program.RowTable} {name : String}
  {allowed : List Effect4.Codegen.Bindings.Origin} {ambient : List TypeScript.Import}
  {module : TypeScript.Module} {r : Effect4.Codegen.ModuleReading table name allowed ambient},
  Eq (Effect4.Codegen.admitModule name module table allowed ambient) (Except.ok r) →
    Eq (Effect4.Program.splitClasses module.decls).fst r.classDecls

mask-rows-table-premisesclaim:mask-rows-table-premises

The mask's two printed rows, the getter as the mask that answers its own restore and a restore site as pipe(E, saved), have two reserved heads and keep the row table's nine decided premises at the extended table; a restore site is readable exactly when its saved term is a readable leaf and its body is readable; read_print and read_exact keep their statements (decisions row 245; program syntax only)

The mask's two rows keep the table's premises (the claim mask-rows-table-premises; concept exact-codecs, requirement R8; decisions row 245).

Reach: program syntax. The table is the one table of Codegen/Templates.lean, and each premise is decided again by the kernel at the extended table. It does not establish typing: a restore site of an ill-typed saved term reads back as well. It establishes no behaviour of a target. An annotated position prints and is not read, as before: Readable excludes it. Its consumers are the checked module production and reading, through read_print and read_exact.

Module

Effect4.Laws.Codegen.Mask

Effect4.Program.MaskRowsPremises

sketch-wireclaim:sketch-wire

A sketch's bytes are its program's canonical bytes and its hole table's (Sketch.encode): a well-formed sketch reads back (Sketch.decode_encode), and whatever reads was that sketch's bytes, well-formed (Sketch.decode_exact); the query tool takes a hole table with a request and gives the grown one with an omission, so the sketch it answers can be sent back; nothing of a stored sketch's renumbering when its application gains a row (decisions row 305, point 3)

Exactness: whatever reads as a sketch was that sketch's bytes, and its value trees are well-formed. The pointer of sketch-wire.

Module

Effect4.Laws.Program.SketchWire

∀ {b : Prod Effect4.Store.Bytes Effect4.Store.Bytes} {s : Effect4.Program.Sketch},
  Eq (Effect4.Program.Sketch.decode b) (Option.some s) →
    And (Eq b s.encode)
      (And (Effect4.Store.ProgramGen.EffC.instCanonicalEff.toVal s.program).WF
        (Effect4.Store.instCanonicalList.toVal s.holes).WF)

json-read-exactclaim:json-read-exact

A canonical carrier read from JSON is the carrier whose canonical print that JSON is (Canonical.ofJson_exact): the reader takes only the canonical print, a number as the binary64 of a natural, hex exact, fields in the shape's order, a case's name checked against its tag; JSON whose objects come in any order reads once ordered by the shape (Canonical.ofJsonAnyOrder), the named normaliser; nothing of the round trip, which needs every natural at most 2^53 and no option holding a shape that prints null (the agent's schema form; decisions row 334)

A carrier read from JSON is the carrier whose canonical print that JSON is. The pointer of json-read-exact.

Module

Effect4.Laws.Store.ShapeRead

∀ {α : Type} [inst : Effect4.Store.Canonical α] {j : Effect4.Json} {a : α},
  Eq (Effect4.Store.Canonical.ofJson j) (Option.some a) → Eq (Effect4.Store.Canonical.print a) j

typed-print-connectorclaim:typed-print-connector

The typed print, the table-driven print with each node's address, writes a call's type arguments where the row check joins the call's request, in the order of the row's variables, and the type arguments of an approved eliminator site where the site's checked context needs them; a program with no such row and no such site (NoJoin) has the typed print that is its print, byte for byte (printTyped_eq_print); it does not say that tsgo accepts a printed call (decisions row 325)

Without a row join annotation, the typed print is the ordinary print. This remains the pointer of typed-print-connector, exact-codecs, R8. The NoJoin premise states absence at every checked address. It makes no TypeScript typing or execution claim.

Module

Effect4.Laws.Codegen.PrintTyped

∀ {Op : Type} (s : Effect4.Program.Signature Op) (env0 : Effect4.Program.TyEnv)
  (p : Effect4.Program.Eff Op),
  Effect4.Program.NoJoin s env0 p →
    Eq (Effect4.Program.printTyped s env0 p) (Effect4.Program.print s (List.length env0) p)

typed-print-erasureclaim:typed-print-erasure

A successful typed print erases to the print: at a readable program and a lawful spelling, the named erasure of the inserted type arguments gives the print of the program, byte for byte; the erasure keeps an operation's own arguments and the stored type annotations; it does not say that tsgo accepts the typed print, or anything of its run (decisions row 325; slice P2b)

Every successful public typed print erases to the existing ordinary print. The exact old readable and spelling premises remain visible (exact-codecs, R8).

Module

Effect4.Laws.Codegen.PrintTyped

∀ {Op : Type} {classes : Effect4.Codegen.Classes.Classes} {sig : Effect4.Program.Signature Op}
  {spell : String → List Effect4.Program.RowArg → Option Op},
  Effect4.Program.LawfulSpelling sig spell →
    ∀ {env0 : Effect4.Program.TyEnv} {e : Effect4.Program.Eff Op},
      Eq (Effect4.Program.Readable classes sig (List.length env0) e) Bool.true →
        ∀ {x : TypeScript.Expr},
          Eq (Effect4.Program.printTyped sig env0 e) (Except.ok x) →
            Eq (Effect4.Program.print sig (List.length env0) e)
              (Except.ok (Effect4.Codegen.eraseJoinArgs classes sig spell (List.length env0) x))

typed-print-readclaim:typed-print-read

The reader reads a successful typed print back to its program after the named erasure, at a readable program and a lawful spelling, by the existing read_print; what the typed reader accepts is the erasure of a print (readTyped_exact); the raw reader still refuses an inserted argument before the erasure, and no equality of raw foreign spellings follows (decisions row 325; slice P3)

The existing reader reads every successful public typed print after named erasure. The theorem carries the existing read_print fragment (exact-codecs, R8).

Module

Effect4.Laws.Codegen.PrintTyped

∀ {Op : Type} {classes : Effect4.Codegen.Classes.Classes} {sig : Effect4.Program.Signature Op}
  {spell : String → List Effect4.Program.RowArg → Option Op},
  Effect4.Program.LawfulSpelling sig spell →
    ∀ {env0 : Effect4.Program.TyEnv} {e : Effect4.Program.Eff Op},
      Eq (Effect4.Program.Readable classes sig (List.length env0) e) Bool.true →
        ∀ {x : TypeScript.Expr},
          Eq (Effect4.Program.printTyped sig env0 e) (Except.ok x) →
            Eq (Effect4.Codegen.readTyped classes sig spell (List.length env0) x) (Except.ok e)

module-defs-round-tripclaim:module-defs-round-trip

A module with a definition block reads back: the module printer prints each definition as a constant before the layers, an arrow from its request and its parameters, each a function named by its declaration (slice HO-3a), with its declared result type around a suspension of its body, an invocation as the definition's name applied to its request, and an invocation with programs as that name applied to the request and to each program as an arrow of the binder due at the call (slice HO-3b, read back under the block's invocation laws, LawfulInvokes); the block's module layers print after the services as constants named by their paths (printModuleLayers), and a reference to one prints as that name; when each declaration has readable columns, an empty requirement row and a name with no layer path, each body and each of its own layers at the signature and spelling map its parameters extend (LawfulSpelling.withParams; a body's own hoisted layers print as constants at the top of its suspension, row 341, step 3b), the main program, each layer and each module layer read back at the block's signature through the block's spelling map, and each module layer's name decodes to its path, the module reads back to the program, its module layers rebuilt in order (readModule_printModule_defs); the block's spelling map is lawful under the signature's invocation laws and readable names (LawfulSpelling.withDefs), which the native signature and the printer's name check give (nativeCalls, defsNamed_of_fault), so the program interface's module round trip holds for a program with a block (Api.printModule_roundTrip); the printer refuses an empty block and a reference out of its scope (Eff.inScope), and a requirement row other than never is printed and not read; the block's services, declared by its definitions' roles, print after the definitions as an Effect service's key and layer each (printServices) and give the roles back from the layers (roleOf), when serviceFault finds no fault (printServices_ok, restoreRoles); it does not say that tsgo accepts the module or how rc.112 runs it (decisions rows 328, 338, 339 and 341, G6; slices PROC-3 and CO-6b)

G6: the round trip of a module with a definition block (decisions rows 328 and 341). The module printer prints a block's definitions as constants, each body's own hoisted layers as constants at the top of its suspension (decisions row 341, step 3), then the block's services' keys and layers (decisions rows 338 and 339), then its module layers, each named by its path (step 2), before the hoisted layers no body took and the main declaration (printModule). When each declaration is readable (DefDecl.readable: readable columns, an empty requirement row, a name with no layer path); each body and each of its own layers read back from their printing at the signature its parameters extend (bodyDeclOf); the main program, each module layer and each other hoisted layer read back at the block's signature through the block's spelling map (defsSpell); and the layers' names decode, the module reads back to the program, with each definition's role given back by the services' layers (roleOf, restoreRoles) and the module's layers by their paths (moduleLayersOf). No hoisted layer stands in the module (Eff.hoistAll_outside). The premises concern the pieces, as readModule_printModule's do, and they are stated of any reader.

Restated for step 3: each body reads back itself (it was its suspension), and the hoisted layers' premise is split by the scope that prints them (localsReadable, layersReadable).

Placement: concept exact-codecs, claim module-defs-round-trip, requirement R8. Consumers: the module round trip of the readable domain (readModule_printModule_readable) and, through it, ModuleEmission.readModule. It is a structural equation: it does not say that tsgo accepts the module or how rc.112 runs it.

Module

Effect4.Laws.Codegen.Module

∀ {Op : Type} {classes : Effect4.Codegen.Classes.Classes} {sig : Effect4.Program.Signature Op}
  {spell : String → List Effect4.Program.RowArg → Option Op} {call param : Nat → Op}
  {root main body : Effect4.Program.Eff Op} {defs : List Effect4.Program.DefDecl}
  {bodies : Effect4.Program.Effs Op} {layers : Effect4.Program.LayerTerms Op}
  {history : List (Prod (List Nat) (Effect4.Program.LayerTerm Op))},
  Eq root.hoistAll (Except.ok { fst := main, snd := history }) →
    Eq main.block?
        (Option.some
          { fst := defs, snd := { fst := bodies, snd := { fst := body, snd := layers } } }) →
      ∀ {classDecls : List TypeScript.ClassDecl},
        Eq (Effect4.Codegen.Classes.readClassDecls classDecls) (Option.some classes) →
          (∀ (d : Effect4.Program.DefDecl),
              List.instMembership.mem defs d → Eq d.readable Bool.true) →
            (∀ (p : Prod Effect4.Program.DefDecl (Effect4.Program.Eff Op)),
                List.instMembership.mem (defs.zip bodies.toList) p →
                  Effect4.Program.ReadsBack classes ((sig.withDefs defs).withParams p.fst.params)
                    (Effect4.Program.paramsSpell param p.fst.params
                      (Effect4.Program.defsSpell call defs spell))
                    1 p.snd) →
              Effect4.Program.ReadsBack classes (sig.withDefs defs)
                  (Effect4.Program.defsSpell call defs spell) 0 body →
                (∀ (l : Effect4.Program.LayerTerm Op),
                    List.instMembership.mem layers.toList l →
                      Effect4.Program.LayerTerm.ReadsBack classes (sig.withDefs defs)
                        (Effect4.Program.defsSpell call defs spell) l) →
                  (∀ (k : Nat),
                      instLTNat.lt k layers.toList.length →
                        Eq
                          (Effect4.Program.LayerTerm.readRefName
                            (Effect4.Program.LayerTerm.refName (Effect4.Program.Path.layerPath k)))
                          (Option.some (Effect4.Program.Path.layerPath k))) →
                    (∀ (entry : Prod (List Nat) (Effect4.Program.LayerTerm Op)),
                        List.instMembership.mem history entry →
                          ∀ (d : Effect4.Program.DefDecl),
                            Eq (Effect4.Program.bodyDeclOf defs entry.fst) (Option.some d) →
                              Effect4.Program.LayerTerm.ReadsBack classes
                                ((sig.withDefs defs).withParams d.params)
                                (Effect4.Program.paramsSpell param d.params
                                  (Effect4.Program.defsSpell call defs spell))
                                entry.snd) →
                      (∀ (entry : Prod (List Nat) (Effect4.Program.LayerTerm Op)),
                          List.instMembership.mem history entry →
                            Eq (Effect4.Program.bodyDeclOf defs entry.fst) Option.none →
                              Effect4.Program.LayerTerm.ReadsBack classes (sig.withDefs defs)
                                (Effect4.Program.defsSpell call defs spell) entry.snd) →
                        (∀ (entry : Prod (List Nat) (Effect4.Program.LayerTerm Op)),
                            List.instMembership.mem history entry →
                              Eq
                                (Effect4.Program.LayerTerm.readRefName
                                  (Effect4.Program.LayerTerm.refName entry.fst))
                                (Option.some entry.fst)) →
                          ∀ {name : String} {ty : Effect4.Program.EffTy}
                            {decls : List TypeScript.ConstDecl},
                            Eq (Effect4.Program.printModule sig name ty root) (Except.ok decls) →
                              Eq
                                (Effect4.Program.readModule sig spell call param
                                  (instHAppendOfAppend.hAppend
                                    (List.map TypeScript.Decl.classDecl classDecls)
                                    (List.map TypeScript.Decl.const decls)))
                                (Except.ok root)

modeled-codecclaim:modeled-codec

A modeled value survives JSON and back at the normal form of its type, under codec admission at the value (Ty.isCodecValue): decoding its encoding and reading the value back answers the value; admission stays a premise, since a natural above 2^53 inhabits nat and has no exact JSON image; no TypeScript codec and no target execution (decisions row 330, slice L1)

The JSON round trip of a modeled value (claim modeled-codec), at the normal form of its type. Membership comes from Modeled.member and hasTy_normalize. Codec admission stays a premise: it is value-specific, and a natural above 2^53 has no exact JSON image.

Module

Effect4.Laws.Schema.Modeled

∀ (α : Type) [m : Effect4.Schema.Modeled α] (a : α),
  Eq
      ((Effect4.Program.CTy.ofRaw (m.ty α)).toRaw.isCodecValue
        ((Effect4.Schema.Modeled.image α).toVal a))
      Bool.true →
    Eq
      (((Effect4.Schema.encode (Effect4.Program.CTy.ofRaw (m.ty α)).toRaw
                ((Effect4.Schema.Modeled.image α).toVal a)).bind
            (Effect4.Schema.decode (Effect4.Program.CTy.ofRaw (m.ty α)).toRaw)).bind
        (Effect4.Schema.Modeled.image α).ofVal)
      (Option.some a)

record-field-lawsclaim:record-field-laws

A field reference is a lens on the record frame: for a record with ascending names, at every identity context, the machine's read at the reference's name reads the field's encoding, and its overwrite at that name writes the record the reference's write gives (FieldRef.frame_laws); on carriers the reference is a lawful lens whose writes at two positions commute; nothing of an optional field (decisions row 330, slice L2)

The record frame's field laws (claim record-field-laws): for a record with ascending names, the machine's read at a reference's name reads the field's encoding, and its overwrite at that name writes the record that the reference's write gives.

Module

Effect4.Laws.Schema.FieldRef

∀ {L : Effect4.Schema.Model.Leaves} {fs : List (Prod String (Prod Bool Effect4.Program.Ty))}
  {t : Effect4.Program.Ty},
  Effect4.Field.Ascending Effect4.Field.bytesKey fs →
    ∀ (f : Effect4.Schema.FieldRef fs t)
      (x : Effect4.Schema.Model.CarrierAt L (Effect4.Program.Ty.record fs))
      (v : Effect4.Schema.Model.CarrierAt L t),
      And
        (Eq
          (Effect4.Machine.Record.read Bool.false
            ((Effect4.Schema.Model.imageAt L (Effect4.Program.Ty.record fs)).toVal x) f.name)
          (Option.some ((Effect4.Schema.Model.imageAt L t).toVal (f.get x))))
        (Eq
          (Effect4.Machine.Record.set
            ((Effect4.Schema.Model.imageAt L (Effect4.Program.Ty.record fs)).toVal x) f.name
            ((Effect4.Schema.Model.imageAt L t).toVal v))
          (Option.some
            ((Effect4.Schema.Model.imageAt L (Effect4.Program.Ty.record fs)).toVal (f.set x v))))