docs(adr): amend ADR-0004 to ADR-0007 for the Go SDK

The review of #1070 found four ADRs whose text the Go SDK design leaves
wrong. Each gets a dated amendment, and each amendment names the
principle it rests on, so a reader can trace the change back.

ADR-0007 gains the binding and language SDK words, the rule that a field
crosses the binding only with its value, the record fixture as the proof
of the lowering, the generator checking declarations with the embedded
guest so the engine's rules have one source, and the fact that the guest
takes one plan in one call. The value exports stay for another host of
the guest and are not a Go path.

ADR-0005 decision 4 named bindings/go, stackencrypt and stackauth. The
module is at languages/golang and the packages are encrypt and auth.

ADR-0006 said the Go binding has a Label held to Rust's by a fixture.
The Go SDK has no Label: the segments come from the context= tag and
the field name, and the engine's own parser checks them at go generate.
The Go half of the fixture is retired with the Go Label.

ADR-0004 decision 5 is convention in Rust and structural in Go, because
Go has no standalone term derivation. Decision 6's plan-versus-value
check moves to go generate for Go, with the engine's check as backstop.

Claude-Session: https://claude.ai/code/session_014jiJy4WhYH2LXojK2jSoxi

Author: auxesis

packages/stack-encrypt/docs/adr/0004-one-context-per-target-threaded-through-the-declaration-tree.md

@@ -315,3 +315,32 @@ What it does **not** fix: a term and a ciphertext written through two separate
 top-level calls still have no relation to each other, because neither knows the
 other exists. Decision 5 narrows this to callers who deliberately bypass the
 target layer on the write side.
+
+## Amended 2026-10-06 (#1070)
+
+G1 to G8 and Go-1 to Go-13 name the principles in
+`docs/sdk-design-principles.md`, general and Go.
+
+Two decisions change shape in the Go SDK and keep their substance.
+
+**Decision 5** keeps standalone term derivation as the query path and directs
+a stored term to a target, by convention and documentation, because the term
+methods cannot tell a probe from a stored term. In Go the rule is structural.
+The Go SDK has no `Cipher.Term`. A stored term exists only in generated code,
+beside its ciphertext, under the one context the declaration gives the field.
+A probe comes from a field entry's query method, which exists only for an
+index the field declares. The compiler refuses a query the field does not
+declare (G4: one declaration serves the write, the query and the read; Go-2:
+the caller reaches every output through a field).
+
+**Decision 6** puts the plan-versus-value check at the FFI boundary, as plan
+validation, with the field named and before any key is requested. In Go that
+check moves earlier. `stashgen` checks the Go type against the declaration at
+`go generate`, by running the guest the SDK embeds, so a field type the engine
+cannot seal or an index that does not fit stops the generator. The engine's
+own check at the boundary stays as the backstop (G3: the earliest stage the
+language allows; Go-1). The dynamic-to-static dispatch itself is unchanged.
+
+Decisions 1 to 4, 7 and 8 do not change. Decision 2's `extend` is what
+`Cipher.Extend` does from Go: a caller's context appends to the declared one,
+and never replaces it.

packages/stack-encrypt/docs/adr/0005-a-separate-credential-guest-for-the-profile-and-auth.md

@@ -248,3 +248,22 @@ crypto guest. A binary that encrypts now carries both guests. Neither
 sandbox changes. The crypto guest still has no environment and no
 filesystem, and the credential guest still has one mount. With no profile
 directory, `stackauth.OpenWithoutProfile` gives it none.
+
+## Amendment (2026-10-06, #1070): the module at `languages/golang`, the packages `encrypt` and `auth`
+
+G1 to G8 and Go-1 to Go-13 name the principles in
+`docs/sdk-design-principles.md`, general and Go.
+
+Decision 4 named the module `bindings/go` and the packages `stackencrypt` and
+`stackauth`. The module is at `languages/golang`, beside the other language
+SDKs, and the packages are `encrypt` and `auth`.
+
+The reason is Go-13: a name says what the thing is for, and no name repeats
+its package. Go code reads a package name at every use. `encrypt.Cipher` and
+`auth.ProfileStore` say what they are; `stackencrypt.Cipher` repeats the
+module's name on every line. ADR-0008 names the user-facing code the Go SDK,
+not the Go binding, so the directory is not `bindings`.
+
+Everything else in decision 4 holds: one module, one internal package both
+import, `auth` does not import `encrypt`, and `ClientKey` is one type under
+both names. The 2026-09-27 amendment holds too: `encrypt` imports `auth`.

packages/stack-encrypt/docs/adr/0006-descriptors-render-with-a-slash-and-describe-is-open.md

