Symbolic Execution and Runtime API

The four headers on this page are the runtime surface of a compiled C* file. When cstarccstarc translates a .c.c file it does not produce a proof object; it produces another C program — one that, when run, drives the symbolic execution engine over the original code, checks the contracts, and either exits quietly or reports where verification failed. Everything that program does, it does by calling functions declared here.

Some of those functions are ones proof code calls directly: cst_get_symbolic_statecst_get_symbolic_state in a proof block, cst_add_axiom_to_headercst_add_axiom_to_header to postpone an obligation, the ENSURE_OKENSURE_OK macro in a hand-written proof-library function. Most are not — they are instrumentation, emitted around the translated statements, and appear in a generated C file by the hundred. Both are documented, because reading a generated file or an error message coming out of one requires knowing what they mean.

Every entry below is therefore tagged by who calls it. Where a whole block of declarations is compiler-only, the block is named and listed rather than documented one function at a time.

symexec.hsymexec.h is the engine header. It declares the lifecycle calls that bracket a verification run, the handful of functions that read and rewrite the symbolic state, the verification-condition and axiom interface, the error reporter, and — behind a banner comment — the AST-builder API through which cstarccstarc feeds the translated program to the engine.

It also declares three opaque typedefs (partial_programpartial_program, expressionexpression, ctypectype) and the two location structs locationlocation and rangerange that appear throughout this page and proof_trace.hproof_trace.h. A rangerange is a start and end locationlocation plus a filename; it is how every call site in a generated file names the piece of user source it came from.

Three calls bracket a run, and all three are emitted by cstarccstarc into the generated mainmain. Hand-written proof code never calls them: by the time a proof block executes, the engine is already up.

void cst_main_entry(bool restore_server_on_exit);

void cst_main_entry(bool restore_server_on_exit);

The main entry of CStar. Should call before everything else.

• bool — restore_server_on_exit A flag to indicate whether to restore the HOL server on exit.
• raises — Exits with non-zero code if failed.

void cst_main_exit(void);

void cst_main_exit(void);

The main exit of CStar. Should call before returning from main.

void cst_symbolic_engine_init(void);

void cst_symbolic_engine_init(void);

Initializes the symbolic execution engine. Should call before any symbolic execution related operations.

cst_main_entrycst_main_entry takes a flag deciding whether the HOL Light server’s theory state is rolled back when the process exits — the header’s @param@param line names the parameter’s type as well as its name, which is why it reads oddly above. cst_symbolic_engine_initcst_symbolic_engine_init is separate because the prover connection and the symbolic engine are separate services: a run that only manipulates terms and theorems needs the first but not the second.

The symbolic state is the assertion the engine believes at the current program point: an hprophprop describing the heap, conjoined with the pure facts in scope. It is a term like any other, and a proof block gets at it through these five functions.

term cst_get_symbolic_state(void);

term cst_get_symbolic_state(void);

Gets the current symbolic state.

• returns — A term for the symbolic state.
• raises — Exits if the symbolic state is unavailable, e.g., after a return statement.
• raises — Returns empty_termempty_term and sets error status if cannot parse.

bool cst_check_symbolic_state(void);

bool cst_check_symbolic_state(void);

Checks whether a symbolic state is currently available.

• returns — truetrue if cst_get_symbolic_statecst_get_symbolic_state would succeed, otherwise falsefalse.

term cst_get_symbolic_state_with_exists(void);

term cst_get_symbolic_state_with_exists(void);

Gets the current symbolic state, with existential binders added properly.

• returns — A term for the symbolic state.
• raises — Exits if the symbolic state is unavailable, e.g., after a return statement.
• raises — Returns empty_termempty_term and sets error status if cannot parse.

void cst_set_symbolic_state(thm th);

void cst_set_symbolic_state(thm th);

Transforms the symbolic state according to the given entailment theorem. This employs a few tactics to rearrange the frames.

• th — The heap entailment theorem.
• raises — Exits if the symbolic state is unavailable, e.g., after a return statement, or the set state cannot be parsed.
• raises — Sets error status if the given theorem is not a entailment, the theorem has hypotheses, or the antecedent does not match the current symbolic state.

const char* cst_pretty_symbolic_state(const char* raw);

const char* cst_pretty_symbolic_state(const char* raw);

