Function preamble_lines 

pub fn preamble_lines(
    version: &str,
    offline: bool,
    skip_contract: bool,
    paths: &[PathBuf],
) -> Vec<String>

The --verbose preamble execute_command prints before dispatching.

--verbose was the other half of #2401: byte-inert on 13 of 16 sampled commands, because only check, oracle and trace ever received it as a parameter. Rather than invent per-command chatter for 104 commands, this reports what the dispatcher actually resolved and decided — facts the run already computed and then threw away:

• which model paths extract_model_paths pulled out of the parsed command, and their sizes on disk;
• whether the PMAT-237 contract gate ran over them, was disabled with --skip-contract, or did not apply because the command is one of the diagnostic ones the gate deliberately exempts. That last line also explains the audit’s separate observation that --skip-contract has “zero effect” on inspect/validate/tensors: there is nothing for it to skip there, and now the CLI says so instead of staying mute.
• whether --offline is latched.

Pure so it can be asserted directly; the caller prints the lines.