@@ -119,3 +119,25 @@ part and otherwise the field name is used; a nested record is an ordinary typed
 field sealed under `<context>/<field>`, its inner layout being its own type's
 business. The struct-level `context = "<prefix>"` form and the rest of this
 decision are unchanged.
+
+## Amended 2026-10-06 (#1070)
+
+G1 to G8 and Go-1 to Go-13 name the principles in
+`docs/sdk-design-principles.md`, general and Go.
+
+The `Label` decision said the Go binding has the same type and the same
+segment rule, held together by one fixture both test suites read. The Go SDK
+has no `Label`, `Context`, `NewContext` or `ParseLabel`. A field's two
+segments are the value of the struct's `context=` tag and the field's name
+(Go-7: the user never sees the plan, and no call takes a context, G4).
+
+The segment rule has one implementation. `stashgen` checks a declaration by
+running the guest the SDK embeds (ADR-0007, amended), so a `/` or an escaped
+character in a `context=` value is refused at `go generate` by the engine's
+own `Label` parser (G1, Go-1). The Go half of the fixture is retired with the
+Go `Label`; the Rust half stays, and the record fixture in ADR-0007 covers the
+bytes Go and Rust must agree on.
+
+The derive's `struct = .., context = "<prefix>"` form and the Go tag bind the
+same pair, so a row the derive writes opens through the Go SDK and the
+reverse. That is the interoperability this ADR was for.

packages/stack-encrypt/docs/adr/0007-bindings-enter-through-a-plan-never-a-second-executor.md

@@ -11,6 +11,11 @@ extends: ADR-0003, ADR-0004
 > (after its grammar is narrowed to the plan's), how EQL types are assembled
 > (per language, from standard outputs), and the consequence that the EQL
 > encoding lives twice.
+>
+> **Amended 2026-10-06**, by #1070. The decision is unchanged. Amended: the
+> words binding and language SDK, what crosses the binding from Go, the proof
+> of the lowering, where the generator gets the engine's rules, and what the
+> guest takes in one call.
 
 Stack Encrypt has one execution engine: the `Encryption` and `Decryption`
 descriptions in `target/` and the batched `Pending` they produce. ADR-0003
@@ -111,3 +116,50 @@ Option 3.
 
 The design history, the names rejected on the way and the sequencing are in
 `docs/plans/2026-10-04-plan-builder.md`.
+
+## Amended 2026-10-06 (#1070)
+
+G1 to G8 and Go-1 to Go-13 name the principles in
+`docs/sdk-design-principles.md`, general and Go.
+
+ADR-0008 fixes two words this ADR used as one. A **binding** is the WASI or
+FFI interface between the engine and a language: the guest's exports and the
+data that crosses them. A **language SDK** is what users of that language work
+with. The decision above is about the binding: a plan is the one thing that
+crosses it. The Go SDK is struct tags, a generator and generated code, and its
+users never see a plan (Go-7). Each "binding" above that names Go reads as the
+Go SDK's generated code.
+
+**A field crosses the binding only when its value does.** The first Go design
+sent the full declaration and skipped passthrough values, which contradicted
+decision 9 of the plan: every plan field is present in the value. Generated Go
+code now sends a declaration and a value for each sealed and each indexed
+field, and nothing for a passthrough or omitted field. The data grammar does
+not change. The generated file still names every field, so a reviewer reads
+the whole declaration (G1, Go-10).
+
+**The record fixture is the proof of the lowering.** Sequencing rested on Go's
+`plantest.Golden` snapshots not changing, and the Go SDK removes the package
+that writes them. The proof is now a fixture both test suites read: the Rust
+chain and the lowering each open the records that the other encrypted, and
+both derive the same bytes for each term. The same fixture later holds
+generated Go code to the Rust chain (G7: a claim is run before it is written).
+
+**The generator asks the engine, and holds no copy of its rules.** `stashgen`
+refuses an index that does not fit a Go type and an EQL type the engine cannot
+produce. A second copy of those rules in Go would be the "lives twice" cost
+this ADR accepts only for an encoder. `stashgen` runs the guest the SDK embeds
+to check each declaration at `go generate`, so the rules have one source (G1)
+and the check runs at the earliest stage Go allows (G3, Go-1).
+
+**The guest takes one plan in one call.** `se_encrypt_record` takes one plan,
+and the engine runs one plan under one key request. So one Go call covers one
+type, and one request for several types is later work: the engine runs several
+plans under one key request, then a guest export takes several plans with
+their values. G5 allows an SDK to put several types in one request; it does
+not require it before the engine can.
+
+**The guest's value exports have no caller in Go.** The Go SDK seals a whole
+value through a declaration (ADR-0008), so `se_encrypt`, `se_decrypt` and the
+element exports have no Go caller. They stay while another host of the guest
+may need them; they are not a Go path.