CREATOR | Mark Raynsford |
DATE | 2022-01-15T17:18:45+00:00 |
DESCRIPTION | Specification for the Calino texture file format. |
IDENTIFIER | ba8fa621-69a4-486d-b5d7-1c31f76eba32 |
LANGUAGE | en |
RIGHTS | Public Domain |
TITLE | Calino 1.0 |
1 |
It would be more accurate to say that the calino specification does not depend
on any other specifications that are at the same level of abstraction. For example,
the calino specification makes references to
Unicode,
IEEE-754, and so on. It does not,
however, require understanding any other existing texture formats, or depend on any
definitions given in
the specifications for any rendering APIs.
References to this footnote:
1
|
Notation | Description |
---|---|
e ∈ A | e is an element of the set A |
e ∉ A | e is not an element of the set A |
{ x₀, x₁, ... xₙ } | A set consisting of values from x₀ to xₙ |
{ e ∈ A | p(e) } | A set consisting of the elements of A for which the proposition p holds |
|A| | The cardinality of the set A; a measure of the number of elements in A |
∅ | The empty set |
𝔹 | The booleans |
ℕ | The natural numbers |
ℝ | The real numbers |
ℤ | The integers |
[a, b] | A closed interval in a set (given separately or implicit from the types of a and b), from a to b, including a and b |
(a, b] | A closed interval in a set (given separately or implicit from the types of a and b), from a to b, excluding a but including b |
[a, b) | A closed interval in a set (given separately or implicit from the types of a and b), from a to b, including a but excluding b |
(a, b) | A closed interval in a set (given separately or implicit from the types of a and b), from a to b, excluding a and b |
A ⊂ B | A is a subset of, and is not equal to, B |
A ⊆ B | A is a subset of, or is equal to, B |
A ∩ B | The smallest set of elements that appear in both A and B (intersection). |
Definition divisible8 (x : nat) : Prop := modulo x 8 = 0.
Theorem divisiblity8Add : ∀ (x y : nat), divisible8 x → divisible8 y → divisible8 (x + y). Proof. (* Proof omitted for brevity; see Divisible8.v for proofs. *) Qed.
Inductive bit : Set := | B0 | B1.
Inductive octet : Set := | OctExact : bit → bit → bit → bit → bit → bit → bit → bit → octet | OctRemain : bit → bit → bit → bit → bit → bit → bit → bit → octet.
Fixpoint octetsBigEndianAux (bits : list bit) (octets : list octet) : list octet := match bits with | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) => octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: rest) => octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: rest) => octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: rest) => octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | [] => octets end.
Definition octetsBigEndian (bits : list bit) : list octet := octetsBigEndianAux bits [].
Definition octetsLittleEndian (bits : list bit) : list octet := rev (octetsBigEndianAux bits []).
Theorem octetsBigEndianLengthDivisibleAllExact : ∀ (b : list bit), divisible8 (length b) → Forall octetIsExact (octetsBigEndian b). Proof. (* Proof omitted for brevity; see ByteOrder.v for proofs. *) Qed.
Theorem octetsLittleEndianLengthDivisibleAllExact : ∀ (b : list bit), divisible8 (length b) → Forall octetIsExact (octetsLittleEndian b). Proof. (* Proof omitted for brevity; see ByteOrder.v for proofs. *) Qed.
Theorem octetsBigEndianLengthIndivisibleRemainder : ∀ (b : list bit), 0 < length b mod 8 → ∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o. Proof. (* Proof omitted for brevity; see ByteOrder.v for proofs. *) Qed.
Theorem octetsLittleEndianLengthIndivisibleRemainder : ∀ (b : list bit), 0 < length b mod 8 → ∃ o, In o (octetsLittleEndian b) ∧ octetIsRemainder o. Proof. (* Proof omitted for brevity; see ByteOrder.v for proofs. *) Qed.
Definition descriptor := string.
Class describable (A : Set) := { descriptorOf : A -> descriptor }.
Inductive channelSemantic : Set := | CSRed | CSGreen | CSBlue | CSAlpha | CSDepth | CSStencil | CSExponent | CSUnused.
Definition channelSemanticDescribe (c : channelSemantic) : descriptor := match c with | CSRed => "R" | CSGreen => "G" | CSBlue => "B" | CSAlpha => "A" | CSDepth => "D" | CSStencil => "S" | CSExponent => "E" | CSUnused => "X" end.
Instance channelSemanticDescribable : describable channelSemantic := { descriptorOf c := channelSemanticDescribe c }.
Inductive channelDescription : Set := channelDescriptionMake { cdSemantic : channelSemantic; cdBits : nat; cdBitsNonzero : 0 ≠ cdBits }.
Definition channelDescriptionDescribe (c : channelDescription) : descriptor := descriptorOf (cdSemantic c) ++ stringOfNat (cdBits c).
Instance channelDescriptionDescribable : describable channelDescription := { descriptorOf c := channelDescriptionDescribe c }.
Fixpoint channelDescriptionsDescribe (c : list channelDescription) : descriptor := match c with | nil => "" | cons d nil => channelDescriptionDescribe d | cons d e => (channelDescriptionDescribe d) ++ ":" ++ (channelDescriptionsDescribe e) end.
Inductive channelLayoutDescription : Set := | ChannelLayoutDescriptionUnpacked : channelLayoutDescriptionUnpacked → channelLayoutDescription | ChannelLayoutDescriptionPacked : channelLayoutDescriptionPacked → channelLayoutDescription.
Fixpoint channelDescriptionsBitsTotal (c : list channelDescription) : nat := match c with | nil => 0 | (x :: rest) => (cdBits x) + (channelDescriptionsBitsTotal rest) end.
Theorem channelLayoutDescriptionBitsDivisible8 : ∀ (c : channelLayoutDescription), divisible8 (channelLayoutDescriptionBits c). Proof. (* Proof omitted for brevity; see ChannelDescription.v for proofs. *) Qed.
Inductive channelLayoutDescriptionUnpacked : Set := CLDUMake { uChannels : list channelDescription; uChannelsNonEmpty : [] ≠ uChannels; uInvariants : Forall channelDescriptionBitsDivisible8 uChannels; }.
Inductive channelLayoutDescriptionPacked : Set := CLDPMake { pChannels : list channelDescription; pChannelsNonEmpty : [] ≠ pChannels; pPacking : channelLayoutPacking; pInvariants : channelDescriptionsBitsTotal pChannels = channelLayoutPackingBits pPacking }.
Inductive channelLayoutPacking : Set := | CLPack8 | CLPack16 | CLPack32 | CLPack64.
Definition channelLayoutPackingBits (c : channelLayoutPacking) : nat := match c with | CLPack8 => 8 | CLPack16 => 16 | CLPack32 => 32 | CLPack64 => 64 end.
Theorem channelLayoutPackingBitsDiv8 : ∀ c, divisible8 (channelLayoutPackingBits (c)). Proof. (* Proof omitted for brevity; see ChannelDescription.v for proofs. *) Qed.
Definition channelLayoutPackingDescribe (c : channelLayoutPacking) : descriptor := match c with | CLPack8 => "p8" | CLPack16 => "p16" | CLPack32 => "p32" | CLPack64 => "p64" end.
Instance channelLayoutPackingDescribable : describable channelLayoutPacking := { descriptorOf c := channelLayoutPackingDescribe c }.
Definition channelLayoutDescriptionUnpackedDescribe (c : channelLayoutDescriptionUnpacked) : descriptor := channelDescriptionsDescribe (uChannels c).
Instance channelLayoutDescriptionUnpackedDescribable : describable channelLayoutDescriptionUnpacked := { descriptorOf c := channelLayoutDescriptionUnpackedDescribe c }.
Definition channelLayoutDescriptionPackedDescribe (c : channelLayoutDescriptionPacked) : descriptor := let packing := descriptorOf (pPacking c) in let channels := channelDescriptionsDescribe (pChannels c) in packing ++ "|" ++ channels.
Instance channelLayoutDescriptionPackedDescribable : describable channelLayoutDescriptionPacked := { descriptorOf c := channelLayoutDescriptionPackedDescribe c }.
Definition channelLayoutDescriptionDescribe (c : channelLayoutDescription) : descriptor := match c with | ChannelLayoutDescriptionPacked p => descriptorOf p | ChannelLayoutDescriptionUnpacked u => descriptorOf u end.
Instance channelLayoutDescriptionDescribable : describable channelLayoutDescription := { descriptorOf c := channelLayoutDescriptionDescribe c }.
Inductive channelType : Set := | CTFixedPointNormalizedUnsigned | CTFixedPointNormalizedSigned | CTScaledUnsigned | CTScaledSigned | CTIntegerUnsigned | CTIntegerSigned | CTFloatIEEE754 | CTCustom : descriptor → channelType.
Definition channelTypeDescribe (c : channelType) : descriptor := match c with | CTFixedPointNormalizedUnsigned => "FIXED_POINT_NORMALIZED_UNSIGNED" | CTFixedPointNormalizedSigned => "FIXED_POINT_NORMALIZED_SIGNED" | CTScaledUnsigned => "SCALED_UNSIGNED" | CTScaledSigned => "SCALED_SIGNED" | CTIntegerUnsigned => "INTEGER_UNSIGNED" | CTIntegerSigned => "INTEGER_SIGNED" | CTFloatIEEE754 => "FLOATING_POINT_IEEE754" | CTCustom d => d end.
Instance channelTypeDescribable : describable channelType := { descriptorOf c := channelTypeDescribe c }.
Definition Layout_R4_G4_B4_A4 : channelLayoutDescription := ChannelLayoutDescriptionPacked (CLDPMake R4_G4_B4_A4_Channels R4_G4_B4_A4_NonEmpty CLPack16 eq_refl).
Definition Layout_A1_R5_G5_B5 : channelLayoutDescription := ChannelLayoutDescriptionPacked (CLDPMake A1_R5_G5_B5_Channels A1_R5_G5_B5_NonEmpty CLPack16 eq_refl).
Definition Layout_R5_G6_B5 : channelLayoutDescription := ChannelLayoutDescriptionPacked (CLDPMake R5_G6_B5_Channels R5_G6_B5_NonEmpty CLPack16 eq_refl).
Definition Layout_R8_G8_B8_A8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_A8_Channels R8_G8_B8_A8_NonEmpty R8_G8_B8_A8_FDiv8).
Definition Layout_R8_G8_B8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_Channels R8_G8_B8_NonEmpty R8_G8_B8_FDiv8).
Definition Layout_R8_G8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_Channels R8_G8_NonEmpty R8_G8_FDiv8).
Definition Layout_R8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_Channels R8_NonEmpty R8_FDiv8).
Definition Layout_R16_G16_B16_A16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_A16_Channels R16_G16_B16_A16_NonEmpty R16_G16_B16_A16_FDiv8).
Definition Layout_R16_G16_B16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_Channels R16_G16_B16_NonEmpty R16_G16_B16_FDiv8).
Definition Layout_R16_G16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_Channels R16_G16_NonEmpty R16_G16_FDiv8).
Definition Layout_R16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_Channels R16_NonEmpty R16_FDiv8).
Definition Layout_R32_G32_B32_A32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_A32_Channels R32_G32_B32_A32_NonEmpty R32_G32_B32_A32_FDiv8).
Definition Layout_R32_G32_B32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_Channels R32_G32_B32_NonEmpty R32_G32_B32_FDiv8).
Definition Layout_R32_G32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_Channels R32_G32_NonEmpty R32_G32_FDiv8).
Definition Layout_R32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_Channels R32_NonEmpty R32_FDiv8).
Definition Layout_R64_G64_B64_A64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_A64_Channels R64_G64_B64_A64_NonEmpty R64_G64_B64_A64_FDiv8).
Definition Layout_R64_G64_B64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_Channels R64_G64_B64_NonEmpty R64_G64_B64_FDiv8).
Definition Layout_R64_G64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_Channels R64_G64_NonEmpty R64_G64_FDiv8).
Definition Layout_R64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_Channels R64_NonEmpty R64_FDiv8).
Inductive colorSpace : Set := | CSLinear | CSsRGB | CSCustom : descriptor → colorSpace.
Definition colorSpaceDescribe (c : colorSpace) : descriptor := match c with | CSLinear => "LINEAR" | CSsRGB => "SRGB" | CSCustom d => d end.
Instance colorSpaceDescribable : describable colorSpace := { descriptorOf c := colorSpaceDescribe c }.
Inductive compressionMethod : Set := | CompressionUncompressed | CompressionBC1 | CompressionBC2 | CompressionBC3 | CompressionBC4 | CompressionBC5 | CompressionBC6 | CompressionBC7 | CompressionETC1 | CompressionETC2 | CompressionEAC | CompressionASTC : nat → nat → compressionMethod | CompressionCustom : ∀ (d : descriptor) (blockSizeX : nat) (blockSizeY : nat) (identifier : nat) (align : nat), 0 < align → compressionMethod.
Definition compressionMethodDescriptor (c : compressionMethod) := match c with | CompressionUncompressed => "UNCOMPRESSED" | CompressionBC1 => "BC1" | CompressionBC2 => "BC2" | CompressionBC3 => "BC3" | CompressionBC4 => "BC4" | CompressionBC5 => "BC5" | CompressionBC6 => "BC6" | CompressionBC7 => "BC7" | CompressionETC1 => "ETC1" | CompressionETC2 => "ETC2" | CompressionEAC => "EAC" | CompressionASTC _ _ => "ASTC" | CompressionCustom c _ _ _ _ _ => c end.
Instance compressionMethodDescribable : describable compressionMethod := { descriptorOf c := compressionMethodDescriptor c }.
Definition compressionBlockSizeX (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 4 | CompressionBC2 => 4 | CompressionBC3 => 4 | CompressionBC4 => 4 | CompressionBC5 => 4 | CompressionBC6 => 4 | CompressionBC7 => 4 | CompressionETC1 => 4 | CompressionETC2 => 4 | CompressionEAC => 4 | CompressionASTC x _ => x | CompressionCustom _ x _ _ _ _ => x end.
Definition compressionBlockSizeY (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 4 | CompressionBC2 => 4 | CompressionBC3 => 4 | CompressionBC4 => 4 | CompressionBC5 => 4 | CompressionBC6 => 4 | CompressionBC7 => 4 | CompressionETC1 => 4 | CompressionETC2 => 4 | CompressionEAC => 4 | CompressionASTC _ y => y | CompressionCustom _ _ y _ _ _ => y end.
Definition compressionBlockAlignment (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 8 | CompressionBC2 => 16 | CompressionBC3 => 16 | CompressionBC4 => 8 | CompressionBC5 => 16 | CompressionBC6 => 16 | CompressionBC7 => 16 | CompressionETC1 => 16 | CompressionETC2 => 16 | CompressionEAC => 16 | CompressionASTC _ _ => 16 | CompressionCustom _ _ _ _ a _ => a end.
Definition compressionSectionIdentifier (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 0 | CompressionBC2 => 0 | CompressionBC3 => 0 | CompressionBC4 => 0 | CompressionBC5 => 0 | CompressionBC6 => 0 | CompressionBC7 => 0 | CompressionETC1 => 0 | CompressionETC2 => 0 | CompressionEAC => 0 | CompressionASTC _ _ => 0 | CompressionCustom _ _ _ i _ _ => i end.
Inductive superCompressionMethod : Set := | SuperCompressionUncompressed | SuperCompressionLZ4 | SuperCompressionCustom : descriptor → nat → superCompressionMethod.
Definition superCompressionMethodDescriptor (c : superCompressionMethod) := match c with | SuperCompressionUncompressed => "UNCOMPRESSED" | SuperCompressionLZ4 => "LZ4" | SuperCompressionCustom c _ => c end.
Instance superCompressionMethodDescribable : describable superCompressionMethod := { descriptorOf c := superCompressionMethodDescriptor c }.
Definition superCompressionSectionIdentifier (c : superCompressionMethod) : nat := match c with | SuperCompressionUncompressed => 0 | SuperCompressionLZ4 => 0 | SuperCompressionCustom _ i => i end.
Inductive coordinateAxisR : Set := | AxisRIncreasingToward | AxisRIncreasingAway.
Inductive coordinateAxisS : Set := | AxisSIncreasingRight | AxisSIncreasingLeft.
Inductive coordinateAxisT : Set := | AxisTIncreasingDown | AxisTIncreasingUp.
Inductive coordinateSystem : Set := CoordinateSystem : coordinateAxisR → coordinateAxisS → coordinateAxisT → coordinateSystem.
Definition coordinateAxisRDescribe (c : coordinateAxisR) : descriptor := match c with | AxisRIncreasingToward => "RT" | AxisRIncreasingAway => "RA" end.
Instance coordinateAxisRDescribable : describable coordinateAxisR := { descriptorOf c := coordinateAxisRDescribe c }.
Definition coordinateAxisSDescribe (c : coordinateAxisS) : descriptor := match c with | AxisSIncreasingRight => "SR" | AxisSIncreasingLeft => "SL" end.
Instance coordinateAxisSDescribable : describable coordinateAxisS := { descriptorOf c := coordinateAxisSDescribe c }.
Definition coordinateAxisTDescribe (c : coordinateAxisT) : descriptor := match c with | AxisTIncreasingDown => "TD" | AxisTIncreasingUp => "TU" end.
Instance coordinateAxisTDescribable : describable coordinateAxisT := { descriptorOf c := coordinateAxisTDescribe c }.
Definition coordinateSystemDescribe (c : coordinateSystem) : descriptor := match c with | CoordinateSystem r s t => descriptorOf r ++ ":" ++ descriptorOf s ++ ":" ++ descriptorOf t end.
Instance coordinateSystemDescribable : describable coordinateSystem := { descriptorOf c := coordinateSystemDescribe c }.
Inductive flag : Set := | FlagAlphaPremultiplied | FlagCustom : descriptor → flag.
Inductive flagSet : Set := { flags : list flag; flagsNoDup : NoDup flags; }.
Definition flagDescribe (f : flag) : descriptor := match f with | FlagAlphaPremultiplied => "ALPHA_PREMULTIPLIED" | FlagCustom d => d end.
Instance flagDescribable : describable flag := { descriptorOf f := flagDescribe f }.
Record imageInfo : Set := ImageInfo { imageSize : imageSize3D; imageChannelsLayout : channelLayoutDescription; imageChannelsType : channelType; imageCompressionMethod : compressionMethod; imageSuperCompressionMethod : superCompressionMethod; imageCoordinateSystem : coordinateSystem; imageColorSpace : colorSpace; imageFlags : flagSet; imageByteOrder : byteOrder }.
Record imageSize3D : Set := ImageSize3D { sizeX : nat; sizeY : nat; sizeZ : nat; sizeXnot0 : 0 ≠ sizeX; sizeYnot0 : 0 ≠ sizeY; sizeZnot0 : 0 ≠ sizeZ; }.
Definition imageInfoTexelBlockAlignment (i : imageInfo) := let c := imageCompressionMethod i in match c with | CompressionUncompressed => channelLayoutDescriptionBits (imageChannelsLayout i) / 8 | _ => compressionBlockAlignment c end.
Inductive mipMap : Set := MipMap { mipMapLevel : nat; mipMapOffset : nat; mipMapSizeCompressed : nat; mipMapSizeUncompressed : nat; mipMapCRC32 : nat }.
Inductive mipMapListIsSorted : list mipMap → Prop := | MipsOne : ∀ m, mipMapListIsSorted [m] | MipsCons : ∀ mm0 mm1 mxs, mipMapLevel mm1 = S (mipMapLevel mm0) → mipMapListIsSorted (mm0 :: mxs) → mipMapListIsSorted (mm1 :: mm0 :: mxs).
Inductive mipMapOffsetsSorted : list mipMap → Prop := | MMSizeOne : ∀ m, mipMapOffsetsSorted [m] | MMSizeCons : ∀ mm0 mm1 mxs, ((mipMapOffset mm1) + (mipMapSizeCompressed mm1)) < (mipMapOffset mm0) → mipMapOffsetsSorted (mm0 :: mxs) → mipMapOffsetsSorted (mm1 :: mm0 :: mxs).
Inductive mipMapList : Set := MipMapList { mipMaps : list mipMap; mipMapListSorted : mipMapListIsSorted mipMaps; mipMapOffsetSorted : mipMapOffsetsSorted mipMaps; }.
Inductive mipMapImageSize : Set := MipMapImageSize { mmSizeX : nat; mmSizeY : nat; mmSizeXRange : 1 < mmSizeX; mmSizeYRange : 1 < mmSizeY; }.
Definition mipMapSize (level : nat) (imageSize : imageSize3D) (levelRange : 0 < level) : option mipMapImageSize := let sx := (sizeX imageSize) / 2 ^ level in let sy := (sizeY imageSize) / 2 ^ level in match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with | (ReflectT _ xt, ReflectT _ yt) => Some (MipMapImageSize sx sy xt yt) | (_, _) => None end.
Fixpoint mipMapImageDataSizeTotalAux (m : list mipMap) : nat := match m with | [] => 0 | (x :: []) => (mipMapOffset x) + (mipMapSizeCompressed x) | (x :: xs) => mipMapImageDataSizeTotalAux xs end.
Definition mipMapImageDataSizeTotal (m : mipMapList) : nat := mipMapImageDataSizeTotalAux (mipMaps m).
Inductive arrayMipMapIndexT : Set := ArrayMipMapIndex { arrayMipMapLevel : nat; arrayMipMapLayer : nat; }.
Inductive arrayMipMap : Set := ArrayMipMap { arrayMipMapIndex : arrayMipMapIndexT; arrayMipMapOffset : nat; arrayMipMapSizeCompressed : nat; arrayMipMapSizeUncompressed : nat; arrayMipMapCRC32 : nat }.
Fixpoint arrayMipMapLayerCountForLevel (level : nat) (m : list arrayMipMap) : nat := match m with | [] => 0 | (x :: xs) => match Nat.eq_dec (arrayMipMapLevel (arrayMipMapIndex x)) level with | left _ => 1 + (arrayMipMapLayerCountForLevel level xs) | right _ => (arrayMipMapLayerCountForLevel level xs) end end.
Definition arrayMipMapLevels (m : list arrayMipMap) : list nat := nodup Nat.eq_dec (map (λ k, arrayMipMapLevel (arrayMipMapIndex k)) m).
Definition arrayMipMapsHaveSameLayers : (list arrayMipMap) → nat → nat → Prop := λ m level0 level1, In level0 (arrayMipMapLevels m) → In level1 (arrayMipMapLevels m) → arrayMipMapLayerCountForLevel level0 m = arrayMipMapLayerCountForLevel level1 m.
Inductive arrayMipMapIndexOrd : arrayMipMapIndexT → arrayMipMapIndexT → Prop := | AMMIOrdEq : ∀ i0 i1, i0 = i1 → arrayMipMapIndexOrd i0 i1 | AMMIOrdLevelEq : ∀ i0 i1, arrayMipMapLevel i0 = arrayMipMapLevel i1 → arrayMipMapLayer i0 < arrayMipMapLayer i1 → arrayMipMapIndexOrd i0 i1 | AMIIOrdLevelLt : ∀ i0 i1, arrayMipMapLevel i1 < arrayMipMapLevel i0 → arrayMipMapIndexOrd i0 i1.
Inductive arrayMipMapIndicesSorted : list arrayMipMapIndexT → Prop := | AMMIOne : ∀ m, arrayMipMapIndicesSorted [m] | AMMICons : ∀ mmx mmy mxs, arrayMipMapIndexOrd mmx mmy → arrayMipMapIndicesSorted (mmy :: mxs) → arrayMipMapIndicesSorted (mmx :: mmy :: mxs).
Inductive arrayMipMapList : Set := ArrayMipMapList { arrayMipMaps : list arrayMipMap; arrayMipMapIndicesAreSorted : arrayMipMapIndicesSorted (map arrayMipMapIndex arrayMipMaps); arrayMipMapOffsetAreSorted : arrayMipMapOffsetsSorted arrayMipMaps; arrayMipMapSameLayers : ∀ level0 level1, arrayMipMapsHaveSameLayers arrayMipMaps level0 level1 }.
Inductive arrayMipMapOffsetsSorted : list arrayMipMap → Prop := | AMMSizeOne : ∀ m, arrayMipMapOffsetsSorted [m] | AMMSizeCons : ∀ mm0 mm1 mxs, ((arrayMipMapOffset mm1) + (arrayMipMapSizeCompressed mm1)) < (arrayMipMapOffset mm0) → arrayMipMapOffsetsSorted (mm0 :: mxs) → arrayMipMapOffsetsSorted (mm1 :: mm0 :: mxs).
Inductive arrayMipMapImageSize : Set := ArrayMipMapImageSize { ammSizeX : nat; ammSizeY : nat; ammSizeXRange : 1 < ammSizeX; ammSizeYRange : 1 < ammSizeY; }.
Definition arrayMipMapSize (level : nat) (imageSize : imageSize3D) (levelRange : 0 < level) : option arrayMipMapImageSize := let sx := (sizeX imageSize) / 2 ^ level in let sy := (sizeY imageSize) / 2 ^ level in match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with | (ReflectT _ xt, ReflectT _ yt) => Some (ArrayMipMapImageSize sx sy xt yt) | (_, _) => None end.
Fixpoint arrayMipMapImageDataSizeTotalAux (m : list arrayMipMap) : nat := match m with | [] => 0 | (x :: []) => (arrayMipMapOffset x) + (arrayMipMapSizeCompressed x) | (x :: xs) => arrayMipMapImageDataSizeTotalAux xs end.
Definition arrayMipMapImageDataSizeTotal (m : arrayMipMapList) : nat := arrayMipMapImageDataSizeTotalAux (arrayMipMaps m).
Inductive cubeMapFace : Set := CubeMapFace { cubeFaceOffset : nat; cubeFaceSizeCompressed : nat; cubeFaceSizeUncompressed : nat; cubeFaceCRC32 : nat }.
Inductive cubeMipMap : Set := CubeMipMap { cubeMapLevel : nat; cubeMapFaceXPos : cubeMapFace; cubeMapFaceXNeg : cubeMapFace; cubeMapFaceYPos : cubeMapFace; cubeMapFaceYNeg : cubeMapFace; cubeMapFaceZPos : cubeMapFace; cubeMapFaceZNeg : cubeMapFace }.
Inductive cubeMipMapListIsSorted : list cubeMipMap → Prop := | CubeOne : ∀ m, cubeMipMapListIsSorted [m] | CubeCons : ∀ mm0 mm1 mxs, cubeMapLevel mm1 = S (cubeMapLevel mm0) → cubeMipMapListIsSorted (mm0 :: mxs) → cubeMipMapListIsSorted (mm1 :: mm0 :: mxs).
Definition cubeFaceExtent (f : cubeMapFace) : nat := cubeFaceOffset f + cubeFaceSizeCompressed f.
Inductive cubeOffsetsSorted : list cubeMipMap → Prop := | CMMSizeOne : ∀ m, cubeFaceExtent (cubeMapFaceXPos m) < cubeFaceOffset (cubeMapFaceXNeg m) → cubeFaceExtent (cubeMapFaceXNeg m) < cubeFaceOffset (cubeMapFaceYPos m) → cubeFaceExtent (cubeMapFaceYPos m) < cubeFaceOffset (cubeMapFaceYNeg m) → cubeFaceExtent (cubeMapFaceYNeg m) < cubeFaceOffset (cubeMapFaceZPos m) → cubeFaceExtent (cubeMapFaceZPos m) < cubeFaceOffset (cubeMapFaceZNeg m) → cubeOffsetsSorted [m] | CMMSizeCons : ∀ mm0 mm1 mxs, cubeFaceExtent (cubeMapFaceZNeg mm1) < cubeFaceOffset (cubeMapFaceXPos mm0) → cubeOffsetsSorted (mm0 :: mxs) → cubeOffsetsSorted (mm1 :: mm0 :: mxs).
Fixpoint cubeMipMapImageDataSizeTotalAux (m : list cubeMipMap) : nat := match m with | [] => 0 | (x :: []) => cubeFaceExtent (cubeMapFaceZNeg x) | (x :: xs) => cubeMipMapImageDataSizeTotalAux xs end.
Definition cubeMipMapImageDataSizeTotal (m : cubeMipMapList) : nat := cubeMipMapImageDataSizeTotalAux (cubeMipMaps m).
Inductive metadataValue : Set := MetadataValue { mKey : string; mValue : string }.
Inductive metadata : Set := Metadata { mValues : list metadataValue }.
Inductive texture : Set := | TTexture2D : texture2d → texture | TTextureArray : textureArray → texture | TTextureCube : textureCube → texture.
Inductive texture2d : Set := Texture2D { i2dInfo : imageInfo; i2dMipMaps : mipMapList; i2dSize : 1 = imageSizeZ i2dInfo }.
Inductive textureArray : Set := TextureArray { iaInfo : imageInfo; iaMipMaps : arrayMipMapList; iaSize : 1 <= imageSizeZ iaInfo }.
Inductive textureCube : Set := TextureCube { icubeInfo : imageInfo; icubeMipMaps : cubeMipMapList; icubeSize : 1 = imageSizeZ icubeInfo }.
Inductive binaryExp : Set := | BiU32 : nat → binaryExp | BiU64 : nat → binaryExp | BiBytes : list byte → binaryExp | BiUTF8 : list byte → binaryExp | BiArray : list binaryExp → binaryExp | BiReserve : nat → binaryExp | BiRecord : list (string * binaryExp) → binaryExp.
Fixpoint binarySize (b : binaryExp) : nat := match b with | BiU32 _ => 4 | BiU64 _ => 8 | BiBytes s => 4 + asMultipleOf4 (length s) | BiUTF8 s => 4 + asMultipleOf4 (length s) | BiArray f => 4 + fold_right plus 0 (map binarySize f) | BiReserve s => asMultipleOf4 s | BiRecord f => fold_right plus 0 (map (binarySize ∘ snd) f) end.
Definition asMultipleOf (size q : nat) (Hnz : 0 ≠ q) : nat := let r := size / q in match Nat.ltb_spec0 r q with | ReflectT _ _ => (r + 1) * q | ReflectF _ _ => r * q end.
Theorem binarySizeMultiple4 : ∀ b, binarySize (b) mod 4 = 0. Proof. (* Proof omitted for brevity; see Binary.v for proofs. *) Qed.
Definition binarySizePadded16 (b : binaryExp) : nat := asMultipleOf16 (binarySize b).
Definition asMultipleOf4 (size : nat) : nat := asMultipleOf size 4 p0not4.
Inductive streamE : Set := | Vu64 : nat → streamE | Vu32 : nat → streamE | Vu8 : nat → streamE.
Fixpoint binaryEval (b : binaryExp) : list streamE := match b with | BiU32 k => [Vu32 k] | BiU64 k => [Vu64 k] | BiBytes s => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4) | BiUTF8 s => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4) | BiArray f => (Vu32 (length f)) :: concat (map binaryEval f) | BiReserve s => repeat (Vu8 0) (asMultipleOf4 s) | BiRecord f => concat (map (binaryEval ∘ snd) f) end.
Definition binaryEvalPaddedBytes (b : list byte) (align : nat) (Hneq : 0 ≠ align) : list streamE := let vremaining := length b mod align in match vremaining with | 0 => map u8byte b | _ => map u8byte (b ++ repeat x00 (align - vremaining)) end.
Inductive streamWellFormed : list streamE → Prop := | BEPEmpty : streamWellFormed [] | BEPVu64 : ∀ k, streamWellFormed [Vu64 k] | BEPVu32 : ∀ k, streamWellFormed [Vu32 k] | BEPVu8s : ∀ es, Forall streamEIsU8 es → length (es) mod 4 = 0 → streamWellFormed es | BEPAppend : ∀ xs ys, streamWellFormed xs → streamWellFormed ys → streamWellFormed (xs ++ ys).
Theorem binaryEvalStreamsWellFormed : ∀ b, streamWellFormed (binaryEval b). Proof. (* Proof omitted for brevity; see Binary.v for proofs. *) Qed.
Theorem streamsWellFormedDivisible4 : ∀ es, streamWellFormed es → streamSize es mod 4 = 0. Proof. (* Proof omitted for brevity; see Binary.v for proofs. *) Qed.
Definition binaryExpFileHeader : binaryExp := BiRecord [ ("id", u64 0x89434C4E0D0A1A0A); ("versionMajor", u32 1); ("versionMinor", u32 0) ].
Identifier | Description |
---|---|
0x434C4E49494E464F | Image information. |
0x434C4E5F49324421 | Image data for 2D textures. |
0x434C4E5F41525221 | Image data for array textures. |
0x434C4E5F43554245 | Image data for cube textures. |
0x434C4E5F4D455441 | Key/value metadata. |
0x434C4E5F454E4421 | File terminator. |
Definition binaryExpImageInfo (i : imageInfo) : binaryExp := BiRecord [ ("sizeX", u32 (imageSizeX i)); ("sizeY", u32 (imageSizeY i)); ("sizeZ", u32 (imageSizeZ i)); ("channelsLayout", utf8 (descriptorOf (imageChannelsLayout i))); ("channelsType", utf8 (descriptorOf (imageChannelsType i))); ("compression", binaryExpCompression (imageCompressionMethod i)); ("superCompression", binaryExpSuperCompression (imageSuperCompressionMethod i)); ("coordinateSystem", utf8 (descriptorOf (imageCoordinateSystem i))); ("colorSpace", utf8 (descriptorOf (imageColorSpace i))); ("flags", BiArray (map (utf8 ∘ descriptorOf) (imageFlagSet i))); ("byteOrder", utf8 (descriptorOf (imageByteOrder i))) ].
Definition binaryExpCompression (c : compressionMethod) : binaryExp := BiRecord [ ("descriptor", utf8 (descriptorOf c)); ("sectionIdentifier", u64 (compressionSectionIdentifier c)); ("blockSizeX", u32 (compressionBlockSizeX c)); ("blockSizeY", u32 (compressionBlockSizeY c)); ("blockAlignment", u32 (compressionBlockAlignment c)) ].
Definition binaryExpSuperCompression (c : superCompressionMethod) : binaryExp := BiRecord [ ("descriptor", utf8 (descriptorOf c)); ("sectionIdentifier", u64 (superCompressionSectionIdentifier c)) ].
Definition binaryExpImageInfoSection (i : imageInfo) : binaryExp := BiRecord [ ("id", u64 0x434C4E49494E464F); ("size", u64 (binarySizePadded16 (binaryExpImageInfo i))); ("data", binaryExpImageInfo i) ].
Definition binaryExpMipMap (m : mipMap) : binaryExp := BiRecord [ ("mipMapLevel", u32 (mipMapLevel m)); ("mipMapDataOffset", u64 (mipMapOffset m)); ("mipMapSizeUncompressed", u64 (mipMapSizeUncompressed m)); ("mipMapSizeCompressed", u64 (mipMapSizeCompressed m)); ("mipMapCRC32", u32 (mipMapCRC32 m)) ].
Definition binaryExpMipMaps (m : mipMapList) : binaryExp := BiArray (map binaryExpMipMap (mipMaps m)).
Definition binaryExpImage2D (i : imageInfo) (m : mipMapList) : binaryExp := let imageDataStart := mipMapOffset (mipMapFirst m) in let encMips := binaryExpMipMaps m in let encMipsSize := binarySize encMips in let encMipsPad := imageDataStart - encMipsSize in let imageSize := mipMapImageDataSizeTotal m in let imageSize16 := asMultipleOf16 imageSize in BiRecord [ ("mipMaps", encMips); ("mipPad", BiReserve encMipsPad); ("mipData", BiReserve imageSize16) ].
Definition binaryExpImage2DSection (i : imageInfo) (m : mipMapList) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F49324421); ("size", u64 (binarySizePadded16 (binaryExpImage2D i m))); ("data", binaryExpImage2D i m) ].
Definition binaryExpArrayMipMap (m : arrayMipMap) : binaryExp := BiRecord [ ("arrayMipMapLevel", u32 (arrayMipMapLevel (arrayMipMapIndex m))); ("arrayMipMapLayer", u32 (arrayMipMapLayer (arrayMipMapIndex m))); ("arrayMipMapDataOffset", u64 (arrayMipMapOffset m)); ("arrayMipMapSizeUncompressed", u64 (arrayMipMapSizeUncompressed m)); ("arrayMipMapSizeCompressed", u64 (arrayMipMapSizeCompressed m)); ("arrayMipMapCRC32", u32 (arrayMipMapCRC32 m)) ].
Definition binaryExpArrayMipMaps (m : arrayMipMapList) : binaryExp := BiArray (map binaryExpArrayMipMap (arrayMipMaps m)).
Definition binaryExpImageArray (i : imageInfo) (m : arrayMipMapList) : binaryExp := let imageDataStart := arrayMipMapOffset (arrayMipMapFirst m) in let encMips := binaryExpArrayMipMaps m in let encMipsSize := binarySize encMips in let encMipsPad := imageDataStart - encMipsSize in let imageSize := arrayMipMapImageDataSizeTotal m in let imageSize16 := asMultipleOf16 imageSize in BiRecord [ ("arrayMipMaps", encMips); ("arrayMipPad", BiReserve encMipsPad); ("arrayMipData", BiReserve imageSize16) ].
Definition binaryExpImageArraySection (i : imageInfo) (m : arrayMipMapList) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F41525221); ("size", u64 (binarySizePadded16 (binaryExpImageArray i m))); ("data", binaryExpImageArray i m) ].
Definition binaryExpCubeMipMapFace (m : cubeMapFace) : binaryExp := BiRecord [ ("cubeFaceDataOffset", u64 (cubeFaceOffset m)); ("cubeFaceSizeUncompressed", u64 (cubeFaceSizeUncompressed m)); ("cubeFaceSizeCompressed", u64 (cubeFaceSizeCompressed m)); ("cubeFaceCRC32", u32 (cubeFaceCRC32 m)) ].
Definition binaryExpCubeMipMap (m : cubeMipMap) : binaryExp := BiRecord [ ("cubeMipMapLevel", u32 (cubeMapLevel m)); ("cubeMipMapFacePosX", binaryExpCubeMipMapFace (cubeMapFaceXPos m)); ("cubeMipMapFaceNegX", binaryExpCubeMipMapFace (cubeMapFaceXNeg m)); ("cubeMipMapFacePosY", binaryExpCubeMipMapFace (cubeMapFaceYPos m)); ("cubeMipMapFaceNegY", binaryExpCubeMipMapFace (cubeMapFaceYNeg m)); ("cubeMipMapFacePosZ", binaryExpCubeMipMapFace (cubeMapFaceZPos m)); ("cubeMipMapFaceNegZ", binaryExpCubeMipMapFace (cubeMapFaceZNeg m)) ].
Definition binaryExpCubeMipMaps (m : cubeMipMapList) : binaryExp := BiArray (map binaryExpCubeMipMap (cubeMipMaps m)).
Definition binaryExpImageCubeMap (i : imageInfo) (m : cubeMipMapList) : binaryExp := let imageDataStart := cubeFaceOffset (cubeMapFaceXPos (cubeMipMapsFirst m)) in let encMips := binaryExpCubeMipMaps m in let encMipsSize := binarySize encMips in let encMipsPad := imageDataStart - encMipsSize in let imageSize := cubeMipMapImageDataSizeTotal m in let imageSize16 := asMultipleOf16 imageSize in BiRecord [ ("cubeMipMaps", encMips); ("cubeMipPad", BiReserve encMipsPad); ("cubeMipData", BiReserve imageSize16) ].
Definition binaryExpImageCubeSection (i : imageInfo) (m : cubeMipMapList) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F43554245); ("size", u64 (binarySizePadded16 (binaryExpImageCubeMap i m))); ("data", binaryExpImageCubeMap i m) ].
Definition binaryExpMetadataValue (m : metadataValue) : binaryExp := BiRecord [ ("key", utf8 (mKey m)); ("value", utf8 (mValue m)) ].
Definition binaryExpMetadata (m : metadata) : binaryExp := BiArray (map binaryExpMetadataValue (mValues m)).
Definition binaryExpMetadataSection (m : metadata) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F4D455441); ("size", u64 (binarySizePadded16 (binaryExpMetadata m))); ("data", binaryExpMetadata m) ].
Definition binaryEndSection : binaryExp := BiRecord [ ("id", u64 0x434c4e5f454e4421); ("size", u64 0) ].
43 4C 4E 5F 4D 45 54 41 ; Identifier 0x434C4E49494E464F 00 00 00 00 00 00 00 30 ; Section is 48 bytes 00 00 00 02 ; Size of metadata array is 2 00 00 00 02 ; Size of first key is 2 4B 30 00 00 ; Key is "K0" plus padding octets 00 00 00 04 ; Size of first value is 4 56 41 4C 30 ; Value is "VAL0", no padding required 00 00 00 04 ; Size of second key is 4 4B 45 59 31 ; Key is "KEY1", no padding required 00 00 00 04 ; Size of second value is 4 56 41 4C 31 ; Value is "VAL1", no padding required 00 00 00 00 00 00 00 00 00 00 00 00 ; 12 padding octets, so the size of the ; section is a multiple of 16
Require Import Coq.Arith.PeanoNat. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Init.Byte. Require Import Coq.Bool.Bool. Require Import Coq.Program.Basics. Require Import Coq.Unicode.Utf8_core. Definition asMultipleOf (size q : nat) (Hnz : 0 ≠ q) : nat := let r := size / q in match Nat.ltb_spec0 r q with | ReflectT _ _ => (r + 1) * q | ReflectF _ _ => r * q end. Lemma p0not4 : 0 ≠ 4. Proof. discriminate. Qed. Lemma p0not16 : 0 ≠ 16. Proof. discriminate. Qed. Definition asMultipleOf4 (size : nat) : nat := asMultipleOf size 4 p0not4. Definition asMultipleOf16 (size : nat) : nat := asMultipleOf size 16 p0not16. Lemma asMultipleOfMod : ∀ s q (Hneq : 0 ≠ q), (asMultipleOf s q Hneq) mod q = 0. Proof. intros s q Hneq. unfold asMultipleOf. destruct (Nat.ltb_spec0 (s / q) q) as [Hlt|H1]. - apply (Nat.mod_mul (s / q + 1) q (Nat.neq_sym _ _ Hneq)). - apply (Nat.mod_mul (s / q) q (Nat.neq_sym _ _ Hneq)). Qed.
Require Import Coq.Arith.PeanoNat. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Bool.Bool. Require Import Coq.Unicode.Utf8_core. Require Import Calino.ImageSize. Import ListNotations. Inductive arrayMipMapIndexT : Set := ArrayMipMapIndex { arrayMipMapLevel : nat; arrayMipMapLayer : nat; }. Inductive arrayMipMapIndexOrd : arrayMipMapIndexT → arrayMipMapIndexT → Prop := | AMMIOrdEq : ∀ i0 i1, i0 = i1 → arrayMipMapIndexOrd i0 i1 | AMMIOrdLevelEq : ∀ i0 i1, arrayMipMapLevel i0 = arrayMipMapLevel i1 → arrayMipMapLayer i0 < arrayMipMapLayer i1 → arrayMipMapIndexOrd i0 i1 | AMIIOrdLevelLt : ∀ i0 i1, arrayMipMapLevel i1 < arrayMipMapLevel i0 → arrayMipMapIndexOrd i0 i1. Inductive arrayMipMapIndicesSorted : list arrayMipMapIndexT → Prop := | AMMIOne : ∀ m, arrayMipMapIndicesSorted [m] | AMMICons : ∀ mmx mmy mxs, arrayMipMapIndexOrd mmx mmy → arrayMipMapIndicesSorted (mmy :: mxs) → arrayMipMapIndicesSorted (mmx :: mmy :: mxs). Inductive arrayMipMap : Set := ArrayMipMap { arrayMipMapIndex : arrayMipMapIndexT; arrayMipMapOffset : nat; arrayMipMapSizeCompressed : nat; arrayMipMapSizeUncompressed : nat; arrayMipMapCRC32 : nat }. Inductive arrayMipMapOffsetsSorted : list arrayMipMap → Prop := | AMMSizeOne : ∀ m, arrayMipMapOffsetsSorted [m] | AMMSizeCons : ∀ mm0 mm1 mxs, ((arrayMipMapOffset mm1) + (arrayMipMapSizeCompressed mm1)) < (arrayMipMapOffset mm0) → arrayMipMapOffsetsSorted (mm0 :: mxs) → arrayMipMapOffsetsSorted (mm1 :: mm0 :: mxs). Fixpoint arrayMipMapLayerCountForLevel (level : nat) (m : list arrayMipMap) : nat := match m with | [] => 0 | (x :: xs) => match Nat.eq_dec (arrayMipMapLevel (arrayMipMapIndex x)) level with | left _ => 1 + (arrayMipMapLayerCountForLevel level xs) | right _ => (arrayMipMapLayerCountForLevel level xs) end end. Definition arrayMipMapLevels (m : list arrayMipMap) : list nat := nodup Nat.eq_dec (map (λ k, arrayMipMapLevel (arrayMipMapIndex k)) m). Definition arrayMipMapsHaveSameLayers : (list arrayMipMap) → nat → nat → Prop := λ m level0 level1, In level0 (arrayMipMapLevels m) → In level1 (arrayMipMapLevels m) → arrayMipMapLayerCountForLevel level0 m = arrayMipMapLayerCountForLevel level1 m. Inductive arrayMipMapList : Set := ArrayMipMapList { arrayMipMaps : list arrayMipMap; arrayMipMapIndicesAreSorted : arrayMipMapIndicesSorted (map arrayMipMapIndex arrayMipMaps); arrayMipMapOffsetAreSorted : arrayMipMapOffsetsSorted arrayMipMaps; arrayMipMapSameLayers : ∀ level0 level1, arrayMipMapsHaveSameLayers arrayMipMaps level0 level1 }. Inductive arrayMipMapImageSize : Set := ArrayMipMapImageSize { ammSizeX : nat; ammSizeY : nat; ammSizeXRange : 1 < ammSizeX; ammSizeYRange : 1 < ammSizeY; }. Lemma arrayMipMapsNonEmpty : ∀ (m : arrayMipMapList), [] ≠ arrayMipMaps m. Proof. intros m. destruct (arrayMipMapOffsetAreSorted m). - discriminate. - discriminate. Qed. Definition arrayMipMapFirst (m : arrayMipMapList) : arrayMipMap. Proof. assert ([] ≠ arrayMipMaps m) as Hneq by (apply (arrayMipMapsNonEmpty)). destruct (arrayMipMaps m) eqn:Hm. - contradiction. - exact a. Defined. Lemma lt_neq : ∀ n, 0 ≠ n ↔ 0 < n. Proof. intros n. constructor. - intro Hneq. induction n as [|k]. -- unfold not in Hneq. assert (0 = 0) as Heq by reflexivity. contradiction. -- apply (Nat.lt_0_succ k). - intro Hneq. induction n as [|k]. -- inversion Hneq. -- discriminate. Qed. Lemma lt_neq_0 : ∀ n, 0 ≠ n → 0 < n. Proof. intros n Hneq. rewrite <- lt_neq; trivial. Qed. Lemma lt_neq_1 : ∀ n, 0 < n → 0 ≠ n. Proof. intros n Hneq. rewrite lt_neq; trivial. Qed. Definition arrayMipMapSize (level : nat) (imageSize : imageSize3D) (levelRange : 0 < level) : option arrayMipMapImageSize := let sx := (sizeX imageSize) / 2 ^ level in let sy := (sizeY imageSize) / 2 ^ level in match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with | (ReflectT _ xt, ReflectT _ yt) => Some (ArrayMipMapImageSize sx sy xt yt) | (_, _) => None end. Fixpoint arrayMipMapImageDataSizeTotalAux (m : list arrayMipMap) : nat := match m with | [] => 0 | (x :: []) => (arrayMipMapOffset x) + (arrayMipMapSizeCompressed x) | (x :: xs) => arrayMipMapImageDataSizeTotalAux xs end. Definition arrayMipMapImageDataSizeTotal (m : arrayMipMapList) : nat := arrayMipMapImageDataSizeTotalAux (arrayMipMaps m). Example exampleArrayMipMapsIndices := [ (ArrayMipMapIndex 2 0); (ArrayMipMapIndex 2 1); (ArrayMipMapIndex 2 2); (ArrayMipMapIndex 1 0); (ArrayMipMapIndex 1 1); (ArrayMipMapIndex 1 2); (ArrayMipMapIndex 0 0); (ArrayMipMapIndex 0 1); (ArrayMipMapIndex 0 2) ]. Example exampleArrayMipMaps := map (λ i, ArrayMipMap i 0 0 0 0) exampleArrayMipMapsIndices. Example exampleArrayMipMapIndicesSorted : arrayMipMapIndicesSorted exampleArrayMipMapsIndices. Proof. apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. } apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. } apply AMMICons. { apply AMIIOrdLevelLt. compute; constructor. } apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. } apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. } apply AMMICons. { apply AMIIOrdLevelLt. compute; constructor. } apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. } apply AMMICons. { apply AMMIOrdLevelEq. reflexivity. compute; constructor. } apply AMMIOne. Qed. Example exampleArrayMipMapsHaveSameLayers0 : arrayMipMapLayerCountForLevel 0 exampleArrayMipMaps = 3. Proof. reflexivity. Qed. Example exampleArrayMipMapsHaveSameLayers1 : arrayMipMapLayerCountForLevel 1 exampleArrayMipMaps = 3. Proof. reflexivity. Qed. Example exampleArrayMipMapsHaveSameLayers2 : arrayMipMapLayerCountForLevel 2 exampleArrayMipMaps = 3. Proof. reflexivity. Qed. Example exampleArrayMipMapsLevel : ∀ n, In n (arrayMipMapLevels exampleArrayMipMaps) → n = 0 \/ n = 1 \/ n = 2. Proof. intros n. simpl. intros H. destruct H; auto. destruct H; auto. destruct H; auto. contradiction H. Qed. Example exampleArrayMipMapsHaveSameLayers : ∀ level0 level1, arrayMipMapsHaveSameLayers exampleArrayMipMaps level0 level1. Proof. intros level0 level1. unfold arrayMipMapsHaveSameLayers. intros H_In0 H_In1. assert (level0 = 0 ∨ level0 = 1 ∨ level0 = 2) as Hl0 by (apply (exampleArrayMipMapsLevel level0 H_In0)). assert (level1 = 0 ∨ level1 = 1 ∨ level1 = 2) as Hl1 by (apply (exampleArrayMipMapsLevel level1 H_In1)). destruct Hl0 as [Heq0|Heq0]. { destruct Hl1 as [Heq1|Heq1]. { rewrite Heq0. rewrite Heq1. reflexivity. } destruct Heq1 as [Heq1_0|Heq1_0]. { rewrite Heq0. rewrite Heq1_0. reflexivity. } rewrite Heq0. rewrite Heq1_0. reflexivity. } destruct Heq0 as [Heq0_0|Heq0_0]. { rewrite Heq0_0. destruct Hl1 as [Heq1|Heq1]. { rewrite Heq1. reflexivity. } destruct Heq1 as [Heq1_0|Heq1_0]. { rewrite Heq1_0. reflexivity. } rewrite Heq1_0. reflexivity. } destruct Hl1 as [Heq1|Heq1]. { rewrite Heq0_0. rewrite Heq1. reflexivity. } destruct Heq1 as [Heq1_0|Heq1_0]. { rewrite Heq0_0. rewrite Heq1_0. reflexivity. } rewrite Heq0_0. rewrite Heq1_0. reflexivity. Qed.
Require Import Coq.Arith.PeanoNat. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Init.Byte. Require Import Coq.Bool.Bool. Require Import Coq.Program.Basics. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Alignment. Require Import Calino.Metadata. Require Import Calino.ArrayMipMap. Require Import Calino.CubeMipMap. Require Import Calino.MipMap. Require Import Calino.ImageInfo. Require Import Calino.Divisible8. Require Import Calino.StringUtility. Require Import Calino.Descriptor. Require Import Calino.ChannelDescription. Require Import Calino.ChannelSemantic. Require Import Calino.ChannelType. Require Import Calino.Compression. Require Import Calino.SuperCompression. Require Import Calino.ColorSpace. Require Import Calino.Flag. Require Import Calino.ByteOrder. Require Import Calino.CoordinateSystem. Require Import Calino.ImageSize. Import ListNotations. Open Scope program_scope. Open Scope string_scope. Set Mangle Names. Inductive streamE : Set := | Vu64 : nat → streamE | Vu32 : nat → streamE | Vu8 : nat → streamE. Definition u8byte : byte → streamE := Vu8 ∘ Byte.to_nat. Definition streamEIsU8 (e : streamE) : Prop := match e with | Vu64 _ => False | Vu32 _ => False | Vu8 _ => True end. Inductive streamWellFormed : list streamE → Prop := | BEPEmpty : streamWellFormed [] | BEPVu64 : ∀ k, streamWellFormed [Vu64 k] | BEPVu32 : ∀ k, streamWellFormed [Vu32 k] | BEPVu8s : ∀ es, Forall streamEIsU8 es → length (es) mod 4 = 0 → streamWellFormed es | BEPAppend : ∀ xs ys, streamWellFormed xs → streamWellFormed ys → streamWellFormed (xs ++ ys). Definition streamElementSize (s : streamE) : nat := match s with | Vu64 _ => 8 | Vu32 _ => 4 | Vu8 _ => 1 end. Definition streamSize (s : list streamE) : nat := fold_right plus 0 (map streamElementSize s). Section binaryExpressions. Local Unset Elimination Schemes. Inductive binaryExp : Set := | BiU32 : nat → binaryExp | BiU64 : nat → binaryExp | BiBytes : list byte → binaryExp | BiUTF8 : list byte → binaryExp | BiArray : list binaryExp → binaryExp | BiReserve : nat → binaryExp | BiRecord : list (string * binaryExp) → binaryExp. Section binaryExp_rect. Variable P : binaryExp → Type. Variable P_list : list binaryExp → Type. Hypothesis P_nil : P_list []. Hypothesis P_cons : ∀ x xs, P x → P_list xs → P_list (x :: xs). Hypothesis P_BiU32 : ∀ x, P (BiU32 x). Hypothesis P_BiU64 : ∀ x, P (BiU64 x). Hypothesis P_BiBytes : ∀ bs, P (BiBytes bs). Hypothesis P_BiUTF8 : ∀ bs, P (BiUTF8 bs). Hypothesis P_BiArray : ∀ bs, P_list bs → P (BiArray bs). Hypothesis P_BiReserve : ∀ x, P (BiReserve x). Hypothesis P_BiRecord : ∀ fs, P_list (map snd fs) → P (BiRecord fs). Fixpoint binaryExp_rect (b : binaryExp) : P b := let fix expForAll (xs : list binaryExp) : P_list xs := match xs as rxs return (P_list rxs) with | [] => @P_nil | (y :: ys) => @P_cons y ys (binaryExp_rect y) (expForAll ys) end in let fix forAllSnd (fs : list (string * binaryExp)) : P_list (map snd fs) := match fs as rf return P_list (map snd rf) with | [] => @P_nil | ((_, y) :: ys) => @P_cons y (map snd ys) (binaryExp_rect y) (forAllSnd ys) end in match b with | BiU32 c => P_BiU32 c | BiU64 c => P_BiU64 c | BiBytes bs => P_BiBytes bs | BiUTF8 bs => P_BiUTF8 bs | BiArray es => P_BiArray es (expForAll es) | BiReserve c => P_BiReserve c | BiRecord fs => P_BiRecord fs (forAllSnd fs) end. End binaryExp_rect. Section binaryExp_ind. Variable P : binaryExp → Prop. Hypothesis P_BiU32 : ∀ x, P (BiU32 x). Hypothesis P_BiU64 : ∀ x, P (BiU64 x). Hypothesis P_BiBytes : ∀ bs, P (BiBytes bs). Hypothesis P_BiUTF8 : ∀ bs, P (BiUTF8 bs). Hypothesis P_BiArray : ∀ bs, Forall P bs → P (BiArray bs). Hypothesis P_BiReserve : ∀ x, P (BiReserve x). Hypothesis P_BiRecord : ∀ fs, Forall P (map snd fs) → P (BiRecord fs). Definition binaryExp_ind (b : binaryExp) : P b := binaryExp_rect P (List.Forall P) (List.Forall_nil _) (λ x xs Px Pxs, List.Forall_cons _ Px Pxs) P_BiU32 P_BiU64 P_BiBytes P_BiUTF8 P_BiArray P_BiReserve P_BiRecord b. End binaryExp_ind. End binaryExpressions. Fixpoint binarySize (b : binaryExp) : nat := match b with | BiU32 _ => 4 | BiU64 _ => 8 | BiBytes s => 4 + asMultipleOf4 (length s) | BiUTF8 s => 4 + asMultipleOf4 (length s) | BiArray f => 4 + fold_right plus 0 (map binarySize f) | BiReserve s => asMultipleOf4 s | BiRecord f => fold_right plus 0 (map (binarySize ∘ snd) f) end. Definition binaryEvalPaddedBytes (b : list byte) (align : nat) (Hneq : 0 ≠ align) : list streamE := let vremaining := length b mod align in match vremaining with | 0 => map u8byte b | _ => map u8byte (b ++ repeat x00 (align - vremaining)) end. Fixpoint binaryEval (b : binaryExp) : list streamE := match b with | BiU32 k => [Vu32 k] | BiU64 k => [Vu64 k] | BiBytes s => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4) | BiUTF8 s => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4) | BiArray f => (Vu32 (length f)) :: concat (map binaryEval f) | BiReserve s => repeat (Vu8 0) (asMultipleOf4 s) | BiRecord f => concat (map (binaryEval ∘ snd) f) end. Definition binarySizePadded16 (b : binaryExp) : nat := asMultipleOf16 (binarySize b). Definition utf8 (s : string) : binaryExp := BiUTF8 (list_byte_of_string s). Definition u32 := BiU32. Definition u64 := BiU64. Definition binaryExpMipMap (m : mipMap) : binaryExp := BiRecord [ ("mipMapLevel", u32 (mipMapLevel m)); ("mipMapDataOffset", u64 (mipMapOffset m)); ("mipMapSizeUncompressed", u64 (mipMapSizeUncompressed m)); ("mipMapSizeCompressed", u64 (mipMapSizeCompressed m)); ("mipMapCRC32", u32 (mipMapCRC32 m)) ]. Remark binaryExpMipMapSize : ∀ m, binarySize (binaryExpMipMap m) = 32. Proof. reflexivity. Qed. Definition binaryExpMipMaps (m : mipMapList) : binaryExp := BiArray (map binaryExpMipMap (mipMaps m)). Definition binaryExpImage2D (i : imageInfo) (m : mipMapList) : binaryExp := let imageDataStart := mipMapOffset (mipMapFirst m) in let encMips := binaryExpMipMaps m in let encMipsSize := binarySize encMips in let encMipsPad := imageDataStart - encMipsSize in let imageSize := mipMapImageDataSizeTotal m in let imageSize16 := asMultipleOf16 imageSize in BiRecord [ ("mipMaps", encMips); ("mipPad", BiReserve encMipsPad); ("mipData", BiReserve imageSize16) ]. Definition binaryExpImage2DSection (i : imageInfo) (m : mipMapList) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F49324421); ("size", u64 (binarySizePadded16 (binaryExpImage2D i m))); ("data", binaryExpImage2D i m) ]. Definition binaryExpArrayMipMap (m : arrayMipMap) : binaryExp := BiRecord [ ("arrayMipMapLevel", u32 (arrayMipMapLevel (arrayMipMapIndex m))); ("arrayMipMapLayer", u32 (arrayMipMapLayer (arrayMipMapIndex m))); ("arrayMipMapDataOffset", u64 (arrayMipMapOffset m)); ("arrayMipMapSizeUncompressed", u64 (arrayMipMapSizeUncompressed m)); ("arrayMipMapSizeCompressed", u64 (arrayMipMapSizeCompressed m)); ("arrayMipMapCRC32", u32 (arrayMipMapCRC32 m)) ]. Remark binaryExpArrayMipMapSize : ∀ m, binarySize (binaryExpArrayMipMap m) = 36. Proof. reflexivity. Qed. Definition binaryExpArrayMipMaps (m : arrayMipMapList) : binaryExp := BiArray (map binaryExpArrayMipMap (arrayMipMaps m)). Definition binaryExpImageArray (i : imageInfo) (m : arrayMipMapList) : binaryExp := let imageDataStart := arrayMipMapOffset (arrayMipMapFirst m) in let encMips := binaryExpArrayMipMaps m in let encMipsSize := binarySize encMips in let encMipsPad := imageDataStart - encMipsSize in let imageSize := arrayMipMapImageDataSizeTotal m in let imageSize16 := asMultipleOf16 imageSize in BiRecord [ ("arrayMipMaps", encMips); ("arrayMipPad", BiReserve encMipsPad); ("arrayMipData", BiReserve imageSize16) ]. Definition binaryExpImageArraySection (i : imageInfo) (m : arrayMipMapList) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F41525221); ("size", u64 (binarySizePadded16 (binaryExpImageArray i m))); ("data", binaryExpImageArray i m) ]. Definition binaryExpCubeMipMapFace (m : cubeMapFace) : binaryExp := BiRecord [ ("cubeFaceDataOffset", u64 (cubeFaceOffset m)); ("cubeFaceSizeUncompressed", u64 (cubeFaceSizeUncompressed m)); ("cubeFaceSizeCompressed", u64 (cubeFaceSizeCompressed m)); ("cubeFaceCRC32", u32 (cubeFaceCRC32 m)) ]. Remark binaryExpCubeMipMapFaceSize : ∀ m, binarySize (binaryExpCubeMipMapFace m) = 28. Proof. reflexivity. Qed. Definition binaryExpCubeMipMap (m : cubeMipMap) : binaryExp := BiRecord [ ("cubeMipMapLevel", u32 (cubeMapLevel m)); ("cubeMipMapFacePosX", binaryExpCubeMipMapFace (cubeMapFaceXPos m)); ("cubeMipMapFaceNegX", binaryExpCubeMipMapFace (cubeMapFaceXNeg m)); ("cubeMipMapFacePosY", binaryExpCubeMipMapFace (cubeMapFaceYPos m)); ("cubeMipMapFaceNegY", binaryExpCubeMipMapFace (cubeMapFaceYNeg m)); ("cubeMipMapFacePosZ", binaryExpCubeMipMapFace (cubeMapFaceZPos m)); ("cubeMipMapFaceNegZ", binaryExpCubeMipMapFace (cubeMapFaceZNeg m)) ]. Remark binaryExpCubeMipMapSize : ∀ m, binarySize (binaryExpCubeMipMap m) = 172. Proof. reflexivity. Qed. Definition binaryExpCubeMipMaps (m : cubeMipMapList) : binaryExp := BiArray (map binaryExpCubeMipMap (cubeMipMaps m)). Definition binaryExpImageCubeMap (i : imageInfo) (m : cubeMipMapList) : binaryExp := let imageDataStart := cubeFaceOffset (cubeMapFaceXPos (cubeMipMapsFirst m)) in let encMips := binaryExpCubeMipMaps m in let encMipsSize := binarySize encMips in let encMipsPad := imageDataStart - encMipsSize in let imageSize := cubeMipMapImageDataSizeTotal m in let imageSize16 := asMultipleOf16 imageSize in BiRecord [ ("cubeMipMaps", encMips); ("cubeMipPad", BiReserve encMipsPad); ("cubeMipData", BiReserve imageSize16) ]. Definition binaryExpImageCubeSection (i : imageInfo) (m : cubeMipMapList) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F43554245); ("size", u64 (binarySizePadded16 (binaryExpImageCubeMap i m))); ("data", binaryExpImageCubeMap i m) ]. Definition binaryExpCompression (c : compressionMethod) : binaryExp := BiRecord [ ("descriptor", utf8 (descriptorOf c)); ("sectionIdentifier", u64 (compressionSectionIdentifier c)); ("blockSizeX", u32 (compressionBlockSizeX c)); ("blockSizeY", u32 (compressionBlockSizeY c)); ("blockAlignment", u32 (compressionBlockAlignment c)) ]. Definition binaryExpSuperCompression (c : superCompressionMethod) : binaryExp := BiRecord [ ("descriptor", utf8 (descriptorOf c)); ("sectionIdentifier", u64 (superCompressionSectionIdentifier c)) ]. Definition binaryExpImageInfo (i : imageInfo) : binaryExp := BiRecord [ ("sizeX", u32 (imageSizeX i)); ("sizeY", u32 (imageSizeY i)); ("sizeZ", u32 (imageSizeZ i)); ("channelsLayout", utf8 (descriptorOf (imageChannelsLayout i))); ("channelsType", utf8 (descriptorOf (imageChannelsType i))); ("compression", binaryExpCompression (imageCompressionMethod i)); ("superCompression", binaryExpSuperCompression (imageSuperCompressionMethod i)); ("coordinateSystem", utf8 (descriptorOf (imageCoordinateSystem i))); ("colorSpace", utf8 (descriptorOf (imageColorSpace i))); ("flags", BiArray (map (utf8 ∘ descriptorOf) (imageFlagSet i))); ("byteOrder", utf8 (descriptorOf (imageByteOrder i))) ]. Definition binaryExpFileHeader : binaryExp := BiRecord [ ("id", u64 0x89434C4E0D0A1A0A); ("versionMajor", u32 1); ("versionMinor", u32 0) ]. Definition binaryExpImageInfoSection (i : imageInfo) : binaryExp := BiRecord [ ("id", u64 0x434C4E49494E464F); ("size", u64 (binarySizePadded16 (binaryExpImageInfo i))); ("data", binaryExpImageInfo i) ]. Definition binaryExpMetadataValue (m : metadataValue) : binaryExp := BiRecord [ ("key", utf8 (mKey m)); ("value", utf8 (mValue m)) ]. Definition binaryExpMetadata (m : metadata) : binaryExp := BiArray (map binaryExpMetadataValue (mValues m)). Definition binaryExpMetadataSection (m : metadata) : binaryExp := BiRecord [ ("id", u64 0x434C4E5F4D455441); ("size", u64 (binarySizePadded16 (binaryExpMetadata m))); ("data", binaryExpMetadata m) ]. Definition binaryEndSection : binaryExp := BiRecord [ ("id", u64 0x434c4e5f454e4421); ("size", u64 0) ]. Lemma fold_right_add_cons : ∀ x xs, x + fold_right plus 0 xs = fold_right plus 0 (x :: xs). Proof. reflexivity. Qed. Lemma forall_map_binarySize : ∀ es, Forall (λ b : binaryExp, binarySize b mod 4 = 0) es ↔ Forall (λ n, n mod 4 = 0) (map binarySize es). Proof. intros es. induction es. constructor. - rewrite Forall_map. intros H. trivial. - rewrite Forall_map. intros H. trivial. - rewrite Forall_map. constructor. intros H; trivial. intros H; trivial. Qed. Theorem binarySizeMultiple4 : ∀ b, binarySize (b) mod 4 = 0. Proof. intros b. induction b as [Hbu32|Hbu64|Hbbyte|Hbutf|xs HFA|Hbuns|xs HFF] using binaryExp_ind. (* U32 values are of size 4 *) - reflexivity. (* U64 values are of size 8 *) - reflexivity. (* Byte array values are rounded up to a multiple of 4 and prefixed with 4 *) - unfold binarySize. unfold asMultipleOf4. remember (asMultipleOf (Datatypes.length Hbbyte) 4 p0not4) as size eqn:Heqsize. rewrite Nat.add_comm. rewrite <- (Nat.add_mod_idemp_l size 4 4 (Nat.neq_sym _ _ p0not4)). assert (size mod 4 = 0) as Hm0. { rewrite Heqsize. apply (asMultipleOfMod (Datatypes.length Hbbyte) 4 (p0not4)). } rewrite Hm0. reflexivity. (* UTF-8 values are rounded up to a multiple of 4 and prefixed with 4 *) - unfold binarySize. unfold asMultipleOf4. remember (asMultipleOf (Datatypes.length Hbutf) 4 p0not4) as size eqn:Heqsize. rewrite Nat.add_comm. rewrite <- (Nat.add_mod_idemp_l size 4 4 (Nat.neq_sym _ _ p0not4)). assert (size mod 4 = 0) as Hm0. { rewrite Heqsize. apply (asMultipleOfMod (Datatypes.length Hbutf) 4 (p0not4)). } rewrite Hm0. reflexivity. (* Each element of an array is a multiple of 4, so the entire array is too. *) - unfold binarySize. fold binarySize. induction xs as [|y ys HforAllInd]. -- reflexivity. -- assert (fold_right add 0 (map binarySize (y :: ys)) mod 4 = 0) as HfoldEq. { apply (@divisibilityNFoldPlus 4 (map binarySize (y :: ys))). discriminate. rewrite <- forall_map_binarySize. exact HFA. } rewrite map_cons. rewrite map_cons in HfoldEq. assert (4 mod 4 = 0) as H4mod40 by (reflexivity). assert (0 ≠ 4) as H0n4 by (discriminate). apply (divisiblityNAdd 4 (fold_right add 0 (binarySize y :: map binarySize ys)) 4 H0n4 H4mod40 HfoldEq). (* Unspecified values are rounded up. *) - unfold binarySize. unfold asMultipleOf4. rewrite asMultipleOfMod. reflexivity. (* Each element of an record is a multiple of 4, so the entire record is too. *) - unfold binarySize. fold binarySize. induction xs as [|y ys HforAllInd]. -- reflexivity. -- rewrite map_cons. rewrite map_cons in HFF. rewrite <- fold_right_add_cons. apply divisiblityNAdd. discriminate. apply (Forall_inv HFF). apply HforAllInd. apply (Forall_inv_tail HFF). Qed. Lemma sub_0_lt_ymx : ∀ x y, 0 <= x → x < y → 0 < y - x. Proof. intros x y Hle Hlt. destruct x as [|a]. - rewrite Nat.sub_0_r. exact Hlt. - rewrite <- Nat.lt_add_lt_sub_l. rewrite Nat.add_0_r. exact Hlt. Qed. Lemma mod_sub : ∀ x m, 0 < m → 0 < m - (x mod m) <= m. Proof. intros x m Hlt. constructor. - assert (0 <= x mod m < m) as HmRange. { apply Nat.mod_bound_pos. apply Nat.le_0_l. exact Hlt. } destruct HmRange as [HA HB]. remember (x mod m) as y. apply (sub_0_lt_ymx y m HA HB). - assert (x mod m < m) as HmRange. { apply Nat.mod_upper_bound. apply Nat.neq_sym. apply Nat.lt_neq. exact Hlt. } apply Nat.le_sub_l. Qed. Lemma mod_opposition : ∀ x a, 0 ≠ a → x mod a + (a - x mod a) = a. Proof. intros x a Hnz. assert (x mod a < a) as Hxma. { apply (Nat.mod_upper_bound). apply Nat.neq_sym. exact Hnz. } remember (x mod a) as y eqn:Heqy. apply Minus.le_plus_minus_r. apply (Nat.lt_le_incl _ _ Hxma). Qed. Theorem binaryEvalPaddedBytesAligned : ∀ bs a (Hnz : 0 ≠ a), length (binaryEvalPaddedBytes bs a Hnz) mod a = 0. Proof. intros bs a Hnz. unfold binaryEvalPaddedBytes. destruct (Datatypes.length bs mod a) eqn:Hlen. - rewrite map_length. exact Hlen. - rewrite map_length. rewrite app_length. rewrite repeat_length. rewrite <- Hlen. remember (Datatypes.length bs) as x. rewrite <- (Nat.add_mod_idemp_l x (a - x mod a) a). assert ((x mod a + (a - x mod a)) = a) as Heqa. { rewrite (mod_opposition x a Hnz). reflexivity. } rewrite Heqa. apply Nat.mod_same. apply Nat.neq_sym; exact Hnz. apply Nat.neq_sym; exact Hnz. Qed. Lemma repeat_eq : ∀ (A : Type) (P : A → Prop) (n : nat) (x : A), Forall (eq x) (repeat x n). Proof. intros A P n x. induction n as [|m Hm]. - constructor. - simpl. constructor. reflexivity. exact Hm. Qed. Lemma Forall_implies : ∀ (A : Type) (P : A → Prop) (Q : A → Prop) (xs : list A) (H : ∀ x, P x → Q x), Forall P xs → Forall Q xs. Proof. intros A P Q xs Ht HforAll. induction HforAll as [|y ys Hpy HfaP HfaQ]. - constructor. - constructor. apply (Ht y Hpy). exact HfaQ. Qed. Theorem binaryEvalPaddedBytesU8 : ∀ bs a (Hnz : 0 ≠ a), Forall streamEIsU8 (binaryEvalPaddedBytes bs a Hnz). Proof. intros bs a Hnz. unfold binaryEvalPaddedBytes. destruct (Datatypes.length bs mod a) as [|HB]. - rewrite Forall_map. induction bs as [|r rs Hrs]. -- constructor. -- constructor. reflexivity. exact Hrs. - rewrite map_app. assert (Forall streamEIsU8 (map u8byte bs)) as Hmap. { rewrite Forall_map. induction bs as [|r rs Hrs]. - constructor. - constructor. reflexivity. exact Hrs. } assert (Forall streamEIsU8 (map u8byte (repeat "000"%byte (a - S HB)))) as HmapR. { rewrite Forall_map. assert (Forall (eq "000"%byte) (repeat "000"%byte (a - S HB))) as Hfeq by (apply (repeat_eq byte (λ _ : byte, True) (a - S HB) "000"%byte)). simpl. apply (@Forall_implies byte (eq "000"%byte) (λ _ : byte, True) (repeat "000"%byte (a - S HB))). { intros. exact I. } exact Hfeq. } apply Forall_app. constructor. exact Hmap. exact HmapR. Qed. Lemma app_cons : ∀ (A : Type) (x : A) (xs : list A), x :: xs = app (cons x nil) xs. Proof. intros A x xs. reflexivity. Qed. Theorem binaryEvalStreamsWellFormed : ∀ b, streamWellFormed (binaryEval b). Proof. intros b. induction b as [a0|a1|a2|a3|a4 Hfa|a5|a6 Hfa]. (* U32 *) - apply BEPVu32. (* U64 *) - apply BEPVu64. (* Bytes *) - unfold binaryEval. rewrite app_cons. apply BEPAppend. apply BEPVu32. assert (length (binaryEvalPaddedBytes a2 4 p0not4) mod 4 = 0) as Hlm by (apply (binaryEvalPaddedBytesAligned)). apply BEPVu8s. apply binaryEvalPaddedBytesU8. exact Hlm. (* UTF-8 *) - unfold binaryEval. rewrite app_cons. apply BEPAppend. apply BEPVu32. assert (length (binaryEvalPaddedBytes a3 4 p0not4) mod 4 = 0) as Hlm by (apply (binaryEvalPaddedBytesAligned)). assert (Forall streamEIsU8 (binaryEvalPaddedBytes a3 4 p0not4)) as Hu8 by (apply (binaryEvalPaddedBytesU8)). apply (BEPVu8s _ Hu8 Hlm). (* Array *) - simpl. rewrite app_cons. apply BEPAppend. apply BEPVu32. induction a4 as [|q qs IHqs]. -- constructor. -- assert (streamWellFormed (concat (map binaryEval qs))) as HqsWF by (apply (IHqs (Forall_inv_tail Hfa))). assert (streamWellFormed (binaryEval q)) as HqWF by (apply (Forall_inv Hfa)). simpl. apply BEPAppend. exact HqWF. exact HqsWF. (* Reserve *) - simpl. unfold asMultipleOf4. remember (asMultipleOf a5 4 p0not4) as size eqn:Heqsize. assert (size mod 4 = 0) as Heqm. { rewrite Heqsize. apply (asMultipleOfMod). } assert ((Vu8 ∘ Byte.to_nat) "000"%byte = (Vu8 0)) as HbyteEq by reflexivity. apply BEPVu8s. assert (Forall (eq (Vu8 0)) (repeat (Vu8 0) size)) as Hfeq by (apply (@repeat_eq streamE streamEIsU8 size (Vu8 0))). apply (@Forall_implies streamE (eq (Vu8 0)) streamEIsU8 (repeat (Vu8 0) size)). { intros x Hxeq. unfold streamEIsU8. rewrite <- Hxeq. exact I. } exact Hfeq. rewrite repeat_length. exact Heqm. (* Record *) - simpl. induction a6 as [|q qs IHqs]. -- constructor. -- assert (Forall (λ b : binaryExp, streamWellFormed (binaryEval b)) (map snd qs)) as Hfqs. { apply (@Forall_inv_tail binaryExp (λ b : binaryExp, streamWellFormed (binaryEval b)) (snd q) (map snd qs)). { assert ((map snd (q :: qs)) = (snd q :: map snd qs)) as Hmc by reflexivity. rewrite <- Hmc. exact Hfa. } } assert (streamWellFormed (concat (map (binaryEval ∘ snd) qs))) as Hconqs by (apply (IHqs Hfqs)). rewrite map_cons. rewrite concat_cons. apply BEPAppend. rewrite map_cons in Hfa. apply (Forall_inv Hfa). exact Hconqs. Qed. Unset Mangle Names. Lemma fold_right_1_length : ∀ xs, Forall (eq 1) xs → fold_right add 0 xs = length xs. Proof. intros xs Hfa. induction xs as [|y ys IHxs]. - reflexivity. - rewrite <- fold_right_add_cons. assert (length (y :: ys) = 1 + length (ys)) as HlenYs by reflexivity. rewrite HlenYs. assert (1 = y) as Hy1 by (apply (Forall_inv Hfa)). rewrite <- Hy1. f_equal. apply IHxs. apply (Forall_inv_tail Hfa). Qed. Theorem fold_right_add_app : ∀ xs ys, fold_right add 0 xs + fold_right add 0 ys = fold_right add 0 (xs ++ ys). Proof. intros xs ys. rewrite fold_right_app. generalize dependent ys. induction xs as [|q qs IHqs]. - reflexivity. - intros ys. simpl. rewrite <- (IHqs ys). rewrite Nat.add_assoc. reflexivity. Qed. Theorem streamSizeApp : ∀ xs ys, streamSize xs + streamSize ys = streamSize (xs ++ ys). Proof. intros xs ys. unfold streamSize. rewrite map_app. rewrite fold_right_add_app. reflexivity. Qed. Theorem streamsWellFormedDivisible4 : ∀ es, streamWellFormed es → streamSize es mod 4 = 0. Proof. intros es Hwf. induction Hwf as [|H1|H2|es Hfa Hsize|xs ys Hxswf Hxsize Hyswf Hysize]. - reflexivity. - reflexivity. - reflexivity. - unfold streamSize. assert (Forall (λ e, 1 = streamElementSize e) es) as HFaSize. { apply (@Forall_implies streamE streamEIsU8 (λ e : streamE, 1 = streamElementSize e) es). { intros x His. destruct x as [u64|u32|u8]. - contradiction. - contradiction. - reflexivity. } exact Hfa. } assert (Forall (eq 1) (map streamElementSize es)) as Hall1. { apply (@Forall_map _ _ _ _ es). exact HFaSize. } assert (fold_right add 0 (map streamElementSize es) = length es) as HlenEq. { assert (length es = length (map streamElementSize es)) as HmapLen. { rewrite map_length. reflexivity. } rewrite HmapLen. apply (fold_right_1_length (map streamElementSize es) Hall1). } rewrite HlenEq. exact Hsize. - rewrite <- streamSizeApp. apply divisiblityNAdd. discriminate. exact Hxsize. exact Hysize. Qed.
Require Import Coq.Arith.PeanoNat. Require Import Coq.Lists.List. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Divisible8. Require Import Calino.Descriptor. Import ListNotations. Inductive byteOrder : Set := | ByteOrderBig | ByteOrderLittle. Inductive bit : Set := | B0 | B1. Inductive octet : Set := | OctExact : bit → bit → bit → bit → bit → bit → bit → bit → octet | OctRemain : bit → bit → bit → bit → bit → bit → bit → bit → octet. Definition octetIsRemainder (o : octet): Prop := match o with | OctExact _ _ _ _ _ _ _ _ => False | OctRemain _ _ _ _ _ _ _ _ => True end. Definition octetIsExact (o : octet): Prop := match o with | OctExact _ _ _ _ _ _ _ _ => True | OctRemain _ _ _ _ _ _ _ _ => False end. Lemma octetIsRemainderNotExact : ∀ (o : octet), octetIsRemainder o → ¬octetIsExact o. Proof. intros o Hrem Hfalse. destruct o; contradiction. Qed. Lemma octetIsExactNotRemainder : ∀ (o : octet), octetIsExact o → ¬octetIsRemainder o. Proof. intros o Hrem Hfalse. destruct o; contradiction. Qed. Inductive bitsOctetsHasRemainder : list octet → Prop := | BOHasRemainder : ∀ (prefix : list octet) (o : octet), Forall octetIsExact prefix → octetIsRemainder o → bitsOctetsHasRemainder (prefix ++ o :: []). Fixpoint octetsBigEndianAux (bits : list bit) (octets : list octet) : list octet := match bits with | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) => octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: b4 :: rest) => octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: b5 :: rest) => octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: b6 :: rest) => octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | (b7 :: rest) => octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest [] | [] => octets end. Definition octetsBigEndian (bits : list bit) : list octet := octetsBigEndianAux bits []. Definition octetsLittleEndian (bits : list bit) : list octet := rev (octetsBigEndianAux bits []). Definition listInduction8 : ∀ (A : Type), ∀ (P : list A → Prop), P [] → (∀ (b0 : A), P (b0 :: [])) → (∀ (b1 b0 : A), P (b1 :: b0 :: [])) → (∀ (b2 b1 b0 : A), P (b2 :: b1 :: b0 :: [])) → (∀ (b3 b2 b1 b0 : A), P (b3 :: b2 :: b1 :: b0 :: [])) → (∀ (b4 b3 b2 b1 b0 : A), P (b4 :: b3 :: b2 :: b1 :: b0 :: [])) → (∀ (b5 b4 b3 b2 b1 b0 : A), P (b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) → (∀ (b6 b5 b4 b3 b2 b1 b0 : A), P (b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) → (∀ (b7 b6 b5 b4 b3 b2 b1 b0 : A) (rest : list A), P rest → P (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest)) → ∀ (L : list A), P L := λ A P P0 P1 P2 P3 P4 P5 P6 P7 P8, fix f (l : list A) := match l with | [] => P0 | x0 :: [] => P1 x0 | (x0 :: x1 :: []) => P2 x0 x1 | (x0 :: x1 :: x2 :: []) => P3 x0 x1 x2 | (x0 :: x1 :: x2 :: x3 :: []) => P4 x0 x1 x2 x3 | (x0 :: x1 :: x2 :: x3 :: x4 :: []) => P5 x0 x1 x2 x3 x4 | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: []) => P6 x0 x1 x2 x3 x4 x5 | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: []) => P7 x0 x1 x2 x3 x4 x5 x6 | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: rest) => P8 x0 x1 x2 x3 x4 x5 x6 x7 rest (f rest) end. Lemma app_non_empty : ∀ (A : Type) (xs : list A) (y : A), xs ++ [y] ≠ []. Proof. intros A xs y. unfold not. destruct xs as [|z zs]. intros Hfalse; inversion Hfalse. intros Hfalse; inversion Hfalse. Qed. Lemma app_list_implies_eq : ∀ (A : Type) (x y : A) (xs : list A), xs ++ [x] = [y] → xs = [] ∧ x = y. Proof. intros A x y xs Happ. induction xs as [|z zs] eqn:Hxe. - constructor. reflexivity. rewrite (app_nil_l [x]) in Happ. injection Happ as Heq; exact Heq. - inversion Happ. assert (zs ++ [x] ≠ []) by (apply app_non_empty). contradiction. Qed. Lemma p8notZ : 8 ≠ 0. Proof. discriminate. Qed. Lemma list_mod8_0 : ∀ (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A), divisible8 (length xs) → divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)). Proof. intros A xs n7 n6 n5 n4 n3 n2 n1 n0 Hlen8. unfold divisible8 in *. assert (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs = (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: []) ++ xs) as HlistEq by reflexivity. rewrite HlistEq. rewrite app_length. assert (length [n7; n6; n5; n4; n3; n2; n1; n0] = 8) as Hprefix8 by reflexivity. rewrite Hprefix8. rewrite <- (Nat.add_mod_idemp_l 8 (length xs) 8 p8notZ). rewrite (Nat.mod_same 8 p8notZ). rewrite (Nat.add_0_l). exact Hlen8. Qed. Lemma list_mod8_1 : ∀ (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A), divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)) → divisible8 (length xs). Proof. intros A xs n7 n6 n5 n4 n3 n2 n1 n0 Hlen8. unfold divisible8 in *. assert (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs = (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: []) ++ xs) as HlistEq by reflexivity. rewrite HlistEq in Hlen8. rewrite app_length in Hlen8. assert (length [n7; n6; n5; n4; n3; n2; n1; n0] = 8) as Hprefix8 by reflexivity. rewrite Hprefix8 in Hlen8. rewrite <- (Nat.add_mod_idemp_l 8 (length xs) 8 p8notZ) in Hlen8. rewrite (Nat.mod_same 8 p8notZ) in Hlen8. rewrite (Nat.add_0_l) in Hlen8. exact Hlen8. Qed. Theorem list_mod8 : ∀ (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A), divisible8 (length xs) ↔ divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)). Proof. intros A xs n7 n6 n5 n4 n3 n2 n1 n0. constructor. - apply list_mod8_0. - apply list_mod8_1. Qed. Theorem octetsBigEndianLengthDivisibleAllExact : ∀ (b : list bit), divisible8 (length b) → Forall octetIsExact (octetsBigEndian b). Proof. intros b Hlen8. unfold octetsBigEndian. induction b using listInduction8. - constructor. - inversion Hlen8. - inversion Hlen8. - inversion Hlen8. - inversion Hlen8. - inversion Hlen8. - inversion Hlen8. - inversion Hlen8. - simpl. rewrite <- list_mod8 in Hlen8. assert (Forall octetIsExact (octetsBigEndianAux b [])) as HallExact by (apply (IHb Hlen8)). assert (octetIsExact (OctExact b7 b6 b5 b4 b3 b2 b1 b0)) as Hexact by constructor. apply (@Forall_cons octet octetIsExact (OctExact b7 b6 b5 b4 b3 b2 b1 b0) (octetsBigEndianAux b []) Hexact HallExact). Qed. Theorem octetsLittleEndianLengthDivisibleAllExact : ∀ (b : list bit), divisible8 (length b) → Forall octetIsExact (octetsLittleEndian b). Proof. intros b Hlen8. apply (Forall_rev (octetsBigEndianLengthDivisibleAllExact b Hlen8)). Qed. Theorem octetsBigEndianLengthDivisibleNoRemainder : ∀ (b : list bit), Forall octetIsExact (octetsBigEndian b) → ¬ bitsOctetsHasRemainder (octetsBigEndian b). Proof. intros b HallExact. unfold octetsBigEndian. intro Hfalse. inversion Hfalse as [prefix o HprefixAllExact HoIsRemainder HprefixEq]. unfold octetsBigEndian in HallExact. (* We know that everything in the list is exact. *) (* We can show that o must be in this list according to HprefixEq. *) assert (In o (octetsBigEndianAux b [])) as HoInB. { assert (In o (prefix ++ [o])) as HoInPrefix by (apply (in_elt o prefix [])). rewrite HprefixEq in HoInPrefix. exact HoInPrefix. } (* And because o is in the list, it must be exact. *) assert (octetIsExact o) as HoIsExact. { rewrite Forall_forall in HallExact. apply (HallExact o HoInB). } (* There is a contradiction; o cannot be both exact and a remainder. *) apply (octetIsExactNotRemainder o HoIsExact HoIsRemainder). Qed. Lemma mod_8_lt_0 : ∀ (m : nat), 0 < m mod 8 → 0 < (m + 8) mod 8. Proof. intros m Hlt. rewrite (Nat.add_mod m 8 8). rewrite (Nat.mod_same). rewrite (Nat.add_0_r). rewrite (Nat.mod_mod). exact Hlt. discriminate. discriminate. discriminate. Qed. Lemma mod_8_lt_1 : ∀ (m : nat), 0 < (m + 8) mod 8 -> 0 < m mod 8. Proof. intros m Hlt. rewrite (Nat.add_mod m 8 8) in Hlt. rewrite (Nat.mod_same) in Hlt. rewrite (Nat.add_0_r) in Hlt. rewrite (Nat.mod_mod) in Hlt. exact Hlt. discriminate. discriminate. discriminate. Qed. Lemma mod_8_lt : ∀ (m : nat), 0 < (m + 8) mod 8 ↔ 0 < m mod 8. Proof. constructor. apply mod_8_lt_1. apply mod_8_lt_0. Qed. Theorem octetsBigEndianLengthIndivisibleRemainder : ∀ (b : list bit), 0 < length b mod 8 → ∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o. Proof. intros b Hlength. induction b using listInduction8. - inversion Hlength. - exists (OctRemain b0 B0 B0 B0 B0 B0 B0 B0). constructor. left. reflexivity. constructor. - exists (OctRemain b1 b0 B0 B0 B0 B0 B0 B0). constructor. left. constructor. constructor. - exists (OctRemain b2 b1 b0 B0 B0 B0 B0 B0). constructor. left. constructor. constructor. - exists (OctRemain b3 b2 b1 b0 B0 B0 B0 B0). constructor. left. constructor. constructor. - exists (OctRemain b4 b3 b2 b1 b0 B0 B0 B0). constructor. left. constructor. constructor. - exists (OctRemain b5 b4 b3 b2 b1 b0 B0 B0). constructor. left. constructor. constructor. - exists (OctRemain b6 b5 b4 b3 b2 b1 b0 B0). constructor. left. constructor. constructor. - assert (0 < length b mod 8) as Hlt. { assert (length (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: b) = length b + 8) as Heq by (rewrite Nat.add_comm; reflexivity). rewrite Heq in Hlength. rewrite <- (mod_8_lt (length b)). exact Hlength. } assert (∃ o : octet, In o (octetsBigEndian b) ∧ octetIsRemainder o) as HEx by (apply (IHb Hlt)). destruct HEx as [ox [HoxIn HoxRem]]. simpl. exists ox. constructor. right. exact HoxIn. exact HoxRem. Qed. Theorem octetsLittleEndianLengthIndivisibleRemainder : ∀ (b : list bit), 0 < length b mod 8 → ∃ o, In o (octetsLittleEndian b) ∧ octetIsRemainder o. Proof. unfold octetsLittleEndian. intros b Hlen. assert (∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o) as Hexists by (apply (octetsBigEndianLengthIndivisibleRemainder b Hlen)). destruct Hexists as [ox [HoxIn HoxRem]]. exists ox. rewrite <- (in_rev (octetsBigEndianAux b [])). constructor. exact HoxIn. exact HoxRem. Qed. Require Import Coq.Strings.String. Definition byteOrderDescribe (b : byteOrder) : descriptor := match b with | ByteOrderBig => "BIG_ENDIAN" | ByteOrderLittle => "LITTLE_ENDIAN" end. #[export] Instance byteOrderDescribable : describable byteOrder := { descriptorOf f := byteOrderDescribe f }.
Require Import Coq.Arith.PeanoNat. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Unicode.Utf8_core. Require Import Calino.ChannelSemantic. Require Import Calino.Descriptor. Require Import Calino.StringUtility. Require Import Calino.Divisible8. Import ListNotations. Set Mangle Names. Inductive channelDescription : Set := channelDescriptionMake { cdSemantic : channelSemantic; cdBits : nat; cdBitsNonzero : 0 ≠ cdBits }. Definition channelDescriptionDescribe (c : channelDescription) : descriptor := descriptorOf (cdSemantic c) ++ stringOfNat (cdBits c). #[export] Instance channelDescriptionDescribable : describable channelDescription := { descriptorOf c := channelDescriptionDescribe c }. Fixpoint channelDescriptionsDescribe (c : list channelDescription) : descriptor := match c with | nil => "" | cons d nil => channelDescriptionDescribe d | cons d e => (channelDescriptionDescribe d) ++ ":" ++ (channelDescriptionsDescribe e) end. Inductive channelLayoutPacking : Set := | CLPack8 | CLPack16 | CLPack32 | CLPack64. Definition channelLayoutPackingBits (c : channelLayoutPacking) : nat := match c with | CLPack8 => 8 | CLPack16 => 16 | CLPack32 => 32 | CLPack64 => 64 end. Theorem channelLayoutPackingBitsDiv8 : ∀ c, divisible8 (channelLayoutPackingBits (c)). Proof. intros c. destruct c; reflexivity. Qed. Definition channelLayoutPackingDescribe (c : channelLayoutPacking) : descriptor := match c with | CLPack8 => "p8" | CLPack16 => "p16" | CLPack32 => "p32" | CLPack64 => "p64" end. #[export] Instance channelLayoutPackingDescribable : describable channelLayoutPacking := { descriptorOf c := channelLayoutPackingDescribe c }. Definition channelDescriptionBitsDivisible8 (c : channelDescription) : Prop := divisible8 (cdBits c). Fixpoint channelDescriptionsBitsTotal (c : list channelDescription) : nat := match c with | nil => 0 | (x :: rest) => (cdBits x) + (channelDescriptionsBitsTotal rest) end. Lemma natAddNonzero : ∀ (n m : nat), 0 ≠ n → 0 ≠ m + n. Proof. intros n m HnZ. destruct m; simpl; auto. Qed. Lemma channelDescriptionsBitsNonEmptyNonZero : ∀ (c : list channelDescription), nil ≠ c → 0 ≠ channelDescriptionsBitsTotal c. Proof. intros c HnotNil. induction c as [|a b]. { contradiction. } { simpl. assert (0 ≠ cdBits a) as HbitsNZ by apply (cdBitsNonzero a). assert (0 ≠ channelDescriptionsBitsTotal b + cdBits a) as Hnz2. { apply natAddNonzero. exact HbitsNZ. } rewrite (Nat.add_comm) in Hnz2. exact Hnz2. } Qed. Inductive channelLayoutDescriptionUnpacked : Set := CLDUMake { uChannels : list channelDescription; uChannelsNonEmpty : [] ≠ uChannels; uInvariants : Forall channelDescriptionBitsDivisible8 uChannels; }. Definition channelLayoutDescriptionUnpackedDescribe (c : channelLayoutDescriptionUnpacked) : descriptor := channelDescriptionsDescribe (uChannels c). #[export] Instance channelLayoutDescriptionUnpackedDescribable : describable channelLayoutDescriptionUnpacked := { descriptorOf c := channelLayoutDescriptionUnpackedDescribe c }. Inductive channelLayoutDescriptionPacked : Set := CLDPMake { pChannels : list channelDescription; pChannelsNonEmpty : [] ≠ pChannels; pPacking : channelLayoutPacking; pInvariants : channelDescriptionsBitsTotal pChannels = channelLayoutPackingBits pPacking }. Definition channelLayoutDescriptionPackedDescribe (c : channelLayoutDescriptionPacked) : descriptor := let packing := descriptorOf (pPacking c) in let channels := channelDescriptionsDescribe (pChannels c) in packing ++ "|" ++ channels. #[export] Instance channelLayoutDescriptionPackedDescribable : describable channelLayoutDescriptionPacked := { descriptorOf c := channelLayoutDescriptionPackedDescribe c }. Inductive channelLayoutDescription : Set := | ChannelLayoutDescriptionUnpacked : channelLayoutDescriptionUnpacked → channelLayoutDescription | ChannelLayoutDescriptionPacked : channelLayoutDescriptionPacked → channelLayoutDescription. Definition channelLayoutDescriptionDescribe (c : channelLayoutDescription) : descriptor := match c with | ChannelLayoutDescriptionPacked p => descriptorOf p | ChannelLayoutDescriptionUnpacked u => descriptorOf u end. #[export] Instance channelLayoutDescriptionDescribable : describable channelLayoutDescription := { descriptorOf c := channelLayoutDescriptionDescribe c }. Definition channelLayoutDescriptionBits (c : channelLayoutDescription) : nat := match c with | ChannelLayoutDescriptionUnpacked u => channelDescriptionsBitsTotal (uChannels u) | ChannelLayoutDescriptionPacked p => channelDescriptionsBitsTotal (pChannels p) end. Lemma channelLayoutDescriptionBitsAdd : ∀ d ds, channelDescriptionsBitsTotal (d :: ds) = (cdBits d) + (channelDescriptionsBitsTotal ds). Proof. intros d ds. reflexivity. Qed. Theorem channelLayoutDescriptionBitsDivisible8 : ∀ (c : channelLayoutDescription), divisible8 (channelLayoutDescriptionBits c). Proof. intros c. destruct c as [u|p]. { assert (Forall channelDescriptionBitsDivisible8 (uChannels u)) as Hf8 by (apply uInvariants). unfold channelLayoutDescriptionBits. induction (uChannels u) as [|d ds IHu]. { reflexivity. } { rewrite channelLayoutDescriptionBitsAdd. assert (divisible8 (channelDescriptionsBitsTotal ds)) as Hdsdiv8. { assert (Forall channelDescriptionBitsDivisible8 ds) as Hfac by (apply (Forall_inv_tail (a := d) (l := ds) Hf8)). apply (IHu Hfac). } assert (divisible8 (cdBits d)) as Hdivbits by (apply (Forall_inv (a := d) (l := ds) Hf8)). apply (divisiblity8Add (cdBits d) (channelDescriptionsBitsTotal ds) Hdivbits Hdsdiv8). } } { simpl. assert (channelDescriptionsBitsTotal (pChannels p) = channelLayoutPackingBits (pPacking p)) as Hbeq by (apply pInvariants). rewrite Hbeq. apply channelLayoutPackingBitsDiv8. } Qed. Theorem channelLayoutDescriptionBitsLe8 : ∀ (c : channelLayoutDescription), 8 <= channelLayoutDescriptionBits c. Proof. intros c. assert (divisible8 (channelLayoutDescriptionBits c)) as Hdiv8 by (apply (channelLayoutDescriptionBitsDivisible8 c)). unfold divisible8 in Hdiv8. destruct c as [u|p]. - simpl. destruct (uChannels u) as [|ch0 chs] eqn:Hcheq. -- symmetry in Hcheq. assert ([] ≠ uChannels u) as Hne by (apply (uChannelsNonEmpty u)). contradiction. -- unfold channelLayoutDescriptionBits in Hdiv8. rewrite Nat.mod_divide in Hdiv8. rewrite <- Hcheq. apply (Nat.divide_pos_le 8 (channelDescriptionsBitsTotal (uChannels u))). rewrite Hcheq. simpl. assert (0 < cdBits ch0) as HbitnZ. { apply Lt.neq_0_lt. apply (cdBitsNonzero ch0). } apply Nat.add_pos_l. exact HbitnZ. exact Hdiv8. discriminate. - simpl. rewrite (pInvariants p). destruct (pPacking p) eqn:Hpack. -- constructor. -- repeat (constructor). -- repeat (constructor). -- repeat (constructor). Qed.
Require Import Coq.Strings.String. Require Import Calino.Descriptor. Inductive channelSemantic : Set := | CSRed | CSGreen | CSBlue | CSAlpha | CSDepth | CSStencil | CSExponent | CSUnused. Definition channelSemanticDescribe (c : channelSemantic) : descriptor := match c with | CSRed => "R" | CSGreen => "G" | CSBlue => "B" | CSAlpha => "A" | CSDepth => "D" | CSStencil => "S" | CSExponent => "E" | CSUnused => "X" end. #[export] Instance channelSemanticDescribable : describable channelSemantic := { descriptorOf c := channelSemanticDescribe c }.
Require Import Coq.Strings.String. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Descriptor. Inductive channelType : Set := | CTFixedPointNormalizedUnsigned | CTFixedPointNormalizedSigned | CTScaledUnsigned | CTScaledSigned | CTIntegerUnsigned | CTIntegerSigned | CTFloatIEEE754 | CTCustom : descriptor → channelType. Definition channelTypeDescribe (c : channelType) : descriptor := match c with | CTFixedPointNormalizedUnsigned => "FIXED_POINT_NORMALIZED_UNSIGNED" | CTFixedPointNormalizedSigned => "FIXED_POINT_NORMALIZED_SIGNED" | CTScaledUnsigned => "SCALED_UNSIGNED" | CTScaledSigned => "SCALED_SIGNED" | CTIntegerUnsigned => "INTEGER_UNSIGNED" | CTIntegerSigned => "INTEGER_SIGNED" | CTFloatIEEE754 => "FLOATING_POINT_IEEE754" | CTCustom d => d end. #[export] Instance channelTypeDescribable : describable channelType := { descriptorOf c := channelTypeDescribe c }.
Require Import Coq.Strings.String. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Descriptor. Inductive colorSpace : Set := | CSLinear | CSsRGB | CSCustom : descriptor → colorSpace. Definition colorSpaceDescribe (c : colorSpace) : descriptor := match c with | CSLinear => "LINEAR" | CSsRGB => "SRGB" | CSCustom d => d end. #[export] Instance colorSpaceDescribable : describable colorSpace := { descriptorOf c := colorSpaceDescribe c }.
Require Import Coq.Strings.String. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Descriptor. Inductive compressionMethod : Set := | CompressionUncompressed | CompressionBC1 | CompressionBC2 | CompressionBC3 | CompressionBC4 | CompressionBC5 | CompressionBC6 | CompressionBC7 | CompressionETC1 | CompressionETC2 | CompressionEAC | CompressionASTC : nat → nat → compressionMethod | CompressionCustom : ∀ (d : descriptor) (blockSizeX : nat) (blockSizeY : nat) (identifier : nat) (align : nat), 0 < align → compressionMethod. Definition compressionMethodDescriptor (c : compressionMethod) := match c with | CompressionUncompressed => "UNCOMPRESSED" | CompressionBC1 => "BC1" | CompressionBC2 => "BC2" | CompressionBC3 => "BC3" | CompressionBC4 => "BC4" | CompressionBC5 => "BC5" | CompressionBC6 => "BC6" | CompressionBC7 => "BC7" | CompressionETC1 => "ETC1" | CompressionETC2 => "ETC2" | CompressionEAC => "EAC" | CompressionASTC _ _ => "ASTC" | CompressionCustom c _ _ _ _ _ => c end. Definition compressionBlockSizeX (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 4 | CompressionBC2 => 4 | CompressionBC3 => 4 | CompressionBC4 => 4 | CompressionBC5 => 4 | CompressionBC6 => 4 | CompressionBC7 => 4 | CompressionETC1 => 4 | CompressionETC2 => 4 | CompressionEAC => 4 | CompressionASTC x _ => x | CompressionCustom _ x _ _ _ _ => x end. Definition compressionBlockSizeY (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 4 | CompressionBC2 => 4 | CompressionBC3 => 4 | CompressionBC4 => 4 | CompressionBC5 => 4 | CompressionBC6 => 4 | CompressionBC7 => 4 | CompressionETC1 => 4 | CompressionETC2 => 4 | CompressionEAC => 4 | CompressionASTC _ y => y | CompressionCustom _ _ y _ _ _ => y end. Definition compressionSectionIdentifier (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 0 | CompressionBC2 => 0 | CompressionBC3 => 0 | CompressionBC4 => 0 | CompressionBC5 => 0 | CompressionBC6 => 0 | CompressionBC7 => 0 | CompressionETC1 => 0 | CompressionETC2 => 0 | CompressionEAC => 0 | CompressionASTC _ _ => 0 | CompressionCustom _ _ _ i _ _ => i end. Definition compressionBlockAlignment (c : compressionMethod) : nat := match c with | CompressionUncompressed => 0 | CompressionBC1 => 8 | CompressionBC2 => 16 | CompressionBC3 => 16 | CompressionBC4 => 8 | CompressionBC5 => 16 | CompressionBC6 => 16 | CompressionBC7 => 16 | CompressionETC1 => 16 | CompressionETC2 => 16 | CompressionEAC => 16 | CompressionASTC _ _ => 16 | CompressionCustom _ _ _ _ a _ => a end. Definition compressionIsNotCompressed (c : compressionMethod) : Prop := match c with | CompressionUncompressed => True | _ => False end. #[export] Instance compressionMethodDescribable : describable compressionMethod := { descriptorOf c := compressionMethodDescriptor c }.
Require Import Coq.Strings.String. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Descriptor. Inductive coordinateAxisR : Set := | AxisRIncreasingToward | AxisRIncreasingAway. Inductive coordinateAxisS : Set := | AxisSIncreasingRight | AxisSIncreasingLeft. Inductive coordinateAxisT : Set := | AxisTIncreasingDown | AxisTIncreasingUp. Definition coordinateAxisRDescribe (c : coordinateAxisR) : descriptor := match c with | AxisRIncreasingToward => "RT" | AxisRIncreasingAway => "RA" end. Definition coordinateAxisSDescribe (c : coordinateAxisS) : descriptor := match c with | AxisSIncreasingRight => "SR" | AxisSIncreasingLeft => "SL" end. Definition coordinateAxisTDescribe (c : coordinateAxisT) : descriptor := match c with | AxisTIncreasingDown => "TD" | AxisTIncreasingUp => "TU" end. #[export] Instance coordinateAxisRDescribable : describable coordinateAxisR := { descriptorOf c := coordinateAxisRDescribe c }. #[export] Instance coordinateAxisSDescribable : describable coordinateAxisS := { descriptorOf c := coordinateAxisSDescribe c }. #[export] Instance coordinateAxisTDescribable : describable coordinateAxisT := { descriptorOf c := coordinateAxisTDescribe c }. Inductive coordinateSystem : Set := CoordinateSystem : coordinateAxisR → coordinateAxisS → coordinateAxisT → coordinateSystem. Definition coordinateSystemDescribe (c : coordinateSystem) : descriptor := match c with | CoordinateSystem r s t => descriptorOf r ++ ":" ++ descriptorOf s ++ ":" ++ descriptorOf t end. #[export] Instance coordinateSystemDescribable : describable coordinateSystem := { descriptorOf c := coordinateSystemDescribe c }.
Require Import Coq.Arith.PeanoNat. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Bool.Bool. Require Import Coq.Unicode.Utf8_core. Require Import Calino.ImageSize. Import ListNotations. Inductive cubeMapFace : Set := CubeMapFace { cubeFaceOffset : nat; cubeFaceSizeCompressed : nat; cubeFaceSizeUncompressed : nat; cubeFaceCRC32 : nat }. Inductive cubeMipMap : Set := CubeMipMap { cubeMapLevel : nat; cubeMapFaceXPos : cubeMapFace; cubeMapFaceXNeg : cubeMapFace; cubeMapFaceYPos : cubeMapFace; cubeMapFaceYNeg : cubeMapFace; cubeMapFaceZPos : cubeMapFace; cubeMapFaceZNeg : cubeMapFace }. Definition cubeFaceExtent (f : cubeMapFace) : nat := cubeFaceOffset f + cubeFaceSizeCompressed f. Inductive cubeOffsetsSorted : list cubeMipMap → Prop := | CMMSizeOne : ∀ m, cubeFaceExtent (cubeMapFaceXPos m) < cubeFaceOffset (cubeMapFaceXNeg m) → cubeFaceExtent (cubeMapFaceXNeg m) < cubeFaceOffset (cubeMapFaceYPos m) → cubeFaceExtent (cubeMapFaceYPos m) < cubeFaceOffset (cubeMapFaceYNeg m) → cubeFaceExtent (cubeMapFaceYNeg m) < cubeFaceOffset (cubeMapFaceZPos m) → cubeFaceExtent (cubeMapFaceZPos m) < cubeFaceOffset (cubeMapFaceZNeg m) → cubeOffsetsSorted [m] | CMMSizeCons : ∀ mm0 mm1 mxs, cubeFaceExtent (cubeMapFaceZNeg mm1) < cubeFaceOffset (cubeMapFaceXPos mm0) → cubeOffsetsSorted (mm0 :: mxs) → cubeOffsetsSorted (mm1 :: mm0 :: mxs). Inductive cubeMipMapListIsSorted : list cubeMipMap → Prop := | CubeOne : ∀ m, cubeMipMapListIsSorted [m] | CubeCons : ∀ mm0 mm1 mxs, cubeMapLevel mm1 = S (cubeMapLevel mm0) → cubeMipMapListIsSorted (mm0 :: mxs) → cubeMipMapListIsSorted (mm1 :: mm0 :: mxs). Inductive cubeMipMapList : Set := CubeList { cubeMipMaps : list cubeMipMap; cubeMipMapsListSorted : cubeMipMapListIsSorted cubeMipMaps; cubeMipMapsOffsetsSorted : cubeOffsetsSorted cubeMipMaps; }. Lemma cubeMipMapsNonEmpty : ∀ (m : cubeMipMapList), [] ≠ cubeMipMaps m. Proof. intros m. destruct (cubeMipMapsOffsetsSorted m). - discriminate. - discriminate. Qed. Definition cubeMipMapsFirst (m : cubeMipMapList) : cubeMipMap. Proof. assert ([] ≠ cubeMipMaps m) as Hneq by (apply (cubeMipMapsNonEmpty)). destruct (cubeMipMaps m) eqn:Hm. - contradiction. - exact c. Defined. Fixpoint cubeMipMapImageDataSizeTotalAux (m : list cubeMipMap) : nat := match m with | [] => 0 | (x :: []) => cubeFaceExtent (cubeMapFaceZNeg x) | (x :: xs) => cubeMipMapImageDataSizeTotalAux xs end. Definition cubeMipMapImageDataSizeTotal (m : cubeMipMapList) : nat := cubeMipMapImageDataSizeTotalAux (cubeMipMaps m). Example cubeFaceXP0 := CubeMapFace 0 8 8 0. Example cubeFaceXN0 := CubeMapFace 16 8 8 0. Example cubeFaceYP0 := CubeMapFace 32 8 8 0. Example cubeFaceYN0 := CubeMapFace 48 8 8 0. Example cubeFaceZP0 := CubeMapFace 64 8 8 0. Example cubeFaceZN0 := CubeMapFace 80 8 8 0. Example cubeMipMap0 := CubeMipMap 1 cubeFaceXP0 cubeFaceXN0 cubeFaceYP0 cubeFaceYN0 cubeFaceZP0 cubeFaceZN0. Example cubeFaceXP1 := CubeMapFace 96 8 8 0. Example cubeFaceXN1 := CubeMapFace 112 8 8 0. Example cubeFaceYP1 := CubeMapFace 128 8 8 0. Example cubeFaceYN1 := CubeMapFace 144 8 8 0. Example cubeFaceZP1 := CubeMapFace 160 8 8 0. Example cubeFaceZN1 := CubeMapFace 176 8 8 0. Example cubeMipMap1 := CubeMipMap 0 cubeFaceXP1 cubeFaceXN1 cubeFaceYP1 cubeFaceYN1 cubeFaceZP1 cubeFaceZN1. Example cubeOffsetsSortedExample0 : cubeOffsetsSorted [cubeMipMap0]. Proof. apply CMMSizeOne. compute; repeat constructor. compute; repeat constructor. compute; repeat constructor. compute; repeat constructor. compute; repeat constructor. Qed. Example cubeOffsetsSortedExample1 : cubeOffsetsSorted [cubeMipMap1]. Proof. apply CMMSizeOne. compute; repeat constructor. compute; repeat constructor. compute; repeat constructor. compute; repeat constructor. compute; repeat constructor. Qed. Example cubeOffsetsSortedExample2 : cubeOffsetsSorted [cubeMipMap0; cubeMipMap1]. Proof. apply CMMSizeCons. compute; repeat constructor. exact cubeOffsetsSortedExample1. Qed. Example cubeLevelSortedExample0 : cubeMipMapListIsSorted [cubeMipMap0]. Proof. apply CubeOne. Qed. Example cubeLevelSortedExample1 : cubeMipMapListIsSorted [cubeMipMap1]. Proof. apply CubeOne. Qed. Example cubeLevelSortedExample2 : cubeMipMapListIsSorted [cubeMipMap0; cubeMipMap1]. Proof. apply CubeCons. reflexivity. apply CubeOne. Qed.
Require Import Coq.Strings.String. Require Import Coq.Strings.Ascii. Open Scope string_scope. Open Scope char_scope. Definition descriptor := string. Class describable (A : Set) := { descriptorOf : A -> descriptor }.
Require Import Coq.PArith.PArith. Require Import Coq.Arith.PeanoNat. Require Import Coq.Init.Nat. Require Import Coq.Lists.List. Require Import Coq.Unicode.Utf8_core. (* Set Mangle Names. *) Definition divisible8 (x : nat) : Prop := modulo x 8 = 0. Theorem divisiblityNAdd : ∀ (x y z : nat), 0 ≠ z → x mod z = 0 → y mod z = 0 → (x + y) mod z = 0. Proof. intros x y z Hz Hx Hy. destruct y as [|y]. (* If y = 0, then this matches one of our assumptions already. *) rewrite Nat.add_0_r; exact Hx. (* Otherwise, the following property always holds given that the divisor is ≠ 0. *) assert ((x mod z + S y) mod z = (x + S y) mod z) as Heq. apply (Nat.add_mod_idemp_l x (S y) z). apply (Nat.neq_sym 0 z Hz). (* x mod z = 0 *) rewrite Hx in Heq. (* 0 + S y = S y *) rewrite Nat.add_0_l in Heq. rewrite <- Heq. exact Hy. Qed. Theorem divisibilityNFoldPlus : ∀ z xs, 0 ≠ z → Forall (λ n, n mod z = 0) xs → (fold_right plus 0 xs) mod z = 0. Proof. intros z xs Hnz HforAll. induction xs as [|y ys]. - apply (Nat.mod_0_l z (Nat.neq_sym 0 z Hnz)). - assert (fold_right add 0 (y :: ys) = y + fold_right add 0 ys) as Hfoldeq by reflexivity. rewrite Hfoldeq. assert (fold_right add 0 ys mod z = 0) as Hfoldeq2. { apply IHys. apply (@Forall_inv_tail nat (λ n : nat, n mod z = 0) y ys HforAll). } rewrite divisiblityNAdd. reflexivity. exact Hnz. apply (@Forall_inv nat (λ n : nat, n mod z = 0) y ys HforAll). exact Hfoldeq2. Qed. Theorem divisiblity8Add : ∀ (x y : nat), divisible8 x → divisible8 y → divisible8 (x + y). Proof. intros x y Hx Hy. unfold divisible8 in *. apply divisiblityNAdd. discriminate. trivial. trivial. Qed.
Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Descriptor. Import ListNotations. Inductive flag : Set := | FlagAlphaPremultiplied | FlagCustom : descriptor → flag. Definition flagDescribe (f : flag) : descriptor := match f with | FlagAlphaPremultiplied => "ALPHA_PREMULTIPLIED" | FlagCustom d => d end. #[export] Instance flagDescribable : describable flag := { descriptorOf f := flagDescribe f }. Inductive flagSet : Set := { flags : list flag; flagsNoDup : NoDup flags; }.
Require Import Coq.PArith.PArith. Require Import Coq.Arith.PeanoNat. Require Import Coq.Program.Basics. Require Import Coq.Strings.String. Require Import Coq.Strings.Ascii. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Divisible8. Require Import Calino.StringUtility. Require Import Calino.Descriptor. Require Import Calino.ChannelDescription. Require Import Calino.ChannelSemantic. Require Import Calino.ChannelType. Require Import Calino.Compression. Require Import Calino.SuperCompression. Require Import Calino.ColorSpace. Require Import Calino.Flag. Require Import Calino.ByteOrder. Require Import Calino.CoordinateSystem. Require Import Calino.ImageSize. Open Scope program_scope. Record imageInfo : Set := ImageInfo { imageSize : imageSize3D; imageChannelsLayout : channelLayoutDescription; imageChannelsType : channelType; imageCompressionMethod : compressionMethod; imageSuperCompressionMethod : superCompressionMethod; imageCoordinateSystem : coordinateSystem; imageColorSpace : colorSpace; imageFlags : flagSet; imageByteOrder : byteOrder }. Definition imageSizeX := sizeX ∘ imageSize. Definition imageSizeY := sizeY ∘ imageSize. Definition imageSizeZ := sizeZ ∘ imageSize. Definition imageFlagSet := flags ∘ imageFlags. Definition imageInfoTexelBlockAlignment (i : imageInfo) := let c := imageCompressionMethod i in match c with | CompressionUncompressed => channelLayoutDescriptionBits (imageChannelsLayout i) / 8 | _ => compressionBlockAlignment c end. Theorem imageInfoTexelBlockAlignmentPositive : ∀ i, 0 < imageInfoTexelBlockAlignment i. Proof. intros i. unfold imageInfoTexelBlockAlignment. destruct (imageCompressionMethod i) eqn:Hm. - assert (8 <= channelLayoutDescriptionBits (imageChannelsLayout i)) as Hle8 by (apply (channelLayoutDescriptionBitsLe8)). apply (Nat.div_le_lower_bound (channelLayoutDescriptionBits (imageChannelsLayout i)) 8 1). discriminate. rewrite Nat.mul_1_r. exact Hle8. - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - repeat (constructor). - auto. Qed. Theorem imageInfoTexelBlockAlignmentNonZero : ∀ i, 0 ≠ imageInfoTexelBlockAlignment i. Proof. intros i. apply Lt.lt_0_neq. apply imageInfoTexelBlockAlignmentPositive. Qed.
Require Import Coq.Unicode.Utf8_core. Record imageSize3D : Set := ImageSize3D { sizeX : nat; sizeY : nat; sizeZ : nat; sizeXnot0 : 0 ≠ sizeX; sizeYnot0 : 0 ≠ sizeY; sizeZnot0 : 0 ≠ sizeZ; }.
Require Import Coq.Strings.String. Require Import Coq.Strings.Ascii. Require Import Coq.Lists.List. Require Import Coq.Unicode.Utf8_core. Open Scope string_scope. Import ListNotations. Inductive metadataValue : Set := MetadataValue { mKey : string; mValue : string }. Inductive metadata : Set := Metadata { mValues : list metadataValue }.
Require Import Coq.Arith.PeanoNat. Require Import Coq.Lists.List. Require Import Coq.Init.Nat. Require Import Coq.Bool.Bool. Require Import Coq.Unicode.Utf8_core. Require Import Calino.ImageSize. Import ListNotations. Inductive mipMap : Set := MipMap { mipMapLevel : nat; mipMapOffset : nat; mipMapSizeCompressed : nat; mipMapSizeUncompressed : nat; mipMapCRC32 : nat }. Inductive mipMapListIsSorted : list mipMap → Prop := | MipsOne : ∀ m, mipMapListIsSorted [m] | MipsCons : ∀ mm0 mm1 mxs, mipMapLevel mm1 = S (mipMapLevel mm0) → mipMapListIsSorted (mm0 :: mxs) → mipMapListIsSorted (mm1 :: mm0 :: mxs). Inductive mipMapOffsetsSorted : list mipMap → Prop := | MMSizeOne : ∀ m, mipMapOffsetsSorted [m] | MMSizeCons : ∀ mm0 mm1 mxs, ((mipMapOffset mm1) + (mipMapSizeCompressed mm1)) < (mipMapOffset mm0) → mipMapOffsetsSorted (mm0 :: mxs) → mipMapOffsetsSorted (mm1 :: mm0 :: mxs). Inductive mipMapList : Set := MipMapList { mipMaps : list mipMap; mipMapListSorted : mipMapListIsSorted mipMaps; mipMapOffsetSorted : mipMapOffsetsSorted mipMaps; }. Inductive mipMapImageSize : Set := MipMapImageSize { mmSizeX : nat; mmSizeY : nat; mmSizeXRange : 1 < mmSizeX; mmSizeYRange : 1 < mmSizeY; }. Lemma mipMapsNonEmpty : ∀ (m : mipMapList), [] ≠ mipMaps m. Proof. intros m. destruct (mipMapListSorted m). - discriminate. - discriminate. Qed. Definition mipMapFirst (m : mipMapList) : mipMap. Proof. assert ([] ≠ mipMaps m) as Hneq by (apply (mipMapsNonEmpty)). destruct (mipMaps m) eqn:Hm. - contradiction. - exact m0. Defined. Lemma lt_neq : ∀ n, 0 ≠ n ↔ 0 < n. Proof. intros n. constructor. - intro Hneq. induction n as [|k]. -- unfold not in Hneq. assert (0 = 0) as Heq by reflexivity. contradiction. -- apply (Nat.lt_0_succ k). - intro Hneq. induction n as [|k]. -- inversion Hneq. -- discriminate. Qed. Lemma lt_neq_0 : ∀ n, 0 ≠ n → 0 < n. Proof. intros n Hneq. rewrite <- lt_neq; trivial. Qed. Lemma lt_neq_1 : ∀ n, 0 < n → 0 ≠ n. Proof. intros n Hneq. rewrite lt_neq; trivial. Qed. Definition mipMapSize (level : nat) (imageSize : imageSize3D) (levelRange : 0 < level) : option mipMapImageSize := let sx := (sizeX imageSize) / 2 ^ level in let sy := (sizeY imageSize) / 2 ^ level in match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with | (ReflectT _ xt, ReflectT _ yt) => Some (MipMapImageSize sx sy xt yt) | (_, _) => None end. Fixpoint mipMapImageDataSizeTotalAux (m : list mipMap) : nat := match m with | [] => 0 | (x :: []) => (mipMapOffset x) + (mipMapSizeCompressed x) | (x :: xs) => mipMapImageDataSizeTotalAux xs end. Definition mipMapImageDataSizeTotal (m : mipMapList) : nat := mipMapImageDataSizeTotalAux (mipMaps m).
Require Import Coq.Lists.List. Require Import Coq.Unicode.Utf8_core. Require Import Calino.ChannelDescription. Require Import Calino.ChannelSemantic. Require Import Calino.ChannelType. Import ListNotations. Declare Scope Forall_scope. Open Scope Forall_scope. Definition p0n1 : 0 ≠ 1 := O_S 0. Definition p0n4 : 0 ≠ 4 := O_S 3. Definition p0n5 : 0 ≠ 5 := O_S 4. Definition p0n6 : 0 ≠ 6 := O_S 5. Definition p0n8 : 0 ≠ 8 := O_S 7. Definition p0n16 : 0 ≠ 16 := O_S 15. Definition p0n32 : 0 ≠ 32 := O_S 31. Definition p0n64 : 0 ≠ 64 := O_S 63. Definition A1 : channelDescription := channelDescriptionMake CSAlpha 1 p0n1. Definition R5 : channelDescription := channelDescriptionMake CSRed 5 p0n5. Definition G6 : channelDescription := channelDescriptionMake CSGreen 6 p0n6. Definition B5 : channelDescription := channelDescriptionMake CSBlue 5 p0n5. Definition G5 : channelDescription := channelDescriptionMake CSGreen 5 p0n5. Definition R4 : channelDescription := channelDescriptionMake CSRed 4 p0n4. Definition G4 : channelDescription := channelDescriptionMake CSGreen 4 p0n4. Definition B4 : channelDescription := channelDescriptionMake CSBlue 4 p0n4. Definition A4 : channelDescription := channelDescriptionMake CSAlpha 4 p0n4. Definition R8 : channelDescription := channelDescriptionMake CSRed 8 p0n8. Definition G8 : channelDescription := channelDescriptionMake CSGreen 8 p0n8. Definition B8 : channelDescription := channelDescriptionMake CSBlue 8 p0n8. Definition A8 : channelDescription := channelDescriptionMake CSAlpha 8 p0n8. Definition R8_Div8 : channelDescriptionBitsDivisible8 R8 := eq_refl. Definition G8_Div8 : channelDescriptionBitsDivisible8 G8 := eq_refl. Definition B8_Div8 : channelDescriptionBitsDivisible8 B8 := eq_refl. Definition A8_Div8 : channelDescriptionBitsDivisible8 A8 := eq_refl. Definition R16 : channelDescription := channelDescriptionMake CSRed 16 p0n16. Definition G16 : channelDescription := channelDescriptionMake CSGreen 16 p0n16. Definition B16 : channelDescription := channelDescriptionMake CSBlue 16 p0n16. Definition A16 : channelDescription := channelDescriptionMake CSAlpha 16 p0n16. Definition R16_Div8 : channelDescriptionBitsDivisible8 R16 := eq_refl. Definition G16_Div8 : channelDescriptionBitsDivisible8 G16 := eq_refl. Definition B16_Div8 : channelDescriptionBitsDivisible8 B16 := eq_refl. Definition A16_Div8 : channelDescriptionBitsDivisible8 A16 := eq_refl. Definition R32 : channelDescription := channelDescriptionMake CSRed 32 p0n32. Definition G32 : channelDescription := channelDescriptionMake CSGreen 32 p0n32. Definition B32 : channelDescription := channelDescriptionMake CSBlue 32 p0n32. Definition A32 : channelDescription := channelDescriptionMake CSAlpha 32 p0n32. Definition R32_Div8 : channelDescriptionBitsDivisible8 R32 := eq_refl. Definition G32_Div8 : channelDescriptionBitsDivisible8 G32 := eq_refl. Definition B32_Div8 : channelDescriptionBitsDivisible8 B32 := eq_refl. Definition A32_Div8 : channelDescriptionBitsDivisible8 A32 := eq_refl. Definition R64 : channelDescription := channelDescriptionMake CSRed 64 p0n64. Definition G64 : channelDescription := channelDescriptionMake CSGreen 64 p0n64. Definition B64 : channelDescription := channelDescriptionMake CSBlue 64 p0n64. Definition A64 : channelDescription := channelDescriptionMake CSAlpha 64 p0n64. Definition R64_Div8 : channelDescriptionBitsDivisible8 R64 := eq_refl. Definition G64_Div8 : channelDescriptionBitsDivisible8 G64 := eq_refl. Definition B64_Div8 : channelDescriptionBitsDivisible8 B64 := eq_refl. Definition A64_Div8 : channelDescriptionBitsDivisible8 A64 := eq_refl. (* Packed channels *) Definition A1_R5_G5_B5_Channels : list channelDescription := [A1; R5; G5; B5]. Definition A1_R5_G5_B5_NonEmpty := nil_cons (x := A1) (l := [R5; G5; B5]). Definition R4_G4_B4_A4_Channels : list channelDescription := [R4; G4; B4; A4]. Definition R4_G4_B4_A4_NonEmpty := nil_cons (x := R4) (l := [G4; B4; A4]). Definition R5_G6_B5_Channels : list channelDescription := [R5; G6; B5]. Definition R5_G6_B5_NonEmpty := nil_cons (x := R5) (l := [G6; B5]). (* 8-bit channels *) Definition R8_G8_B8_A8_Channels : list channelDescription := [R8; G8; B8; A8]. Definition R8_G8_B8_A8_NonEmpty := nil_cons (x := R8) (l := [G8; B8; A8]). Definition R8_G8_B8_A8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_G8_B8_A8_Channels := Forall_cons R8 R8_Div8 (Forall_cons G8 G8_Div8 (Forall_cons B8 B8_Div8 (Forall_cons A8 A8_Div8 (Forall_nil _)))). Definition R8_G8_B8_Channels : list channelDescription := [R8; G8; B8]. Definition R8_G8_B8_NonEmpty := nil_cons (x := R8) (l := [G8;B8]). Definition R8_G8_B8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_G8_B8_Channels := Forall_cons R8 R8_Div8 (Forall_cons G8 G8_Div8 (Forall_cons B8 B8_Div8 (Forall_nil _))). Definition R8_G8_Channels : list channelDescription := [R8; G8]. Definition R8_G8_NonEmpty := nil_cons (x := R8) (l := [G8]). Definition R8_G8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_G8_Channels := Forall_cons R8 R8_Div8 (Forall_cons G8 G8_Div8 (Forall_nil _)). Definition R8_Channels : list channelDescription := [R8]. Definition R8_NonEmpty := nil_cons (x := R8) (l := []). Definition R8_FDiv8 : Forall channelDescriptionBitsDivisible8 R8_Channels := Forall_cons R8 R8_Div8 (Forall_nil _). (* 16-bit channels *) Definition R16_G16_B16_A16_Channels : list channelDescription := [R16; G16; B16; A16]. Definition R16_G16_B16_A16_NonEmpty := nil_cons (x := R16) (l := [G16; B16; A16]). Definition R16_G16_B16_A16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_G16_B16_A16_Channels := Forall_cons R16 R16_Div8 (Forall_cons G16 G16_Div8 (Forall_cons B16 B16_Div8 (Forall_cons A16 A16_Div8 (Forall_nil _)))). Definition R16_G16_B16_Channels : list channelDescription := [R16; G16; B16]. Definition R16_G16_B16_NonEmpty := nil_cons (x := R16) (l := [G16;B16]). Definition R16_G16_B16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_G16_B16_Channels := Forall_cons R16 R16_Div8 (Forall_cons G16 G16_Div8 (Forall_cons B16 B16_Div8 (Forall_nil _))). Definition R16_G16_Channels : list channelDescription := [R16; G16]. Definition R16_G16_NonEmpty := nil_cons (x := R16) (l := [G16]). Definition R16_G16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_G16_Channels := Forall_cons R16 R16_Div8 (Forall_cons G16 G16_Div8 (Forall_nil _)). Definition R16_Channels : list channelDescription := [R16]. Definition R16_NonEmpty := nil_cons (x := R16) (l := []). Definition R16_FDiv8 : Forall channelDescriptionBitsDivisible8 R16_Channels := Forall_cons R16 R16_Div8 (Forall_nil _). (* 32-bit channels *) Definition R32_G32_B32_A32_Channels : list channelDescription := [R32; G32; B32; A32]. Definition R32_G32_B32_A32_NonEmpty := nil_cons (x := R32) (l := [G32; B32; A32]). Definition R32_G32_B32_A32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_G32_B32_A32_Channels := Forall_cons R32 R32_Div8 (Forall_cons G32 G32_Div8 (Forall_cons B32 B32_Div8 (Forall_cons A32 A32_Div8 (Forall_nil _)))). Definition R32_G32_B32_Channels : list channelDescription := [R32; G32; B32]. Definition R32_G32_B32_NonEmpty := nil_cons (x := R32) (l := [G32;B32]). Definition R32_G32_B32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_G32_B32_Channels := Forall_cons R32 R32_Div8 (Forall_cons G32 G32_Div8 (Forall_cons B32 B32_Div8 (Forall_nil _))). Definition R32_G32_Channels : list channelDescription := [R32; G32]. Definition R32_G32_NonEmpty := nil_cons (x := R32) (l := [G32]). Definition R32_G32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_G32_Channels := Forall_cons R32 R32_Div8 (Forall_cons G32 G32_Div8 (Forall_nil _)). Definition R32_Channels : list channelDescription := [R32]. Definition R32_NonEmpty := nil_cons (x := R32) (l := []). Definition R32_FDiv8 : Forall channelDescriptionBitsDivisible8 R32_Channels := Forall_cons R32 R32_Div8 (Forall_nil _). (* 64-bit channels *) Definition R64_G64_B64_A64_Channels : list channelDescription := [R64; G64; B64; A64]. Definition R64_G64_B64_A64_NonEmpty := nil_cons (x := R64) (l := [G64; B64; A64]). Definition R64_G64_B64_A64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_G64_B64_A64_Channels := Forall_cons R64 R64_Div8 (Forall_cons G64 G64_Div8 (Forall_cons B64 B64_Div8 (Forall_cons A64 A64_Div8 (Forall_nil _)))). Definition R64_G64_B64_Channels : list channelDescription := [R64; G64; B64]. Definition R64_G64_B64_NonEmpty := nil_cons (x := R64) (l := [G64;B64]). Definition R64_G64_B64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_G64_B64_Channels := Forall_cons R64 R64_Div8 (Forall_cons G64 G64_Div8 (Forall_cons B64 B64_Div8 (Forall_nil _))). Definition R64_G64_Channels : list channelDescription := [R64; G64]. Definition R64_G64_NonEmpty := nil_cons (x := R64) (l := [G64]). Definition R64_G64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_G64_Channels := Forall_cons R64 R64_Div8 (Forall_cons G64 G64_Div8 (Forall_nil _)). Definition R64_Channels : list channelDescription := [R64]. Definition R64_NonEmpty := nil_cons (x := R64) (l := []). Definition R64_FDiv8 : Forall channelDescriptionBitsDivisible8 R64_Channels := Forall_cons R64 R64_Div8 (Forall_nil _). (* Layouts *) Definition Layout_A1_R5_G5_B5 : channelLayoutDescription := ChannelLayoutDescriptionPacked (CLDPMake A1_R5_G5_B5_Channels A1_R5_G5_B5_NonEmpty CLPack16 eq_refl). Definition Layout_R4_G4_B4_A4 : channelLayoutDescription := ChannelLayoutDescriptionPacked (CLDPMake R4_G4_B4_A4_Channels R4_G4_B4_A4_NonEmpty CLPack16 eq_refl). Definition Layout_R5_G6_B5 : channelLayoutDescription := ChannelLayoutDescriptionPacked (CLDPMake R5_G6_B5_Channels R5_G6_B5_NonEmpty CLPack16 eq_refl). Definition Layout_R8_G8_B8_A8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_A8_Channels R8_G8_B8_A8_NonEmpty R8_G8_B8_A8_FDiv8). Definition Layout_R8_G8_B8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_B8_Channels R8_G8_B8_NonEmpty R8_G8_B8_FDiv8). Definition Layout_R8_G8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_G8_Channels R8_G8_NonEmpty R8_G8_FDiv8). Definition Layout_R8 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R8_Channels R8_NonEmpty R8_FDiv8). Definition Layout_R16_G16_B16_A16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_A16_Channels R16_G16_B16_A16_NonEmpty R16_G16_B16_A16_FDiv8). Definition Layout_R16_G16_B16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_B16_Channels R16_G16_B16_NonEmpty R16_G16_B16_FDiv8). Definition Layout_R16_G16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_G16_Channels R16_G16_NonEmpty R16_G16_FDiv8). Definition Layout_R16 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R16_Channels R16_NonEmpty R16_FDiv8). Definition Layout_R32_G32_B32_A32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_A32_Channels R32_G32_B32_A32_NonEmpty R32_G32_B32_A32_FDiv8). Definition Layout_R32_G32_B32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_B32_Channels R32_G32_B32_NonEmpty R32_G32_B32_FDiv8). Definition Layout_R32_G32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_G32_Channels R32_G32_NonEmpty R32_G32_FDiv8). Definition Layout_R32 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R32_Channels R32_NonEmpty R32_FDiv8). Definition Layout_R64_G64_B64_A64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_A64_Channels R64_G64_B64_A64_NonEmpty R64_G64_B64_A64_FDiv8). Definition Layout_R64_G64_B64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_B64_Channels R64_G64_B64_NonEmpty R64_G64_B64_FDiv8). Definition Layout_R64_G64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_G64_Channels R64_G64_NonEmpty R64_G64_FDiv8). Definition Layout_R64 : channelLayoutDescription := ChannelLayoutDescriptionUnpacked (CLDUMake R64_Channels R64_NonEmpty R64_FDiv8).
Require Import Coq.Arith.PeanoNat. Require Import Coq.Strings.String. Require Import Coq.Strings.Ascii. Open Scope string_scope. Open Scope char_scope. Set Mangle Names. Definition digitOfNat (n : nat) : ascii := match n with | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9" end. Fixpoint stringOfNatAux (time n : nat) (acc : string) : string := let acc' := String (digitOfNat (n mod 10)) acc in match time with | 0 => acc' | S time' => match n / 10 with | 0 => acc' | n' => stringOfNatAux time' n' acc' end end. Definition stringOfNat (n : nat) : string := stringOfNatAux n n "".
Require Import Coq.Strings.String. Require Import Coq.Unicode.Utf8_core. Require Import Calino.Descriptor. Inductive superCompressionMethod : Set := | SuperCompressionUncompressed | SuperCompressionLZ4 | SuperCompressionCustom : descriptor → nat → superCompressionMethod. Definition superCompressionMethodDescriptor (c : superCompressionMethod) := match c with | SuperCompressionUncompressed => "UNCOMPRESSED" | SuperCompressionLZ4 => "LZ4" | SuperCompressionCustom c _ => c end. Definition superCompressionIsNotCompressed (c : superCompressionMethod) : Prop := match c with | SuperCompressionUncompressed => True | _ => False end. Definition superCompressionSectionIdentifier (c : superCompressionMethod) : nat := match c with | SuperCompressionUncompressed => 0 | SuperCompressionLZ4 => 0 | SuperCompressionCustom _ i => i end. #[export] Instance superCompressionMethodDescribable : describable superCompressionMethod := { descriptorOf c := superCompressionMethodDescriptor c }.
Require Import Coq.Unicode.Utf8_core. Require Import Calino.CubeMipMap. Require Import Calino.ArrayMipMap. Require Import Calino.ImageInfo. Require Import Calino.MipMap. Inductive texture2d : Set := Texture2D { i2dInfo : imageInfo; i2dMipMaps : mipMapList; i2dSize : 1 = imageSizeZ i2dInfo }. Inductive textureArray : Set := TextureArray { iaInfo : imageInfo; iaMipMaps : arrayMipMapList; iaSize : 1 <= imageSizeZ iaInfo }. Inductive textureCube : Set := TextureCube { icubeInfo : imageInfo; icubeMipMaps : cubeMipMapList; icubeSize : 1 = imageSizeZ icubeInfo }. Inductive texture : Set := | TTexture2D : texture2d → texture | TTextureArray : textureArray → texture | TTextureCube : textureCube → texture. Definition imageInfoOf (i : texture) : imageInfo := match i with | TTexture2D (Texture2D i _ _) => i | TTextureArray (TextureArray i _ _) => i | TTextureCube (TextureCube i _ _) => i end.