Renders a symbolic state captured as engine text (_get_symbolic_state_get_symbolic_state) the way assertions are shown elsewhere (the LSP dump, the VCs).

• raw — The state as engine text, or NULL.
• returns — The rendered assertion, or NULL if rawraw is empty or the prover cannot parse/print it.

cst_check_symbolic_statecst_check_symbolic_state exists because there are program points with no state at all — after a returnreturn, most obviously. Calling cst_get_symbolic_statecst_get_symbolic_state there exits the process; calling cst_check_symbolic_statecst_check_symbolic_state first lets a caller such as the LSP daemon skip the field and carry on. cst_pretty_symbolic_statecst_pretty_symbolic_state is the printer used by the error reporter, and is deliberately built never to fail or to leave an error status behind: it runs while a failure is already being reported.

Not every obligation the engine raises is discharged where it arises. Safety side conditions and postponed proof goals are collected and printed at the end of the run, and cst_add_axiom_to_headercst_add_axiom_to_header is how a proof deliberately defers one.

const char* cst_print_vc(void);

const char* cst_print_vc(void);

Renders the verification conditions as a JSON object with a verification_conditionsverification_conditions array and an axiomsaxioms array.

• returns — The rendered verification-conditions text (GC-managed).

int cst_set_ignore_unsafe_vc_flag(bool flag);

int cst_set_ignore_unsafe_vc_flag(bool flag);

Toggles if printing safety verification conditions.

• flag — Ignore or not.
• returns — zero.

bool cst_check_ignore_unsafe_vc_flag(void);

bool cst_check_ignore_unsafe_vc_flag(void);

Checks if printing safety verification conditions.

• returns — truetrue if ignoring safety verification conditions, otherwise falsefalse.

thm cst_add_axiom_to_header(term tm);

thm cst_add_axiom_to_header(term tm);

A user-side wrapper for creating a temporary axiom that intended to be proved later.

• tm — The term for the axiom.
• returns — A theorem for the axiom.
• raises — Returns empty_theoremempty_theorem and sets error status if tmtm is not of :bool:bool type.

int cst_get_axiom_count(void);

int cst_get_axiom_count(void);

Gets the number of axioms to be proved.

• returns — The number of axioms to be proved.

term cst_get_axiom_to_be_prove(int i);

term cst_get_axiom_to_be_prove(int i);

Gets the i-th axiom to be proved.

• i — The index of the axiom.
• returns — The term for the i-th axiom to be proved.
• raises — Returns a truetrue term if ii is out of bounds.

cst_print_vccst_print_vc renders everything collected as a JSON object with a verification_conditionsverification_conditions array and an axiomsaxioms array — the format cstarc --vccstarc --vc and the editor integration both consume. The ignore-unsafe flag controls whether the memory-safety side conditions are included; it is set from the command line, and the check function lets emitted code query it. Verification Condition Generation explains where these conditions come from and how to read the output.

cst_add_axiom_to_headercst_add_axiom_to_header is the escape hatch. It turns a term into a theorem without proving it, records the term as an outstanding obligation, and lets the run continue; cst_get_axiom_countcst_get_axiom_count and cst_get_axiom_to_be_provecst_get_axiom_to_be_prove walk the list afterwards. A run with a non-empty axiom list is not a completed proof.

const char* cst_print_assertion(term tm);

const char* cst_print_assertion(term tm);

Serialize a HOL separation-logic assertion for the active engine.

char* cst_purify_entailment(const char* ant, const char* con, int num_scope,
                            char** scopes);

char* cst_purify_entailment(const char* ant, const char* con, int num_scope,
                            char** scopes);

Run the active engine's entailment-purification strategy.

cst_print_assertioncst_print_assertion is the canonical renderer for separation-logic assertions: the symbolic-state dumps, the verification conditions and the LSP output all go through it, so what you read in one place is spelled the same way in the others.

cst_purify_entailmentcst_purify_entailment runs the engine’s purification strategy over an entailment given as text — antecedent, consequent, and the scope names that bind its free variables — and returns the residual goal. This is the machinery behind the strategy files registered with cst_add_strategy_to_headercst_add_strategy_to_header; Purifying Entailments with Strategies describes what a strategy file contains and how the unfold, fold and cancel rules inside it drive this call.

