module Observe.Interchange import Data.UTF8 import Model.Word32 import Std.Byte import Std.Flag import Data.JSON import Data.JSONAccess import Observe.Value import Std.Natural -- AOS-JSON/1 RECORDS (docs/standards/AOS-1.0-draft-1.md §24): one line of a -- stream -- a header, descriptor, event, artifact, coverage or footer -- record, or a record of a type this reader does not know (retained and -- skipped, AOS-JSON-003) -- and the verdict code that says whether it is a -- valid record and, if not, the first rule it breaks. -- -- THE CODES ARE A CONTRACT (docs/observability/README.md §"Validation -- contract"): the bootstrap tool's reader (tool/Aos.hs `LineCode`) returns -- the same number for the same line, and scripts/ci/observability.sh holds -- the two to it on every fixture. Never renumber one. -- -- 0 valid 1 json 2 duplicate-key 3 limit -- 4 not-object 5 format 6 type 7 missing-field -- 8 integer 9 identity 10 value 11 availability -- 12 enum 13 field-type 14 required-extension -- -- The checks run in a fixed order and the first that fails decides the -- code; the order is part of the contract. family AosLine : Type 0 constructor AosLineInvalid field unrestricted aosLineInvalidCode : Nat constructor AosLineValid field unrestricted aosLineRecord : (family JSON) end-family -- The limits every AOS-JSON/1 stream declares in its header (a line of -- 1 MiB, 64 levels, a string of 256 KiB, 65,536 members), stated with -- Data.JSON's bounds. def aosLimits : (family JSONLimits) = (constructor JSONLimits JSONLimitsValue (constructor JSONBound JSONBoundAtMost 1048576) (constructor JSONBound JSONBoundAtMost 64) (constructor JSONBound JSONBoundAtMost 262144) (constructor JSONBound JSONBoundAtMost 1024) (constructor JSONBound JSONBoundAtMost 65536) (constructor JSONBound JSONBoundBelowTwoPower 24)) -- a parse failure's code: a duplicate name 2, a limit 3, anything else 1 def aosParseErrorCode = (lambda unrestricted error : (family JSONErrorCode) . (eliminate JSONErrorCode (lambda unrestricted current : (family JSONErrorCode) . Nat) error (branch JSONInvalidUTF8 . 1) (branch JSONUnexpectedEnd . 1) (branch JSONTrailingBytes . 1) (branch JSONInvalidValue . 1) (branch JSONObjectKeyNotString . 1) (branch JSONObjectColonMissing . 1) (branch JSONObjectDelimiterMissing . 1) (branch JSONObjectDuplicateKey . 2) (branch JSONArrayDelimiterMissing . 1) (branch JSONStringUnterminated . 1) (branch JSONStringControlCharacter . 1) (branch JSONEscapeInvalid . 1) (branch JSONUnicodeEscapeInvalid . 1) (branch JSONUnicodeLowWithoutHigh . 1) (branch JSONUnicodeHighWithoutLow . 1) (branch JSONNumberIntegerInvalid . 1) (branch JSONNumberFractionDigitsMissing . 1) (branch JSONNumberExponentDigitsMissing . 1) (branch JSONExpectedObject . 1) (branch JSONMissingMember . 1) (branch JSONDuplicateMember . 2) (branch JSONExpectedString . 1) (branch JSONExpectedArray . 1) (branch JSONExpectedNumber . 1) (branch JSONExpectedInteger . 1) (branch JSONExpectedBoolean . 1) (branch JSONExpectedNull . 1) (branch JSONInputLimitExceeded . 3) (branch JSONDepthLimitExceeded . 3) (branch JSONStringLimitExceeded . 3) (branch JSONNumberLimitExceeded . 3) (branch JSONContainerLimitExceeded . 3) (branch JSONOutputLimitExceeded . 3) (branch JSONNumericRangeUnsupported . 1) (branch JSONMalformedTree . 1))) -- --------------------------------------------------------------------------- -- Field rules (each 0 when it holds, else its code) def aosTextCode = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (naturalSelect (naturalIsZero (aosHas name value)) 7 (naturalSelect (naturalIsZero (aosMemberIsString name value)) 13 0)))) def aosNonEmptyTextCode = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (aosThen (aosTextCode name value) (naturalSelect (naturalIsZero (bytes-length (aosMemberBytes name value))) 13 0)))) def aosIdentityCode = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (naturalSelect (naturalIsZero (aosHas name value)) 7 (naturalSelect (naturalAnd (aosMemberIsString name value) (aosIsIdentity (aosMemberBytes name value))) 0 9)))) def aosU64Code = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (naturalSelect (naturalIsZero (aosHas name value)) 7 (naturalSelect (naturalAnd (aosMemberIsString name value) (aosIsU64Text (aosMemberBytes name value))) 0 8)))) def aosObjectCode = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (naturalSelect (naturalIsZero (aosHas name value)) 7 (naturalSelect (aosIsObject (aosMemberValue name value)) 0 13)))) def aosBooleanCode = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (naturalSelect (naturalIsZero (aosHas name value)) 7 (naturalSelect (aosIsBoolean (aosMemberValue name value)) 0 13)))) -- 1 when every element of an array is a string (1 for a chain's end) def aosArrayAllStrings = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . 0) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . 0) (branch JSONArray values valuesInduction . valuesInduction) (branch JSONArrayEnd . 1) (branch JSONArrayNext head tail headInduction tailInduction . (naturalAnd (aosIsString head) tailInduction)) (branch JSONString text . 0) (branch JSONNumber digits . 0) (branch JSONBoolean flag . 0) (branch JSONNull . 0))) def aosStringArrayCode = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (naturalSelect (naturalIsZero (aosHas name value)) 7 (let unrestricted member = (aosMemberValue name value) in (naturalSelect (naturalAnd (aosIsArray member) (aosArrayAllStrings member)) 0 13))))) def aosArrayIsEmpty = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . 0) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . 0) (branch JSONArray values valuesInduction . valuesInduction) (branch JSONArrayEnd . 1) (branch JSONArrayNext head tail headInduction tailInduction . 0) (branch JSONString text . 0) (branch JSONNumber digits . 0) (branch JSONBoolean flag . 0) (branch JSONNull . 0))) -- A required feature is interpretable only with its structural AND stream -- state handlers. Unknown requirements continue to refuse full validation. def aosKnownRequirements = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . 0) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . 0) (branch JSONArray values valuesInduction . valuesInduction) (branch JSONArrayEnd . 1) (branch JSONArrayNext head tail headInduction tailInduction . (naturalAnd headInduction tailInduction)) (branch JSONString text . (bytes-equal text b"aos.coverage.cumulative@1")) (branch JSONNumber digits . 0) (branch JSONBoolean flag . 0) (branch JSONNull . 0))) def aosContainsCumulativeRequirement = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . 0) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . 0) (branch JSONArray values valuesInduction . valuesInduction) (branch JSONArrayEnd . 0) (branch JSONArrayNext head tail headInduction tailInduction . (naturalOr headInduction tailInduction)) (branch JSONString text . (bytes-equal text b"aos.coverage.cumulative@1")) (branch JSONNumber digits . 0) (branch JSONBoolean flag . 0) (branch JSONNull . 0))) def aosCriticalExtensionCode = (lambda unrestricted record : (family JSON) . (naturalSelect (aosHas b"required_extensions" record) (aosThen (aosStringArrayCode b"required_extensions" record) (naturalSelect (aosKnownRequirements (aosMemberValue b"required_extensions" record)) 0 14)) 0)) -- 0 when the member (a present string) is one of the names, else 12 def aosEnumCode = (lambda unrestricted found : Nat . (naturalSelect found 0 12)) -- an availability slot (AOS-JSON-006): {state: present, value} with the -- present value's own rule, or a non-present state, an optional structured -- reason, and no value def aosSlotCode = (lambda unrestricted slot : (family JSON) . (lambda unrestricted present : (pi unrestricted value : (family JSON) . Nat) . (let unrestricted state = (aosMemberBytes b"state" slot) in (naturalSelect (naturalIsZero (aosMemberIsString b"state" slot)) 11 (naturalSelect (bytes-equal state b"present") (naturalSelect (aosHasExactly2 b"state" b"value" slot) (present (aosMemberValue b"value" slot)) 11) (naturalSelect (aosIsAbsenceState state) (naturalSelect (aosHasExactly1 b"state" slot) 0 (naturalSelect (aosHasExactly2 b"state" b"reason" slot) (naturalSelect (aosIsObject (aosMemberValue b"reason" slot)) 0 11) 11)) 11)))))) -- a present time: exactly clock_id, clock_epoch and ticks def aosTimeCode = (lambda unrestricted value : (family JSON) . (naturalSelect (aosHasExactly3 b"clock_id" b"clock_epoch" b"ticks" value) (aosThen (aosIdentityCode b"clock_id" value) (aosThen (aosIdentityCode b"clock_epoch" value) (aosU64Code b"ticks" value))) 11)) -- a present context: exactly id def aosContextCode = (lambda unrestricted value : (family JSON) . (naturalSelect (aosHasExactly1 b"id" value) (aosIdentityCode b"id" value) 11)) def aosValueCode = (lambda unrestricted value : (family JSON) . (naturalSelect (aosIsValue value) 0 10)) -- a payload member: a tagged value, or an availability slot of one def aosPayloadMemberCode = (lambda unrestricted member : (family JSON) . (naturalSelect (aosHas b"t" member) (aosValueCode member) (naturalSelect (aosHas b"state" member) (aosSlotCode member aosValueCode) 10))) -- every payload member, in order: the first failure's code def aosPayloadCode = (lambda unrestricted payload : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) payload (branch JSONObject members membersInduction . membersInduction) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . (aosThen (aosPayloadMemberCode member) tailInduction)) (branch JSONArray values valuesInduction . 0) (branch JSONArrayEnd . 0) (branch JSONArrayNext head tail headInduction tailInduction . 0) (branch JSONString text . 0) (branch JSONNumber digits . 0) (branch JSONBoolean flag . 0) (branch JSONNull . 0))) def aosIsRecordClass = (lambda unrestricted text : Bytes . (naturalOr (bytes-equal text b"event") (naturalOr (bytes-equal text b"diagnostic") (naturalOr (bytes-equal text b"activity") (naturalOr (bytes-equal text b"state") (naturalOr (bytes-equal text b"metric") (naturalOr (bytes-equal text b"relation") (naturalOr (bytes-equal text b"artifact") (naturalOr (bytes-equal text b"receipt") (naturalOr (bytes-equal text b"descriptor") (bytes-equal text b"capture-control"))))))))))) def aosIsOriginKind = (lambda unrestricted text : Bytes . (naturalOr (bytes-equal text b"direct") (naturalOr (bytes-equal text b"reported") (naturalOr (bytes-equal text b"derived") (naturalOr (bytes-equal text b"simulated") (bytes-equal text b"estimated")))))) -- --------------------------------------------------------------------------- -- Records def aosHeaderCode = (lambda unrestricted record : (family JSON) . (aosThen (aosNonEmptyTextCode b"aos_version" record) (aosThen (aosIdentityCode b"bundle_id" record) (aosThen (aosNonEmptyTextCode b"exporter" record) (aosStringArrayCode b"required_extensions" record))))) def aosDescriptorCode = (lambda unrestricted record : (family JSON) . (aosThen (aosNonEmptyTextCode b"descriptor_id" record) (aosThen (naturalSelect (naturalLessOrEqual (bytes-length (aosMemberBytes b"descriptor_id" record)) 256) 0 13) (aosThen (aosNonEmptyTextCode b"kind" record) (aosObjectCode b"body" record))))) def aosEventCode = (lambda unrestricted record : (family JSON) . (let unrestricted identity = (aosMemberValue b"event_id" record) in (let unrestricted origin = (aosMemberValue b"origin" record) in (aosThen (aosNonEmptyTextCode b"aos_version" record) (aosThen (aosObjectCode b"event_id" record) (aosThen (aosIdentityCode b"attempt_id" identity) (aosThen (aosIdentityCode b"producer_id" identity) (aosThen (aosIdentityCode b"producer_epoch" identity) (aosThen (aosU64Code b"sequence" identity) (aosThen (aosNonEmptyTextCode b"schema_id" record) (aosThen (aosTextCode b"record_class" record) (aosThen (aosEnumCode (aosIsRecordClass (aosMemberBytes b"record_class" record))) (aosThen (aosIdentityCode b"policy_id" record) (aosThen (aosObjectCode b"origin" record) (aosThen (aosTextCode b"kind" origin) (aosThen (aosEnumCode (aosIsOriginKind (aosMemberBytes b"kind" origin))) (aosThen (naturalSelect (aosHas b"time" record) 0 7) (aosThen (aosSlotCode (aosMemberValue b"time" record) aosTimeCode) (aosThen (naturalSelect (aosHas b"context" record) 0 7) (aosThen (aosSlotCode (aosMemberValue b"context" record) aosContextCode) (aosThen (aosObjectCode b"payload" record) (aosThen (aosPayloadCode (aosMemberValue b"payload" record)) (aosThen (naturalSelect (aosHas b"extensions" record) (naturalSelect (aosIsArray (aosMemberValue b"extensions" record)) 0 13) 7) (aosStringArrayCode b"required_extensions" record)))))))))))))))))))))))) -- `input` begins with `prefix` def aosHasPrefix = (lambda unrestricted prefix : Bytes . (lambda unrestricted input : Bytes . (app (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted rest : Bytes . Nat)) (lambda unrestricted rest : Bytes . 1) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : (pi unrestricted rest : Bytes . Nat) . (lambda unrestricted rest : Bytes . (naturalAnd (naturalNonzero (bytes-length rest)) (naturalAnd (byte-equal head (bytes-head rest)) (induction (bytes-tail rest)))))))) prefix) input))) -- `input` without its first `count` bytes def aosDropBytes = (lambda unrestricted count : Nat . (lambda unrestricted input : Bytes . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted rest : Bytes . Bytes)) (lambda unrestricted rest : Bytes . rest) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted rest : Bytes . Bytes) . (lambda unrestricted rest : Bytes . (induction (bytes-tail rest))))) count) input))) -- `sha256:` then 64 lowercase hex digits def aosIsArtifactIdentity = (lambda unrestricted text : Bytes . (naturalAnd (aosHasPrefix b"sha256:" text) (aosIsHexOfWidth 64 (aosDropBytes 7 text)))) def aosIsPublicationState = (lambda unrestricted text : Bytes . (naturalOr (bytes-equal text b"requested") (naturalOr (bytes-equal text b"writing") (naturalOr (bytes-equal text b"complete") (naturalOr (bytes-equal text b"verified") (bytes-equal text b"published")))))) def aosArtifactCode = (lambda unrestricted record : (family JSON) . (aosThen (aosTextCode b"artifact_id" record) (aosThen (naturalSelect (aosIsArtifactIdentity (aosMemberBytes b"artifact_id" record)) 0 9) (aosThen (aosNonEmptyTextCode b"media" record) (aosThen (aosU64Code b"logical_size" record) (aosThen (aosTextCode b"state" record) (aosThen (aosEnumCode (aosIsPublicationState (aosMemberBytes b"state" record))) (aosIdentityCode b"attempt_id" record)))))))) -- A cumulative snapshot is exact and must announce its critical semantics -- on the record itself, so an older line reader cannot silently add totals. def aosCoverageModeCode = (lambda unrestricted record : (family JSON) . (naturalSelect (aosHas b"coverage_mode" record) (naturalSelect (naturalAnd (aosMemberIsString b"coverage_mode" record) (naturalAnd (bytes-equal (aosMemberBytes b"coverage_mode" record) b"cumulative") (naturalAnd (aosBooleanFlag (aosMemberValue b"dropped_exact" record)) (naturalAnd (aosIsArray (aosMemberValue b"required_extensions" record)) (aosContainsCumulativeRequirement (aosMemberValue b"required_extensions" record)))))) 0 12) 0)) def aosCoverageCode = (lambda unrestricted record : (family JSON) . (aosThen (aosIdentityCode b"attempt_id" record) (aosThen (aosIdentityCode b"producer_id" record) (aosThen (aosIdentityCode b"producer_epoch" record) (aosThen (aosU64Code b"next_sequence" record) (aosThen (aosU64Code b"records_accepted" record) (aosThen (aosU64Code b"records_dropped" record) (aosThen (aosU64Code b"records_excluded" record) (aosThen (aosBooleanCode b"dropped_exact" record) (aosCoverageModeCode record)))))))))) def aosIsTermination = (lambda unrestricted text : Bytes . (naturalOr (bytes-equal text b"clean") (naturalOr (bytes-equal text b"error") (bytes-equal text b"interrupted")))) def aosFooterCode = (lambda unrestricted record : (family JSON) . (aosThen (aosU64Code b"records" record) (aosThen (aosTextCode b"termination" record) (aosThen (aosEnumCode (aosIsTermination (aosMemberBytes b"termination" record))) (aosThen (aosBooleanCode b"complete" record) (aosStringArrayCode b"omissions" record)))))) -- a parsed line's code: an object with the right format and a string type, -- then its type's rules (an unknown type is valid and skipped) def aosRecordCode = (lambda unrestricted record : (family JSON) . (let unrestricted kind = (aosMemberBytes b"type" record) in (naturalSelect (naturalIsZero (aosIsObject record)) 4 (aosThen (naturalSelect (naturalAnd (aosMemberIsString b"format" record) (bytes-equal (aosMemberBytes b"format" record) b"AOS-JSON/1")) 0 5) (aosThen (naturalSelect (aosMemberIsString b"type" record) 0 6) (aosThen (naturalSelect (bytes-equal kind b"header") (aosHeaderCode record) (naturalSelect (bytes-equal kind b"descriptor") (aosDescriptorCode record) (naturalSelect (bytes-equal kind b"event") (aosEventCode record) (naturalSelect (bytes-equal kind b"artifact") (aosArtifactCode record) (naturalSelect (bytes-equal kind b"coverage") (aosCoverageCode record) (naturalSelect (bytes-equal kind b"footer") (aosFooterCode record) 0)))))) (aosCriticalExtensionCode record))))))) -- --------------------------------------------------------------------------- -- Lines -- a line: parsed within the stream limits, then checked def aosClassifyLine = (lambda unrestricted line : Bytes . (eliminate JSONDocumentResult (lambda unrestricted current : (family JSONDocumentResult) . (family AosLine)) (parseJSONWithLimits aosLimits line) (branch JSONDocumentParsed record . (let unrestricted code = (aosRecordCode record) in (nat-eliminate (lambda unrestricted current : Nat . (family AosLine)) (constructor AosLine AosLineValid record) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AosLine) . (constructor AosLine AosLineInvalid code))) code))) (branch JSONDocumentFailed error offset . (constructor AosLine AosLineInvalid (aosParseErrorCode error))))) -- the line's verdict code (0: a valid record) def aosLineCode = (lambda unrestricted line : Bytes . (eliminate AosLine (lambda unrestricted current : (family AosLine) . Nat) (aosClassifyLine line) (branch AosLineInvalid code . code) (branch AosLineValid record . 0))) -- A descriptor is source-declared data. Constructing this tree grants no -- validity or authority; renderJSON and the normal AOS readers still check it. def aosDescriptorRecord = (lambda unrestricted kind : Bytes . (lambda unrestricted identity : Bytes . (lambda unrestricted body : (family JSON) . (constructor JSON JSONObject (constructor JSON JSONObjectMember b"format" (constructor JSON JSONString b"AOS-JSON/1") (constructor JSON JSONObjectMember b"type" (constructor JSON JSONString b"descriptor") (constructor JSON JSONObjectMember b"kind" (constructor JSON JSONString kind) (constructor JSON JSONObjectMember b"descriptor_id" (constructor JSON JSONString identity) (constructor JSON JSONObjectMember b"body" body (constructor JSON JSONObjectEnd))))))))))