README.md

Example proofs

This directory is the Rocq theory LinuxProcessSemantics.Examples (opam package rocq-linux-process-semantics-examples). Each <name>_ns/ directory proves that two binaries have the same observable behavior. The source binary is a C program. The target binary is a Zig program that does the same work. "ns" means "no start files": the C program uses the minimal start code in crt/_start.S.

Read this document if you want to read an example proof or add an example. Read ../Common/README.md for the proof library.

The examples

Example	Program	Main library lemma
rwx_flag_ns	Store a byte and exit with it. The source has one segment that is writable and executable.	CatSim.cat_omni_strong_equiv_te

Two directories are not equivalence proofs:

• patchclassify_demo/ is an instance of the patch-classifier statement.
• measure_lib_demo/ is an instance of each part of MeasureLib.v.

Files of an example

File	Contents
source/program.c	The C program. source/cflags.txt and source/ldflags.txt are optional extra compiler and linker flags.
target/program.zig, target/flags.txt	The Zig program and its extra compiler flags (one line, can be empty).
SourceMemImage.v, TargetMemImage.v, *_seg_*.hex	Snapshots of the two binaries, made by elf-snapshot. They are in the repository, so you can build the proofs without a cross-compiler. The binaries are not in the repository.
<name>_defs.v	The specification of the program output, facts about the images, and shared tactics.
<name>_source.v, <name>_target.v	Symbolic execution of each binary: one result lemma per input case. Large examples split these files further.
Proof.v	The top-level proof.
<name>_code.v	Generated by dune from the snapshots (gen-fd-lemmas): a fetch lemma and a decode lemma for each instruction.
Checker.v	Generated by dune (tools/gen_checker.py): the top-level check.

The two generated files are only in _build/default/theories/Examples/<name>/. A generator error cannot make a proof pass: the _code.v lemmas are checked by vm_compute, and Checker.v is a type check.

What the proof must show

Proof.v must end with these two theorems:

Theorem omni_strong_universal : OmniEquivalence.omni_strong_universal_T
  (mkImage SourceMemImage.Source.loaded_segments
           SourceMemImage.Source.init_pc SourceMemImage.Source.phdrs)
  (mkImage TargetMemImage.Target.loaded_segments
           TargetMemImage.Target.init_pc TargetMemImage.Target.phdrs).

Theorem strong_universal : Equivalence.strong_universal_T
  (mkImage SourceMemImage.Source.loaded_segments
           SourceMemImage.Source.init_pc SourceMemImage.Source.phdrs)
  (mkImage TargetMemImage.Target.loaded_segments
           TargetMemImage.Target.init_pc TargetMemImage.Target.phdrs).
Proof. apply OmniEquivalence.strong_universal_iff. exact omni_strong_universal. Qed.

The top-level README explains what strong_universal_T means.

Checker.v does these checks:

1. It ascribes strong_universal to Equivalence.SPEC and omni_strong_universal to OmniEquivalence.OMNI_SPEC. Thus the theorems must have exactly the expected types.
2. It ascribes each image to Equivalence.IMAGE_WF. This makes sure that the image can start, so the theorem is not true only because no valid launch exists.
3. It runs Print Assumptions on both theorems. The only permitted assumptions are functional_extensionality_dep and the PrimInt63, PrimString and PrimArray primitives. Any other assumption (for example, from Admitted) means that the proof is not complete.

Add an example

These steps use the name foo_ns.

1. Make the directory theories/Examples/foo_ns/. Put the C program in source/program.c. Put the Zig program in target/program.zig and its flags in target/flags.txt.

2. Build the source binary with a riscv64-linux-musl-gcc cross-compiler:

   cd theories/Examples/foo_ns/source
   riscv64-linux-musl-gcc -std=gnu17 -march=rv64imafd -Os -static -nostartfiles \
     -fno-builtin -fno-strict-aliasing $(grep -hv '^#' cflags.txt 2>/dev/null) \
     -Wl,-z,separate-code -Wl,--error-rwx-segments \
     ../../crt/_start.S program.c -o program
   cd -

   If source/ldflags.txt exists, use its lines that do not start with # in place of the two -Wl options. --error-rwx-segments needs binutils 2.39 or later.