The engine does not throw. Nearly every call sets a status that the caller is expected to check, and the emitted verifier checks it after every statement it emits.

void cst_exit_on_error(void);

void cst_exit_on_error(void);

Exits the program if get_last_status()get_last_status() is not OK, reporting the error and, under it, wherever the trace says it happened.

• loc — Unused; the trace carries the location. See cst_exit_on_error_with_loccst_exit_on_error_with_loc.
• raises — Exits if the last status is not OK.

void cst_exit_on_error_with_loc(range ran);

void cst_exit_on_error_with_loc(range ran);

If error, exits with the given location string for error reporting.

• ran — The location range for error reporting.
• raises — Exits if the last status is not OK.

void cst_record_last_loc_for_report(const char* loc);

void cst_record_last_loc_for_report(const char* loc);

Records the last location for reporting purposes.

• loc — The location string to record.

void cst_set_debug(bool debug);

void cst_set_debug(bool debug);

Set the runtime debug flag used when feeding program texts to the symbolic engine. The generated program calls this once at startup with its CST_DEBUG value.

• debug — Whether to print each fed header segment.

bool cst_check_debug(void);

bool cst_check_debug(void);

Check the runtime debug flag.

• returns — Whether the debug flag is set.

cst_exit_on_errorcst_exit_on_error is the check the compiler emits: if the last status is not OK, it prints the error together with the location the trace recorded and exits. Its doc comment still documents a locloc parameter that the declaration no longer takes — the location now comes from proof_trace.hproof_trace.h rather than from the argument, and cst_exit_on_error_with_loccst_exit_on_error_with_loc is the older form that names the range explicitly. cst_record_last_loc_for_reportcst_record_last_loc_for_report is the matching setter for code paths that have a location string but no rangerange.

The two debug functions gate the tracing of program segments as they are fed to the engine. The generated program calls cst_set_debugcst_set_debug once at startup with the value of its CST_DEBUGCST_DEBUG macro, so cstarc -DCST_DEBUG=1cstarc -DCST_DEBUG=1 turns the segment dump on without recompiling the runtime.

int cst_checkpoint(void);

int cst_checkpoint(void);

Checkpoint the server's theory state. Returns an id for cst_restore.

void cst_restore(int id);

void cst_restore(int id);

Roll the server's theory state back to a cst_checkpoint id.

• raises — Fails if the given id is invalid.

void cst_resume(void);

void cst_resume(void);

Rebuild the prover connection after cst_checkpoint_fork(). Does NOT touch libsac (its state is already in memory).

• raises — Fails if cannot re-initialize the prover connection.

These three are a prototype, used by the LSP daemon and not intended for proof code. A verification run accumulates state in two places at once: the engine’s in-process symbolic state, and the HOL Light server’s global theory state. Resuming from a mid-proof point means capturing both, so the daemon checkpoints the server and fork()fork()s to freeze the engine’s memory by copy-on-write. The prover connection is not fork-safe, which is why it is dropped before the fork and rebuilt on each side afterwards — that rebuild is what cst_resumecst_resume does. Expect the interface to change.

Everything after the header’s AST builder APIAST builder API banner exists so that cstarccstarc can hand the engine a program to symbolically execute. The compiler walks the C source it is translating and emits, for each construct, a call that reconstructs that construct as an engine-side AST node: make_int_type()make_int_type() for a type, make_binary_expr(...)make_binary_expr(...) for an expression, make_while_condition(...)make_while_condition(...) for a loop head, make_cst_require(...)make_cst_require(...) for a contract clause. The results are threaded together and pushed into the engine.

The int opint op arguments of make_unary_exprmake_unary_expr, make_binary_exprmake_binary_expr, make_assignmake_assign and make_inc_decmake_inc_dec are drawn from four enumerations the header declares just above the builders: bin_opbin_op (the eighteen binary operators, BINOP_MULTIPLYBINOP_MULTIPLY through BINOP_LOGICAL_ORBINOP_LOGICAL_OR), assign_opassign_op (plain assignment and the ten compound forms), unary_opunary_op (UNOP_ADDRESSUNOP_ADDRESS, UNOP_DEREFUNOP_DEREF, the arithmetic signs, and the two negations) and incdec_opincdec_op (pre- and post- increment and decrement). The parameters are typed intint rather than by the enum, so a generated file shows the numeric constant.

