lingenic_text-utf8

--  Copyright © 2026 Lingenic LLC. All rights reserved.
--  Licensed under the Lingenic Source-Available License v2.3.
--  Production use requires a separate license from Licensor.
--  See LICENSE.md and COPYRIGHT in the project root.
--

-------------------------------------------------------------------------------
--  Lingenic-Text
--  Formally Verified Unicode Text Processing Library
--
--  UTF-8 encoding and decoding per RFC 3629.
--
--  Postconditions reference the ghost spec in Lingenic_Text.UTF8_Spec.
--  The ghost spec encodes the RFC rules as expression functions; the prover
--  unfolds them and verifies the implementation matches.
-------------------------------------------------------------------------------

with Lingenic_Text.UTF8_Spec;

package Lingenic_Text.UTF8
   with SPARK_Mode, Pure
is

   ---------------------------------------------------------------------------
   --  Decode one UTF-8 sequence starting at Source (Pos).
   --
   --  Completeness: Valid = Well_Formed_At (bidirectional, not just =>)
   --  Round-trip:   Source bytes are the encoding of the decoded CP
   --  Scalar:       Decoded CP is always a scalar value (surrogates excluded)
   ---------------------------------------------------------------------------

   procedure Decode
     (Source : Byte_Array;
      Pos    : Positive;
      CP     : out Codepoint;
      Length : out Positive;
      Valid  : out Boolean)
   with Pre  => Pos in Source'Range
                and then Source'Last < Positive'Last,
        Post => Length in 1 .. 4
                and then Valid = UTF8_Spec.Well_Formed_At (Source, Pos)
                and then
                  (if Valid then
                     Length = UTF8_Spec.Lead_Length (Source (Pos))
                     and then CP = UTF8_Spec.Decoded_At (Source, Pos)
                     and then Is_Scalar_Value (CP)
                     and then UTF8_Spec.Encoded_At (Source, Pos, CP)
                   else
                     CP = 0 and then Length = 1);

   ---------------------------------------------------------------------------
   --  Encode one codepoint as a UTF-8 sequence into Target starting at Pos.
   --
   --  Round-trip:  Encoded bytes are well-formed and decode back to CP
   --  Frame:       Bytes outside the written range are unchanged
   ---------------------------------------------------------------------------

   procedure Encode
     (CP     : Codepoint;
      Target : in out Byte_Array;
      Pos    : Positive;
      Length : out Positive)
   with Pre  => Is_Scalar_Value (CP)
                and then Pos in Target'Range
                and then Target'Last < Positive'Last
                and then Target'Last - Pos >= UTF8_Spec.Encoded_Length (CP) - 1,
        Post => Length = UTF8_Spec.Encoded_Length (CP)
                and then UTF8_Spec.Encoded_At (Target, Pos, CP)
                and then UTF8_Spec.Well_Formed_At (Target, Pos)
                and then UTF8_Spec.Decoded_At (Target, Pos) = CP
                and then (for all I in Target'Range =>
                            (if I < Pos or else I - Pos >= Length then
                               Target (I) = Target'Old (I)));

end Lingenic_Text.UTF8;