3. Build the target binary with zig:

   zig build-exe theories/Examples/foo_ns/target/program.zig \
     $(cat theories/Examples/foo_ns/target/flags.txt) -target riscv64-linux-none \
     -femit-bin=theories/Examples/foo_ns/target/program

4. Make the two snapshots:

   elf-snapshot theories/Examples/foo_ns/source/program \
     theories/Examples/foo_ns/SourceMemImage.v --prefix SourceMemImage \
     --module-name Source --namespace LinuxProcessSemantics.Examples.foo_ns
   elf-snapshot theories/Examples/foo_ns/target/program \
     theories/Examples/foo_ns/TargetMemImage.v --prefix TargetMemImage \
     --module-name Target --namespace LinuxProcessSemantics.Examples.foo_ns

   A different compiler version can make a different binary. Then the addresses in an existing proof are wrong and the build fails.

5. In theories/Examples/dune, copy the two stanzas of an existing example and change the name to foo_ns. These stanzas make foo_ns_code.v and Checker.v.

6. Write a Proof.v that has the two theorems above, with Admitted for omni_strong_universal. Build the example:

   dune build theories/Examples/foo_ns

   Now all files compile, and Print Assumptions shows the Admitted proof. To read the generated lemmas, open _build/default/theories/Examples/foo_ns/foo_ns_code.v.

7. Add foo_ns_defs.v, foo_ns_source.v and foo_ns_target.v. Start each lemma with Admitted. Replace one Admitted at a time, and build only the file that you changed.

8. The example is complete when Print Assumptions shows only the permitted assumptions and rocqchk accepts the compiled checker. After dune build, run python3 .github/check_assumptions.py to check both.

If a new example uses the same system calls as an existing example, copy the _defs.v file of that example and use the same library lemma.

Write the proof

The defs file: agree on the output first

Both binaries must give the same output, so define it once. In foo_ns_defs.v, write a function of the input that gives the output (for example, rev_buf s, or the list of buffers and the exit code). The source proof and the target proof both use this function. Make the function computable, and make it correct before you start the other files.

The defs file also contains:

• source_init_pc_val and target_init_pc_val, proved by vm_compute; reflexivity,
• facts that the buffers of the program are writable and do not overlap read-only segments,
• lemmas about valid_argv for the case split in Proof.v,
• the step tactics, exported to the other files of the example.

Step through a binary

A per-binary file starts with a section over the process input and the launch, for example:

Section SourceProof.

Variable inp : ProcInput.
Local Abbreviation av := (in_argv inp).
Local Abbreviation ev := (in_envp inp).
Local Abbreviation fs0 := (in_fs inp).
Hypothesis Hva : valid_argv av.
Hypothesis Hve : valid_envp ev.
Hypothesis Hvl : valid_launch inp.        (* the E2BIG cap on the launch *)

Variable rsp : word.                    (* the stack pointer *)
Variable rbrk : word.                   (* the initial program break *)
Variable rmb : word.                    (* the mmap base *)
Variable rrnd : EntryDraw.              (* the AT_RANDOM bytes, the stack
                                           VMA's end, and the vDSO's
                                           register and frame leftovers *)
Hypothesis Hsp_lo : (sp_window_lo <= bv_unsigned rsp)%Z.
Hypothesis Hsp_hi : (bv_unsigned rsp <= sp_window_hi)%Z.
Hypothesis Hlau : entry_launch_ok_va Sv48 (mkEntry rsp rbrk rmb rrnd) inp.

Follow these rules:

• Quantify over the ProcInput record, not over its fields. Run.init_machine_state, Run.init_config and State.init_model take the whole record. Separate variables for av and ev would let a lemma mix values from two different inputs.
• Use Local Abbreviation, not Local Notation. Rocq 9.2 gives an error for Notation without parameters.
• Do not declare an abbreviation whose name is already a binder in the file.
• Give the launch draw (EntryDraw: the AT_RANDOM bytes, the stack VMA's end ed_top, and the vDSO's leftover-naming function) a variable. The kernel can choose any value the launch conjunct admits. In the target section, use a different variable (for example, arnd): the two launches are independent.
• Take entry_launch_ok_va as a hypothesis if the proof reads the initial stack or fetches through the overlay. It is the fifth conjunct of Run.valid_entry_va, and it is what bounds the entry block (StepTac.bsb_bound) and what puts sp at or below ed_top, hence the zero-filled stack window at or above sp - 8 MiB (WxExec.mem_clear_wrap). valid_argv and valid_envp no longer bound the block: the strings sit at the top of it, and the exec file name and arch_align_stack's pad are in it too.
• Take valid_launch as well for StepTac.bsb_bound: it is the E2BIG cap bprm_stack_limits computes (fs/exec.c, Linux v6.18.46, commit 1f99e9ab748f).
• A section that reads the auxv needs no variable for the user ID or for the AT_HWCAP value: init_machine_state takes the input, so use (in_uid inp) and (in_hwcap inp).
• Common/ArgvEnv.v proves this scaffolding once. Instantiate it rather than writing argcN, bsb_nw, envp_ptr and the read-backs again.

The section then builds the initial memory in layers: wrap_mem for the initial stack, then wbytes for each store of the start code.

Step through instructions with the tactics of Common/StepTac.v:

• stepi F D does one instruction. F and D are the fetch lemma SF_<addr> and the decode lemma SD_<addr> from foo_ns_code.v.
• stepiv F D v tac does one instruction and writes the value v.
• stepj F D does an unconditional jump.
• norm_pc computes the next program counter. sp_norm simplifies offsets from the stack pointer.
• step_ecall starts a system call. Then a lemma of the behavior file (for example CatSim) continues after it.

For a function that the program calls, prove one lemma for the function, with the return address as a parameter. Then use the lemma at each call.

For long straight-line blocks, the reflective executor SymTac.sym_block is faster than stepi.

Choose the library lemma for each case

In Proof.v, each input case uses exactly one library lemma:

Behavior in this case	Lemma	Each binary must give
writes to standard output, then exit	CatSim.cat_omni_strong_equiv_te	to_wexit ... bufs code, with the same (bufs, code), and a cat_launch fact (see below)
exit only	ExitSim.exit_omni_strong_equiv	to_exit with the same code
brk allocation	AllocSim.alloc_omni_strong_equiv	to_outcomes ... U, with the same outcome set U
one anonymous mmap	MmapSim.mmap_omni_strong_equiv_te	tmw ..., with the same failure and success results
read and write loop that does not stop	StreamSim.stream_omni_strong_equiv	a loop invariant to_rd
every source execution crashes	ErrEscape.err_escape_omni_strong_equiv	source only: msteps to a MachineFault
any shape, any allocator	ShapeAlg.shape_omni_strong_equiv	a realizes derivation of the same shape

Use the crash row only when every execution of the source crashes. If an earlier system call has more than one result, each result must lead to a crash.

State.in_channel_reader says if the far end of standard output has a reader. Run.valid_input pins it present, and Run.valid_input_channel_reader reads that pin back out, so a proof under the ordinary predicate has the reader fact for free. cat_omni_strong_equiv_te takes CatSim.cat_launch, which is one of these:

• bufs = []: the program writes nothing, so the reader does not matter. Give left; left; reflexivity.
• in_channel_reader inp = true: give left; right, and under Run.valid_input that fact is Run.valid_input_channel_reader.
• No reader, and SIGPIPE is fatal (CatSim.sigpipe_fatal: the disposition is the default, the launch declares the SIGPIPE death (State.in_sigpipe_terminal), and in_sigmask inp does not block signal 13). Each first write kills its process with SIGPIPE, so both runs end in the same KillEv. Give right, the sigpipe_fatal fact and a CatSim.wfirst_ok fact for each binary: the first write passes access_ok. This case is reachable only under Run.valid_input_channel_closed, the launch whose reader has gone and which declares the death: Run.valid_input rules it out, because it pins the reader present and the death declined. That predicate no longer gives the SIG_DFL disposition for free, though — it leaves State.in_sigpipe_default unpinned, as Run.valid_input and the other ordinary launch predicates now do (only Run.valid_input_sigpipe_ignored pins it, to the other value), so that conjunct of sigpipe_fatal comes from the launch the proof names rather than from the validity premise.