Two further declarations belong to the same internal tier. cst_feed_program_segment_with_loccst_feed_program_segment_with_loc is the call that actually pushes a built segment into the engine together with the source range it came from — the emitted counterpart to everything above. MEMSTREAM_TO_GCMEMSTREAM_TO_GC is a convenience macro used inside the runtime to capture a printer’s output into a garbage-collected string; it opens a memory stream, runs its body, and copies the result onto the GC heap.

Many engine and prover calls take a list — a list of terms, of theorems, of term pairs, of strings. C has no list literal, so the runtime supplies five variadic macros that build one from an argument list. Emitted code uses them constantly; hand-written proof code may use them too, and they are the clearest way to pass a list.

#define TERM_LIST(...)                                                    \
  term_list_n(sizeof((term[]){__VA_ARGS__}) / sizeof(term) __VA_OPT__(, ) \
                                                  __VA_ARGS__)

#define TERM_LIST(...)                                                    \
  term_list_n(sizeof((term[]){__VA_ARGS__}) / sizeof(term) __VA_OPT__(, ) \
                                                  __VA_ARGS__)

#define THM_LIST(...)                                                  \
  thm_list_n(sizeof((thm[]){__VA_ARGS__}) / sizeof(thm) __VA_OPT__(, ) \
                                                __VA_ARGS__)

#define THM_LIST(...)                                                  \
  thm_list_n(sizeof((thm[]){__VA_ARGS__}) / sizeof(thm) __VA_OPT__(, ) \
                                                __VA_ARGS__)

#define TERM_PAIR_LIST(...)                             \
  term_pair_list_n(sizeof((term_pair[]){__VA_ARGS__}) / \
                   sizeof(term_pair) __VA_OPT__(, ) __VA_ARGS__)

#define TERM_PAIR_LIST(...)                             \
  term_pair_list_n(sizeof((term_pair[]){__VA_ARGS__}) / \
                   sizeof(term_pair) __VA_OPT__(, ) __VA_ARGS__)

#define STRING_LIST(...)                                                      \
  string_list_n(sizeof((char*[]){__VA_ARGS__}) / sizeof(char*) __VA_OPT__(, ) \
                                                     __VA_ARGS__)

#define STRING_LIST(...)                                                      \
  string_list_n(sizeof((char*[]){__VA_ARGS__}) / sizeof(char*) __VA_OPT__(, ) \
                                                     __VA_ARGS__)

#define CONST_STRING_LIST(...)                               \
  const_string_list_n(sizeof((const char*[]){__VA_ARGS__}) / \
                      sizeof(const char*) __VA_OPT__(, ) __VA_ARGS__)

#define CONST_STRING_LIST(...)                               \
  const_string_list_n(sizeof((const char*[]){__VA_ARGS__}) / \
                      sizeof(const char*) __VA_OPT__(, ) __VA_ARGS__)

Each macro computes its length from a compound literal — sizeof((term[]){...}) / sizeof(term)sizeof((term[]){...}) / sizeof(term) — and forwards it with the arguments to a variadic backend. Those five backends are the functions that do the work:

proof_util.hproof_util.h is the support header for proof-library code: the error-handling macros that every library function is written around, and the string helpers those functions use to build messages. Unlike the rest of this page it is aimed squarely at hand-written code — an operation body, a glgl function, a helper in a user proof library.

The prover client never throws and never returns an error code. Instead every call leaves a status behind, readable through get_last_status()get_last_status(), together with a message readable through get_last_error()get_last_error(). A function that calls three prover primitives in a row must check the status after each one, and the value it received in the meantime is meaningless if the status is not OK.

Writing those checks by hand is unbearable, so proof-library functions follow a fixed shape instead. The function declares its result variable, runs its steps with a checking macro after each, and ends with two labels:

thm my_rule(term tm) {
  thm result = empty_theorem;
  ASSUME_OK();                       // refuse to start with an error pending
  thm h = ASSUME(tm);
  ENSURE_OK("my_rule: ASSUME failed on %s", cstr_term(tm));
  result = ...;
  ENSURE_OK("");                     // propagate the callee's own message
  return result;
err:                                 // a step failed: record and fall through
  ERR_FUN_PUTS("my_rule", cstr_term(tm));
def:                                 // the default exit: status already set
  return empty_theorem;
}

