Struct StringEscapeRoundtripPin 

pub struct StringEscapeRoundtripPin {

    pub scan_fn: String,
    pub escape_fn: String,
    pub validate_fn: String,
    pub finish_fn: String,
    pub unicode_fn: String,
    pub codepoint_fn: String,
    pub apply_fn: String,
    pub read_hex_fn: String,
    pub hex_val_fn: String,
    pub high_surrogate_fn: String,
    pub low_surrogate_fn: String,
    pub producer_fn: String,
    pub fold_fn: String,
    pub classifier_fn: String,
    pub control_fn: String,
    pub control_escape_fn: String,
    pub ok_ctor: String,
    pub str_ctor: String,
    pub terminator: char,
    pub escape_char: char,
    pub unicode_letter: char,
    pub pairs: Vec<EscapePairSpec>,
    pub control_threshold: i64,
    pub high_surrogate_min: i64,
    pub low_surrogate_min: i64,
}

Parameter pack for ProofStrategy::StringEscapeRoundtrip — every fn name and literal the Lean renderer’s suffix-invariant proof skeleton quotes. All fn names are source names (backends translate); all chars/codes are the SOURCE literals the detector read off the validated arm patterns, so the renderer can rebuild them as Lean literals without re-walking the AST.

Fields

scan_fn: String

The scanner SCC member the law enters (parseStringChunk). Body: charAt dispatch over { terminator → finish, escape-char → escape dispatch, default → validate }.

escape_fn: String

Escape dispatcher (parseEscape): slices the open segment, then maps escape letters to decoded chars / the unicode hop.

validate_fn: String

Default-arm validator (validateChar): control chars error, printable chars extend the open segment.

finish_fn: String

Terminator continuation (finishString): slice + join + Ok.

unicode_fn: String

\uXXXX reader head (parseUnicode): readHex4 + codepoint.

codepoint_fn: String

Codepoint surrogate filter (parseUnicodeCodePoint).

apply_fn: String

Decoded-codepoint continuation (applyCodePoint): Char.fromCode + chunk flush back into the scanner.

read_hex_fn: String

Four-hex-digit reader (readHex4), separately fueled on count climbing to the literal bound 4.

hex_val_fn: String

User hex-digit valuation (hexVal : String -> Option<Int>).

high_surrogate_fn: String

High-surrogate guard (isHighSurrogate): cp >= MIN && ….

low_surrogate_fn: String

Low-surrogate guard (isLowSurrogate).

producer_fn: String

Producer wrapper (escapeJsonString): fold(String.chars(s), "").

fold_fn: String

Producer accumulator fold (escapeJsonChars).

classifier_fn: String

Per-char classifier (escapeJsonChar): two-char escape table

• default to the control classifier.

control_fn: String

Control classifier (escapeControlChar): equality ladder + code < threshold → control escape + printable passthrough.

control_escape_fn: String

Hex control escape (controlCodeEscape): Byte.toHex + 4-char prefix.

ok_ctor: String

Success ctor of the law’s rhs, source spelling ("ParseResult.Ok").

str_ctor: String

String-payload ctor inside the success ctor ("Json.JsonString").

terminator: char

Scan terminator char ('"' — the finish arm’s literal).

escape_char: char

Escape introducer char ('\\' — the escape arm’s literal, also the first char of every two-char escape output).

unicode_letter: char

Hex-escape letter ('u' — second char of the control-escape prefix, the consumer’s unicode arm literal).

pairs: Vec<EscapePairSpec>

Two-char escape table, producer-derived and consumer-aligned.

control_threshold: i64

Control threshold (32): producer hex-escapes below it, the consumer validator rejects below it. Gated <= 256.

high_surrogate_min: i64

cp >= MIN bound of the high-surrogate guard (55296).

low_surrogate_min: i64

cp >= MIN bound of the low-surrogate guard (56320). The Lean renderer probes the scanner SCC’s emitted averStringPosFuel rank itself (it must match the emission byte-for-byte), so the rank is deliberately NOT pinned here.

Trait Implementations

impl Clone for StringEscapeRoundtripPin

fn clone(&self) -> StringEscapeRoundtripPin

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for StringEscapeRoundtripPin

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.