cerro_manifest.ads
1 -- Cerro Torre Manifest - SPARK-verified manifest parsing 2 -- SPDX-License-Identifier: MIT OR AGPL-3.0-or-later 3 -- Palimpsest-Covenant: 1.0 4 -- 5 -- This package provides manifest parsing with formal verification. 6 -- The parser is proven to terminate on all inputs and to correctly 7 -- validate manifest structure. 8 9 with Ada.Strings.Unbounded; 10 with Ada.Containers.Vectors; 11 with Ada.Calendar; 12 13 package Cerro_Manifest 14 with SPARK_Mode => On 15 is 16 use Ada.Strings.Unbounded; 17 18 --------------------- 19 -- Type Definitions -- 20 --------------------- 21 22 -- Package name (validated identifier) 23 subtype Package_Name_Length is Positive range 1 .. 64; 24 subtype Package_Name is String 25 with Dynamic_Predicate => 26 Package_Name'Length in Package_Name_Length 27 and then (for all C of Package_Name => 28 C in 'a' .. 'z' | '0' .. '9' | '-'); 29 30 -- Version components 31 type Version is record 32 Epoch : Natural := 0; 33 Upstream : Unbounded_String; 34 Revision : Positive := 1; 35 end record; 36 37 -- Hash specification 38 type Hash_Algorithm is (SHA256, SHA384, SHA512, Blake3); 39 40 type Hash_Value is record 41 Algorithm : Hash_Algorithm; 42 Digest : Unbounded_String; -- Hex-encoded 43 end record; 44 45 -- SPDX license expression (simplified) 46 subtype License_Expression is Unbounded_String; 47 48 -- Dependency reference 49 type Version_Constraint_Kind is (Any, Exact, Minimum, Maximum, Range_Constraint); 50 51 type Version_Constraint (Kind : Version_Constraint_Kind := Any) is record 52 case Kind is 53 when Any => 54 null; 55 when Exact | Minimum | Maximum => 56 Bound : Unbounded_String; 57 when Range_Constraint => 58 Lower_Bound : Unbounded_String; 59 Upper_Bound : Unbounded_String; 60 end case; 61 end record; 62 63 type Dependency_Reference is record 64 Name : Unbounded_String; 65 Constraint : Version_Constraint; 66 end record; 67 68 -- Dependency list 69 package Dependency_Vectors is new Ada.Containers.Vectors 70 (Index_Type => Positive, 71 Element_Type => Dependency_Reference); 72 73 subtype Dependency_List is Dependency_Vectors.Vector; 74 75 -- String list (for patches, flags, etc.) 76 package String_Vectors is new Ada.Containers.Vectors 77 (Index_Type => Positive, 78 Element_Type => Unbounded_String); 79 80 subtype String_List is String_Vectors.Vector; 81 82 ---------------------- 83 -- Manifest Sections -- 84 ---------------------- 85 86 -- [metadata] section 87 type Metadata_Section is record 88 Name : Unbounded_String; 89 Version : Cerro_Manifest.Version; 90 Summary : Unbounded_String; 91 Description : Unbounded_String; 92 License : License_Expression; 93 Homepage : Unbounded_String; 94 Maintainer : Unbounded_String; 95 end record; 96 97 -- [provenance] section 98 type Provenance_Section is record 99 Upstream_URL : Unbounded_String; 100 Upstream_Hash : Hash_Value; 101 Upstream_Signature : Unbounded_String; -- Optional 102 Upstream_Keyring : Unbounded_String; -- Optional 103 Imported_From : Unbounded_String; -- e.g., "debian:nginx/1.26.0-1" 104 Import_Date : Ada.Calendar.Time; 105 Patches : String_List; 106 end record; 107 108 -- [dependencies] section 109 type Dependencies_Section is record 110 Runtime : Dependency_List; 111 Build : Dependency_List; 112 Check : Dependency_List; 113 Optional : Dependency_List; 114 Conflicts : Dependency_List; 115 Provides : Dependency_List; 116 Replaces : Dependency_List; 117 end record; 118 119 -- Build system identifier 120 type Build_System is 121 (Autoconf, CMake, Meson, Cargo, Alire, Dune, Mix, Make, Custom); 122 123 -- [build] section 124 type Build_Section is record 125 System : Build_System; 126 Configure_Flags : String_List; 127 Build_Flags : String_List; 128 Install_Flags : String_List; 129 -- Environment and phases handled separately 130 end record; 131 132 -- [outputs] section 133 type Outputs_Section is record 134 Primary : Unbounded_String; 135 Split : String_List; 136 end record; 137 138 -- Attestation types 139 type Attestation_Type is 140 (Source_Signature, Reproducible_Build, SBOM_Complete, 141 Security_Audit, Fuzz_Tested); 142 143 package Attestation_Vectors is new Ada.Containers.Vectors 144 (Index_Type => Positive, 145 Element_Type => Attestation_Type); 146 147 subtype Attestation_List is Attestation_Vectors.Vector; 148 149 -- [attestations] section 150 type Attestations_Section is record 151 Required : Attestation_List; 152 Recommended : Attestation_List; 153 end record; 154 155 ----------------------- 156 -- Complete Manifest -- 157 ----------------------- 158 159 type Manifest is record 160 Metadata : Metadata_Section; 161 Provenance : Provenance_Section; 162 Dependencies : Dependencies_Section; 163 Build : Build_Section; 164 Outputs : Outputs_Section; 165 Attestations : Attestations_Section; 166 end record; 167 168 ------------------ 169 -- Parse Result -- 170 ------------------ 171 172 type Parse_Error_Kind is 173 (None, 174 File_Not_Found, 175 Invalid_Encoding, 176 Syntax_Error, 177 Missing_Required_Field, 178 Invalid_Value, 179 Duplicate_Section, 180 Unknown_Section); 181 182 type Parse_Result (Success : Boolean := False) is record 183 case Success is 184 when True => 185 Value : Manifest; 186 when False => 187 Error : Parse_Error_Kind; 188 Error_Line : Natural; 189 Error_Msg : Unbounded_String; 190 end case; 191 end record; 192 193 ----------------------- 194 -- Parsing Functions -- 195 ----------------------- 196 197 -- Parse a manifest from string content 198 function Parse_String (Content : String) return Parse_Result 199 with Global => null, 200 Pre => Content'Length <= 1_000_000; -- 1MB max manifest 201 202 -- Parse a manifest from file 203 function Parse_File (Path : String) return Parse_Result 204 with Pre => Path'Length > 0 and Path'Length <= 4096; 205 206 ------------------------- 207 -- Validation Functions -- 208 ------------------------- 209 210 -- Validate manifest completeness (all required fields present) 211 function Is_Complete (M : Manifest) return Boolean 212 with Global => null; 213 214 -- Validate hash format 215 function Is_Valid_Hash (H : Hash_Value) return Boolean 216 with Global => null; 217 218 -- Validate version string 219 function Is_Valid_Version (V : Version) return Boolean 220 with Global => null; 221 222 ----------------------- 223 -- Serialization -- 224 ----------------------- 225 226 -- Serialize manifest to string 227 function To_String (M : Manifest) return String 228 with Global => null; 229 230 end Cerro_Manifest;