thm my_rule(term tm) {
  thm result = empty_theorem;
  ASSUME_OK();                       // refuse to start with an error pending
  thm h = ASSUME(tm);
  ENSURE_OK("my_rule: ASSUME failed on %s", cstr_term(tm));
  result = ...;
  ENSURE_OK("");                     // propagate the callee's own message
  return result;
err:                                 // a step failed: record and fall through
  ERR_FUN_PUTS("my_rule", cstr_term(tm));
def:                                 // the default exit: status already set
  return empty_theorem;
}

Two labels, two meanings. err:err: is where a failed step jumps after the failure has been recorded, and it is the place to append the function’s own name and arguments to the error trail. def:def: is the bare default exit — reached by ASSUME_OKASSUME_OK when the function was entered with an error already pending, and fallen into from err:err:. Both return the function’s empty value, leaving the status set so the caller’s own ENSURE_OKENSURE_OK sees it.

The macros divide along the same lines. ASSUME_OKASSUME_OK guards the entry and jumps to defdef. ENSURE_OKENSURE_OK and ENSURE_CONDENSURE_COND check a step and jump to errerr, recording a message on the way. CHECK_OK_OR_RETCHECK_OK_OR_RET and CHECK_OK_OR_GOTOCHECK_OK_OR_GOTO are the recovering forms: they clear the status and take a normal exit, for a step whose failure is expected and handled. TRY_BEGINTRY_BEGIN / TRY_ENDTRY_END bracket a region in which errors accumulate silently instead of printing, so that a strategy may attempt something and back out without noise.

#define NOT_OK (get_last_status() != HOL_STATUS_OK)

#define NOT_OK (get_last_status() != HOL_STATUS_OK)

Macro to check if the last status is not OK.

• returns — True if the last status is not OK, false otherwise.

#define IN_TRY (proof_is_in_try() == true)

#define IN_TRY (proof_is_in_try() == true)

Macro to check if currently inside a try block.

• returns — True if inside a try block, false otherwise.

#define TRY_BEGIN() proof_try_begin()

#define TRY_BEGIN() proof_try_begin()

Macro to mark the beginning of a try block.

#define TRY_END() proof_try_end()

#define TRY_END() proof_try_end()

Macro to mark the end of a try block.

#define SET_OK()          \
  do {                    \
    set_status_error(""); \
    set_status_ok();      \
    proof_clear_errors(); \
  } while (0)

#define SET_OK()          \
  do {                    \
    set_status_error(""); \
    set_status_ok();      \
    proof_clear_errors(); \
  } while (0)

Macro to set the last status to OK.

#define PUTS_ERR(...)                                  \
  do {                                                 \
    if (IN_TRY) {                                      \
      proof_accumulate_error(gc_sprintf(__VA_ARGS__)); \
    } else {                                           \
      log_caught_error(__VA_ARGS__);                   \
    }                                                  \
  } while (0)

#define PUTS_ERR(...)                                  \
  do {                                                 \
    if (IN_TRY) {                                      \
      proof_accumulate_error(gc_sprintf(__VA_ARGS__)); \
    } else {                                           \
      log_caught_error(__VA_ARGS__);                   \
    }                                                  \
  } while (0)

Macro to print an error message, and if inside a try block, accumulate the error message instead of printing it immediately.

#define ASSUME_OK()                                       \
  do {                                                    \
    if (NOT_OK) {                                         \
      PUTS_ERR("ASSUME_OK failed: %s", get_last_error()); \
      goto def;                                           \
    }                                                     \
  } while (0)

#define ASSUME_OK()                                       \
  do {                                                    \
    if (NOT_OK) {                                         \
      PUTS_ERR("ASSUME_OK failed: %s", get_last_error()); \
      goto def;                                           \
    }                                                     \
  } while (0)

Macro to assume the last status is OK, and if not, print the last error message and goto a defdef label.

#define CHECK_OK_OR_RET(val)                                     \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      return val;                                                \
    }                                                            \
  } while (0)

#define CHECK_OK_OR_RET(val)                                     \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      return val;                                                \
    }                                                            \
  } while (0)

