Explain verifier inputs and examples in the Gradio introduction

demo/app.py

@@ -130,8 +130,30 @@ def create_app(examples_directory=None):
         session = gr.State(UISession())
         ticket = gr.State(None)
         reference_function = gr.State(None)
-        gr.Markdown("# Decompiler verifier\nCompare a C candidate with a binary function across shared random seeds.",
-                    elem_id="intro")
+        gr.Markdown("""# Decompiler verifier
+Check whether candidate C behaves like an original binary function on shared, seeded random inputs.
+
+Choose an **example** below to fill in the inputs, or upload an **x86-64 ELF binary**, enter the
+**function start address**, and paste complete **Candidate C**. Set **Candidate function name**
+to the C function to test. Examples include matching implementations, deliberate bugs, real
+`factor` binary functions, and saved **Ghidra exports at the end of the list**. Some Ghidra
+exports agree; others reveal mismatches or compile/type errors. **Reference C**, when shown,
+is a reading aid; verification runs the binary.
+
+Open **Bindings** to map candidate `extern` names to original binary addresses: `globals`
+for shared data and `callees` for called functions. Bound callees receive deterministic
+synthetic returns. In the same panel, `original_prototype` is the **trusted prototype**: a C
+declaration describing the original function's argument and return types, such as
+`unsigned original(unsigned x);`. Supply it from your knowledge of the binary, independently
+of the candidate's guessed types; it controls input generation and return interpretation.
+The examples supply it. You can also specify callee interfaces and memory ranges there.
+
+Open **Run settings** to adjust seeds, instruction budget, compiler, or flags, then click
+**Verify**. Inspect the assembly panes, per-seed results, and first mismatch, or download the
+JSON report. Agreement covers the tested inputs and comparison scope described below.
+**Try changing the Candidate C**—an operator, constant, or type—and verify again with the
+same seeds to see how the assembly and results change.
+""", elem_id="intro")
         # Render inputs later so the example picker can sit above setup.
         binary = gr.File(label="Binary", type="filepath", file_count="single", render=False, elem_id="binary")
         function = gr.Textbox(label="Function start address", placeholder="0x401000",
@@ -154,7 +176,7 @@ def create_app(examples_directory=None):
                   seed_count, seed_start, instruction_budget, compiler, flags, interfaces]
         example_picker = gr.Examples(examples=examples, inputs=inputs, label="Examples",
                                      example_labels=list(EXAMPLE_LABELS),
-                                     examples_per_page=20,
+                                     examples_per_page=len(examples),
                                      cache_examples=False, elem_id="examples")
         with gr.Row(elem_id="setup"):
             binary.render()