docs: drop the references to the downstream project

The module docs and doc/caliper.md described Caliper as the compilation
target of one particular caller, down to its file paths and gadget names.
State the general case instead: a target for languages that want certified
resource bounds, with downstream layers proving their own claims.

Author: rot256

Caliper/Core.lean

@@ -4,10 +4,10 @@ import Mathlib.Tactic
 # A unit-cost machine model
 
 A small imperative language whose every instruction runs in constant time, intended
-as a compilation target for Clean's witness-generation IR
-(`Clean/Circuit/WitnessIR.lean`). Programs carry machine-checked upper bounds on
-running time and memory. Design rationale, the lowering contract and the trust
-boundary are in `doc/caliper.md`; this module is the machine.
+as a compilation target for languages that want certified resource bounds. Programs
+carry machine-checked upper bounds on running time and memory. Design rationale, the
+lowering contract and the trust boundary are in `doc/caliper.md`; this module is the
+machine.
 
 Buffers, not a RAM: the machine has an unbounded supply of independent, named
 buffers, so the only separation fact a proof ever needs is `b₁ ≠ b₂` on buffer
@@ -56,7 +56,7 @@ abbrev Reg := ℕ
 /-- Buffer names. Static: part of the syntax, never a runtime value. -/
 abbrev BufId := ℕ
 
-/-- Machine words. Fixed at `w = 64` for Clean's witgen backend. -/
+/-- Machine words. Fixed at `w = 64` by the `Caliper64` surface. -/
 abbrev Word (w : ℕ) := BitVec w
 
 variable {w : ℕ}

Caliper/Render.lean

@@ -12,7 +12,7 @@ Control flow renders structurally: `ifnz r<c> { … } else { … }`, and `whileN
 verdict register, mirroring the `Exec` rules (guard, test, body, repeat). `skip`
 renders as `skip`, since compiled code can contain genuine no-ops.
 
-The printer is for *reading* programs, builder output or compiled witgen code. It is
+The printer is for *reading* programs, builder output or compiled code. It is
 not part of any trusted surface and nothing is proved about it.
 -/
 

Caliper/W64.lean

@@ -4,8 +4,8 @@ import Caliper.Builder
 /-!
 # Caliper at word size 64
 
-The Caliper core is generic over the word size `w`, but in practice, and in
-particular for Clean's witgen backend, the word size is 64. This file is the surface
+The Caliper core is generic over the word size `w`, but in practice, and for every
+intended backend, the word size is 64. This file is the surface
 programs and specs should be written against: reducible `abbrev`s fixing `w := 64`,
 so that
 

doc/caliper.md

@@ -2,10 +2,8 @@
 
 Caliper is a deep-embedded imperative language whose every instruction runs in
 constant time, designed as a compilation target for languages that want certified
-resource bounds; in particular the witness-generation IR of the
-[Clean](https://github.com/rot256/clean) zk-circuit project, which depends on this
-library. Programs carry machine-checked upper bounds on running time and on
-allocated memory.
+resource bounds, witness-generation IRs among them. Programs carry machine-checked
+upper bounds on running time and on allocated memory.
 
 ## Files
 
@@ -19,14 +17,13 @@ allocated memory.
 | `Liveness.lean` | Backward liveness analysis (`Stmt.liveBefore`), inferred peak register pressure (`Stmt.regPeak`/`Stmt.regPeak₀`), the live-ins + writes bound, the combined buffers-plus-registers judgment (`SpaceBound`), and `Exec.straight_total_footprint_le` |
 | `W64.lean` | Fixed 64-bit surface: namespace `Caliper64` of reducible `abbrev`s pinning `w := 64` |
 
-## Where the rest of the pipeline lives
+## Scope
 
 This repository contains the machine: syntax, cost semantics, program logic,
-builder surface, renderer, and the fixed 64-bit surface `Caliper64`. The layers
-on top of it (the witness-generation compiler, the prime-field gadget library
-`Fp w p`, the `TimedCircuit` budgeted-witgen structure) live in the
-[Clean](https://github.com/rot256/clean) project, which depends on this library.
-Claims about those layers are stated and proved there, not here.
+builder surface, renderer, and the fixed 64-bit surface `Caliper64`. Layers built
+on top of it, such as a compiler targeting the machine or a gadget library, live in
+the projects that depend on this one; claims about those layers are stated and
+proved there, not here.
 
 ## Design decisions
 
@@ -416,9 +413,9 @@ their own concrete numerals. `#print axioms <theorem>` is the audit tool.
 ## Caveats / next steps
 - Natural next steps: a performant runner beyond the reference interpreter, and
   refining the cost model toward a concrete backend.
-- A `Proc` record bundling `code`/`Pre`/`Post`/`time`/`space`/`spec` (mirroring
-  Clean's `FormalCircuit`) would package subroutines more tightly; the examples
-  inline this pattern with plain `have`s for now.
+- A `Proc` record bundling `code`/`Pre`/`Post`/`time`/`space`/`spec` would package
+  subroutines more tightly; the examples inline this pattern with plain `have`s for
+  now.
 - Registers in the examples use fixed conventions (callee-clobbered scratch); a
   register-window or parameterized-register discipline is mechanical to add
   (distinctness side conditions close by `decide`).