Macro to check if the last status is OK, and if not, depress previous error and return a specified value.

• val — The value to return if the last status is not OK.

#define CHECK_OK_OR_GOTO(lab)                                    \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      goto lab;                                                  \
    }                                                            \
  } while (0)

#define CHECK_OK_OR_GOTO(lab)                                    \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      goto lab;                                                  \
    }                                                            \
  } while (0)

Macro to check if the last status is OK, and if not, depress previous error and goto a specified label.

• lab — The label to goto if the last status is not OK.

#define ENSURE_OK(msg, ...)                                                   \
  do {                                                                        \
    if (NOT_OK) {                                                             \
      PUTS_ERR("ENSURE_OK failed: %s", get_last_error());                     \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

#define ENSURE_OK(msg, ...)                                                   \
  do {                                                                        \
    if (NOT_OK) {                                                             \
      PUTS_ERR("ENSURE_OK failed: %s", get_last_error());                     \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

Macro to check if the last status is OK, and if not, print the last error message, record a specified error message and goto the errerr label.

• msg — The error message to record if the last status is not OK, it can be a format string with variadic arguments.
• ... — The variadic arguments for the error message format string.

#define ENSURE_COND(cond, msg, ...)                                           \
  do {                                                                        \
    if (!(cond)) {                                                            \
      PUTS_ERR("ENSURE_COND failed: %s", get_last_error());                   \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

#define ENSURE_COND(cond, msg, ...)                                           \
  do {                                                                        \
    if (!(cond)) {                                                            \
      PUTS_ERR("ENSURE_COND failed: %s", get_last_error());                   \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

Macro to check a condition, and if not satisfied, print the last error message, record a specified error message and goto the errerr label.

• cond — The condition to check.
• msg — The error message to record if the condition is not satisfied, it can be a format string with variadic arguments.
• ... — The variadic arguments for the error message format string.

#define ERR_FUN_PUTS(func, ...)                          \
  do {                                                   \
    err_fun_puts(func __VA_OPT__(, ) __VA_ARGS__, NULL); \
  } while (0)

#define ERR_FUN_PUTS(func, ...)                          \
  do {                                                   \
    err_fun_puts(func __VA_OPT__(, ) __VA_ARGS__, NULL); \
  } while (0)

Macro to append a message to the error log with the function name and variadic arguments.

• func — The function name.
• ... — The variadic arguments of the message, should be a list of strings.

Every message above is built with gc_sprintfgc_sprintf, and every value spliced into one is rendered by a cstr_*cstr_* printer. Both allocate on the garbage-collected heap, so a message may be built and forgotten without bookkeeping, and neither ever fails — an error path must not itself be able to fail.

char* gc_sprintf(const char* fmt, ...);

char* gc_sprintf(const char* fmt, ...);

Formats a string with the given format and arguments with GC_MALLOC.

• fmt — The format string.
• ... — The variadic arguments for the format string.
• returns — A pointer to the formatted string.
• raises — Never fails.

char* gc_strcat(const char* s1, const char* s2);

char* gc_strcat(const char* s1, const char* s2);

Concatenates two strings.

• s1 — The first string.
• s2 — The second string.
• returns — A pointer to the concatenated string.
• raises — Never fails.

The printers cover the object types the prover client traffics in, each producing a colorized rendering suitable for dropping straight into a message:

The try-state plumbing (proof_try_beginproof_try_begin, proof_try_endproof_try_end, proof_is_in_tryproof_is_in_try), the error-recording functions (proof_accumulate_errorproof_accumulate_error, proof_flush_errorsproof_flush_errors, proof_clear_errorsproof_clear_errors, set_status_error_and_record_msgset_status_error_and_record_msg, err_putserr_puts, err_fun_putserr_fun_puts), strip_ansi_colorstrip_ansi_color, and the ANSI color code and wrapper macros are runtime-internal: they exist so the macros above can be written, and proof code should reach for the macro rather than the function underneath.

A verification failure has two locations: the proof step that failed, and the place in the user’s source that step was checking. proof_trace.hproof_trace.h is what connects them. The emitted verifier brackets every proof statement with a location record, pushes a frame for every glgl-function activation together with its arguments, and on failure turns the accumulated records into a source-level stack trace: the failing statement, one line per activation, and the enclosing C* function.

This makes the header unusual on this page — its output is read by users constantly, in every error message the toolchain prints, but its API is called only by generated code. Term and theorem arguments are captured as bare handles at call time, a pointer store with no round trip to the prover, and stringified lazily only if a failure is actually reported, so the instrumentation costs nearly nothing on the passing path.

The first block is what cstarccstarc emits around proof-block statements and glgl-function calls.

void cst_record_last_stmt(range stmt, const char* text, const char* fn,
                          range fn_loc);

void cst_record_last_stmt(range stmt, const char* text, const char* fn,
                          range fn_loc);

Open a proof-block statement window: record the statement being run and the C* function that encloses the proof block.

• stmt — The statement's source range.
• text — The statement's source text.
• fn — The enclosing C* function's name.
• fn_loc — The proof block's source range.

void cst_record_gl_stmt(range stmt, const char* text);

void cst_record_gl_stmt(range stmt, const char* text);

Record the statement being run inside a gl function body.

• stmt — The statement's source range.
• text — The statement's source text.

void cst_frame_push(const char* fn);

void cst_frame_push(const char* fn);

Push a frame for a gl-function activation.

• fn — The gl function's name.

void cst_frame_arg_term(const char* name, term tm);

void cst_frame_arg_term(const char* name, term tm);

Record a term-valued argument of the innermost frame.

• name — The parameter's name.
• tm — The term handle; stringified only if a failure is reported.

void cst_frame_arg_thm(const char* name, thm th);

void cst_frame_arg_thm(const char* name, thm th);

Record a theorem-valued argument of the innermost frame.

• name — The parameter's name.
• th — The theorem handle; stringified only if a failure is reported.

void cst_frame_arg_int(const char* name, long long v);

void cst_frame_arg_int(const char* name, long long v);

Record an integer-valued argument of the innermost frame.

• name — The parameter's name.
• v — The value.

void cst_frame_arg_str(const char* name, const char* s);

void cst_frame_arg_str(const char* name, const char* s);

Record a string-valued argument of the innermost frame.

• name — The parameter's name.
• s — The value; borrowed, must outlive the activation.

void cst_frame_pop(void);

void cst_frame_pop(void);

Pop the innermost frame. A pop at depth 0 is a no-op.

The second block is emitted around the program statements — the translated user code that goes to the symbolic engine, as opposed to the proof steps that run alongside it.

void cst_trace_note_program_stmt(range stmt, const char* text);

void cst_trace_note_program_stmt(range stmt, const char* text);

Note the program statement about to be fed to the symbolic engine.

• stmt — The statement's source range.
• text — The statement as the engine sees it; collapsed to one line.

void cst_trace_note_unlocated_stmt(const char* text);

void cst_trace_note_unlocated_stmt(const char* text);

Note a program segment that carries no source location (a header line the runtime synthesizes, say).

• text — The segment as the engine sees it.

void cst_trace_enter_function(const char* fn, range fn_loc);

void cst_trace_enter_function(const char* fn, range fn_loc);

Enter the C* function the following statements belong to.

• fn — The function's name.
• fn_loc — The range of the function's header.

void cst_trace_leave_function(void);

void cst_trace_leave_function(void);

Leave the current C* function.

The header’s third block is marked runtime-internal and is not documented here: it is the reporting side — building and printing the trace, the signal-handler path, the depth and truncation hooks the TRYTRY recovery uses, and the reset. Its functions are called by the runtime’s own error reporter, never by emitted or hand-written code.

symexec.hsymexec.h is the engine: three lifecycle calls, five functions over the symbolic state governed by the read-prove-commit discipline, the verification-condition and axiom interface, purification, the error reporter, and — behind its banner — the 74 make_*make_* builders that exist so the compiler can describe a program to the engine. proof_runtime.hproof_runtime.h supplies the list constructors emitted code needs without linking a user library. proof_util.hproof_util.h is the error-handling discipline hand-written proof code is built around: status checks, the err:err: / def:def: label pair, and the GC-allocated printers that fill in the messages. proof_trace.hproof_trace.h is why those messages point at user source.

Between them they account for everything a generated C file does apart from the actual inference — and the inference is the prover client’s job.