dev.idiolect.defs

Shared types for the dev.idiolect.* lexicon family. Two kinds of content live here:

  • Cross-cutting reference shapes — lens, schema, encounter, vocab, and strong-record references; tool identity; visibility.
  • Content-theory types — purpose, lens property, evidence, caveat, basis. Shared across multiple records.

Record-specific combinator trees (condition, eligibility, constraint, convention) live in their respective record lexicons, not here.

Source: lexicons/dev/idiolect/defs.json · Rust: idiolect_records::generated::defs · TS: @idiolect-dev/schema/defs

Reference shapes

schemaRef

Reference to a schema. Either an at-uri or a content hash; at least one must be present.

SubfieldTypeNotes
uriat-uriAT-URI pointing to a schema record.
cidcid-linkContent hash of the schema.
languagestringSchema-language identifier (atproto-lexicon, postgres-sql, protobuf, graphql, json-schema).

lensRef

SubfieldTypeNotes
uriat-uriAT-URI of a lens record.
cidcid-linkContent hash of the lens.
directionenumunidirectional / bidirectional.

encounterRef

SubfieldTypeNotes
uriat-uri (required)AT-URI of the encounter.
cidcid-linkOptional CID for revision pinning.

vocabRef

SubfieldTypeNotes
uriat-uriAT-URI of a vocab record.
cidcid-linkContent hash pinning a specific vocab revision.

strongRecordRef

SubfieldTypeRequiredNotes
uriat-uriyesAT-URI of the referenced record.
cidcid-linkyesContent hash.

Parallel to com.atproto.repo.strongRef. Repeated here so the defs tree is self-contained.

tool

SubfieldTypeRequiredNotes
namestringyesCanonical tool name (panproto, coq, tlaplus, z3, nextest).
versionstringyesVersion string.
commitstringnoOptional source commit or build identifier.

visibility

A closed-enum string. Five values:

ValueMeaning
public-detailedFull record body published.
public-minimalRecord published with elided detail (e.g. omits source instance).
public-aggregate-onlyRecord consumed only by aggregators; individual reads suppressed.
community-scopedReserved for v1 substrate enforcement; should not be served to parties outside the named community once enforcement lands.
privateShould not be published at all.

The substrate does not enforce these today; they are policy hints.

Content-theory types

use

The compound "what was done, on what material, for what end, by which actor" tuple, reused across records whose subject is an action performed, desired, endorsed, or prohibited.

SubfieldTypeRequiredNotes
actionstring (≤256)yesAction identifier, resolved against actionVocabulary.
materialmaterialSpecnoWhat is being acted on.
purposestring (≤256)noThe end the action serves.
actorstring (≤256)noWho performs or benefits.
actionVocabularyvocabRefnoVocab the action slug resolves against.
purposeVocabularyvocabRefnoVocab the purpose slug resolves against.

materialSpec

SubfieldTypeNotes
scopestring (≤256)Community-defined scope (classroom_materials, production_logs, scraped_corpus).
uriuriOptional pointer to a specific dataset.

lensProperty

A union covering the seven verification kinds. Each verification record carries one of these as its property field.

VariantUsed by
lpRoundtripkind: roundtrip-test
lpGeneratorkind: property-test
lpTheoremkind: formal-proof
lpConformancekind: conformance-test
lpCheckerkind: static-check
lpConvergencekind: convergence-preserving
lpCoercionLawkind: coercion-law

lpRoundtrip

SubfieldTypeRequiredNotes
domainstring (≤512)yesSymbolic description of the input set.
generatorurinoOptional pointer to a generator that enumerates the domain.

lpGenerator

SubfieldTypeRequiredNotes
specstring (≤2000)yesGenerator specification (proptest Strategy reference, Hypothesis strategy, QuickCheck Arbitrary).
runnerstringnoName of the PBT runtime.
seedintegernoOptional seed for reproducibility.

lpTheorem

SubfieldTypeRequiredNotes
statementstring (≤4000)yesThe theorem, in the declared system syntax.
systemstringnoProof system (coq, lean4, agda, tlaplus, z3).
freeVariablesarray of stringsnoNames of free variables.

lpConformance

SubfieldTypeRequiredNotes
standardstringyesStandard identifier (iso-8601, rfc-3339, en-pos-v2.1).
versionstringyesStandard version.
clausesarray of stringsnoOptional subset of the standard's clauses.

lpChecker

SubfieldTypeRequiredNotes
checkerstringyesStatic-checker identifier (panproto-check, clippy, tsc-strict).
rulesetstringnoNamed ruleset or configuration preset.
versionstringnoChecker version.

lpConvergence

SubfieldTypeRequiredNotes
propertystring (≤1000)yesSymbolic name or description of the preserved property.
boundStepsintegernoOptional bound on steps to fixpoint.

lpCoercionLaw

SubfieldTypeRequiredNotes
standardstring (≤256)yesIdentifier of the coercion-law standard.
versionstring (≤64)noOptional version.
violationThresholdintegernoCap on the violations a runner may report before falsifying.

evidence

A union of structured witnesses for retrospection findings.

VariantUsed when finding kind is
evidenceDivergencemerge-divergence
evidenceLossdata-loss
evidenceMismatchreconciliation-mismatch

evidenceDivergence

SubfieldTypeRequiredNotes
pathAarray of lensRefyesLenses composed in path A.
pathBarray of lensRefyesLenses composed in path B.
witnessInputcid-linknoOptional CID where the two paths diverge.

evidenceLoss

SubfieldTypeRequiredNotes
sourceFieldstringyesDotted path identifying the lost field.
targetSchemaschemaRefnoTarget schema where the loss was observed.
witnessInputcid-linknoWitness input.

evidenceMismatch

SubfieldTypeRequiredNotes
leftRecordcid-linknoLeft record.
rightRecordcid-linknoRight record.
expectedEqualityOnstringnoDotted path or projection under which equality was expected.

caveat

SubfieldTypeRequiredNotes
modestringyesShort failure-mode identifier.
affectsarray of stringsnoDotted paths or field names.
severityenumnoinfo / warn / error.

basis

A union of structured grounds for an attitudinal claim.

VariantUse when
basisSelfAssertedThe holder asserts directly. The default when basis is omitted.
basisCommunityPolicyGrounded in a community's published policy. Carries community (at-uri) and optional policyUri.
basisExternalSignalGrounded in something outside ATProto. Carries url, optional signalType, optional description.
basisDerivedFromRecordGrounded in another ATProto record. Carries source (strongRecordRef) and optional inferenceRule.

basisSelfAsserted has no fields; the variant tag itself is the content. basisDerivedFromRecord.inferenceRule is the canonical hook for declaring how this record derives from another (classifier:purpose-v1, lens:v1-to-v2, aggregation:byte-mean, ...).

Concept references