The lemma does not cover a program that writes when the reader is gone and signal 13 is blocked or ignored. There the first write returns -EPIPE and the program continues, and to_wexit has no node for that return value.

A typical Proof.v:

Theorem omni_strong_universal : OmniEquivalence.omni_strong_universal_T ... .
Proof.
  intros [sp_source brk_source mb_source rnd_source]
         [sp_target brk_target mb_target rnd_target]
    inp Hens Hent Hvalid.
  (* valid_input fixes Sv48, so the entry predicates are the Sv48 ones. *)
  pose proof (valid_input_va_size _ Hvalid) as Hsv48.
  rewrite (valid_entry_sv48 _ _ _ Hsv48) in Hens.
  rewrite (valid_entry_sv48 _ _ _ Hsv48) in Hent.
  destruct Hens as (Hspr & _ & _ & _ & Hlau_source).
  destruct Hent as (Hspa & _ & _ & _ & Hlau_target).
  red in Hvalid.
  repeat (lazymatch type of Hvalid with
          | _ /\ _ => let Hc := fresh "Hc" in destruct Hvalid as [Hc Hvalid]
          end).
  set (argv := in_argv inp) in *.
  rewrite source_init_pc_val, target_init_pc_val.
  destruct (le_lt_dec 2 (length argv)) as [Hge | Hlt].
  - eapply cat_omni_strong_equiv_te;
      [apply source_wexit_ge2 | apply target_wexit_ge2 | ... | (* cat_launch *) ...].
  - eapply cat_omni_strong_equiv_te; [apply source_wexit_lt2 | ...].
Qed.

Run.valid_input gains a conjunct whenever the input class learns to say something new — three of them this revision — so a positional pattern over it names a different clause after each insertion rather than failing. Do not count. Peel it as above: the guard stops the peel at Run.valid_launch, which stays folded, so that clause arrives whole and every other one sits in the context where assumption finds it. Where only one clause is wanted, take it from its accessor lemma — Run.valid_input_va_size, Run.valid_input_abort_terminal, Run.valid_input_image_real, Run.valid_input_urandom, Run.valid_input_vdso, Run.valid_input_hwcap_rv64gc_word — which no insertion can move. The kernel accessors are the ones a start-up proof wants: Run.valid_input fixes eight fields of the build at State.default_kernel's values (Run.recorded_kernel) and leaves kb_thp, kb_aslr, kb_guard, kb_rnd_bits and kb_rseq free, and each fixed field has its accessor — Run.valid_input_vdso, Run.valid_input_vlenb, Run.valid_input_cache, the socket numbers — with Run.valid_input_cache_words, Run.valid_input_vdso_text_pages and Run.valid_input_min_sigframe_size for what the auxv computes from them. Do not assume a value for the five free fields: a start-up proof covers both auxiliary-vector layouts, 27 pairs and 29, by a case split on kb_rseq (in_kernel inp).

Run.valid_entry has five. Its fifth, Run.entry_launch_ok_va, is the one a per-binary section needs, so a positional pattern over it has five parts, not four.

Do not destruct inp. Run.run reads the input through projections, so it reduces when inp is a variable.

Case-split only on properties of the input (for example argc, a byte value, a length). Do not case-split on the machine state.

Speed

Measure the time and the peak memory of each file:

/usr/bin/time -v dune build theories/Examples/foo_ns/foo_ns_source.vo

Try to keep each file below 30 seconds and well below 2 GB.

• Use N or Z for addresses, lengths and counters. Do not use nat.
• Compute closed terms with vm_compute. Do not use simpl or cbn on a term that contains a memory image.
• Keep the image constants opaque (Global Strategy 200, from the header of _code.v).
• Do not use discriminate without a hypothesis name on a goal with large terms. Give the name: discriminate H.
• Split a large proof into more files. Then a change in Proof.v does not compile the step lemmas again.