1  --  Cerro Torre Crypto - SPARK-verified cryptographic operations
  2  --  SPDX-License-Identifier: MIT OR AGPL-3.0-or-later
  3  --  Palimpsest-Covenant: 1.0
  4  --
  5  --  This package provides cryptographic primitives with formal verification.
  6  --  All operations are proven free of runtime errors and implement their
  7  --  mathematical specifications correctly.
  8  
  9  with Interfaces;
 10  
 11  package Cerro_Crypto
 12     with SPARK_Mode => On
 13  is
 14     use Interfaces;
 15  
 16     ---------------------
 17     -- Type Definitions --
 18     ---------------------
 19  
 20     --  SHA-256 digest (32 bytes)
 21     subtype Digest_Index is Positive range 1 .. 32;
 22     type SHA256_Digest is array (Digest_Index) of Unsigned_8;
 23  
 24     --  SHA-512 digest (64 bytes)
 25     subtype Digest_512_Index is Positive range 1 .. 64;
 26     type SHA512_Digest is array (Digest_512_Index) of Unsigned_8;
 27  
 28     --  Ed25519 public key (32 bytes)
 29     subtype Key_Index is Positive range 1 .. 32;
 30     type Ed25519_Public_Key is array (Key_Index) of Unsigned_8;
 31  
 32     --  Ed25519 signature (64 bytes)
 33     subtype Signature_Index is Positive range 1 .. 64;
 34     type Ed25519_Signature is array (Signature_Index) of Unsigned_8;
 35  
 36     --  Hash algorithm enumeration
 37     type Hash_Algorithm is (SHA256, SHA384, SHA512, Blake3);
 38  
 39     --  Maximum input size for hashing (prevent overflow in length encoding)
 40     Max_Hash_Input_Length : constant := 2**32 - 1 - 64;
 41  
 42     -------------------
 43     -- Hash Functions --
 44     -------------------
 45  
 46     --  Compute SHA-256 hash of input data
 47     function Compute_SHA256 (Data : String) return SHA256_Digest
 48        with Global => null,
 49             Pre    => Data'Length <= Max_Hash_Input_Length,
 50             Post   => Compute_SHA256'Result'Length = 32;
 51  
 52     --  Compute SHA-512 hash of input data
 53     function Compute_SHA512 (Data : String) return SHA512_Digest
 54        with Global => null,
 55             Pre    => Data'Length <= Max_Hash_Input_Length,
 56             Post   => Compute_SHA512'Result'Length = 64;
 57  
 58     -------------------------
 59     -- Signature Verification --
 60     -------------------------
 61  
 62     --  Verify an Ed25519 signature
 63     --  Returns True if and only if the signature is valid for the given
 64     --  message and public key.
 65     function Verify_Ed25519
 66        (Message   : String;
 67         Signature : Ed25519_Signature;
 68         Public_Key: Ed25519_Public_Key) return Boolean
 69        with Global => null,
 70             Pre    => Message'Length <= Max_Hash_Input_Length;
 71  
 72     -----------------------
 73     -- Utility Functions --
 74     -----------------------
 75  
 76     --  Convert hex string to bytes
 77     --  Returns empty array if input is invalid
 78     function Hex_To_Bytes (Hex : String) return SHA256_Digest
 79        with Global => null,
 80             Pre    => Hex'Length = 64;
 81  
 82     --  Convert bytes to hex string
 83     function Bytes_To_Hex (Digest : SHA256_Digest) return String
 84        with Global => null,
 85             Post   => Bytes_To_Hex'Result'Length = 64;
 86  
 87     --  Constant-time comparison to prevent timing attacks
 88     function Constant_Time_Equal
 89        (Left, Right : SHA256_Digest) return Boolean
 90        with Global => null;
 91  
 92     -----------------------
 93     -- Hash Verification --
 94     -----------------------
 95  
 96     --  Verify that data matches expected hash
 97     function Verify_SHA256
 98        (Data          : String;
 99         Expected_Hash : SHA256_Digest) return Boolean
100        with Global => null,
101             Pre    => Data'Length <= Max_Hash_Input_Length;
102  
103     --  Parse and verify a hash string (algorithm:hexdigest format)
104     type Verification_Result is (Valid, Invalid_Hash, Algorithm_Mismatch, Parse_Error);
105  
106     function Verify_Hash_String
107        (Data        : String;
108         Hash_String : String) return Verification_Result
109        with Global => null,
110             Pre    => Data'Length <= Max_Hash_Input_Length
111                       and Hash_String'Length >= 8;  -- Minimum: "sha256:X"
112  
113  end Cerro_Crypto;