v2 - #6
Merged
Merged
Conversation
Mechanism SOUND + spike-proven (eval-via-spec exact at Flat(4); full-Flat(8) 3-op recognition via equiv in 610us, non-vacuous). But unsafe as ONE delegation: 3-crate blast radius, 72-site/27-file struct ripple, 4 gaps (selection, admit layering, both-present precedence, 2 enumeration-hang guards + a silent-vacuity vector). Split into 3a (representation+eval+admit; move BvExpr to core, PrimSpec pair, eval-via-spec, hang/vacuity guards) -> 3b (selection-by-equiv recognition, Flat(8)^3 payoff). DEFERRED for go/no-go: first foundational theseus-core+eval change, near-workspace-wide allowlist. Spike preserved. L21.
…im REPRESENTATION + eval + admit (NO new recognition). Let PrimDef carry an optional symbolic spec PAIR so a Flat(8)^3 prim is representable/evaluable/admissible/adjointable without a 16.7M-entry table; every recognizer/lowering path rejects a symbolic-only prim EXPLICITLY + INSTANTLY (hang/vacuity guards). Foundational theseus-core + theseus-eval change → highest bar; full adversarial impl-review + L19.
Worker: BvExpr+eval_expr moved to theseus-core (re-export from bveq); PrimSpec (fwd,bwd) pair + PrimDef.symbolic + the workspace-wide symbolic:None ripple; adjoint swaps specs; core::admit spec-presence early-return (AdmitError) before enumerate_values (hang guard); bveq::admit_symbolic BDD mutual-inverse; eval-via-spec (core-native, table-wins precedence); fail-closed guards (bveq_verify_emission empty-table reject, recognize_prim symbolic-only reject). Advisor fix: 1 needless_range_loop in admit_symbolic. Workspace clippy clean; full gate green (core/eval/check/netlist/tisc, goldens UNCHANGED = I1).
… + I1 holds + vacuity guard teeth-proven; F1 I2 self-checker [L19 class], F2 hang bypass, F3 malformed-spec, F4/F5). L21.
…iew — F1 (HIGH) the I2 whole-domain test is a SELF-WRITTEN copy of the eval path (L19 class) not the oracle; F2 partial-table+spec bypasses the hang guards; F3 no spec<->type validation (release silent out-of-range); F4/F5. Each with an L20 reproducing test. Foundational theseus-core+eval → full adversarial re-review + L19.
…eeth-proven [flips under 2 eval corruptions], F2 hang guard teeth-proven [neuter->OOM], F3 release-active malformed-spec reject, F4/F5; 4 LOW residuals for 3b). L21.
…esentation broken) MERGED @ 6513f4b; a Flat(8)^3 prim is representable/evaluable/admissible without a 16.7M table. 3b (recognition payoff) next.
…b in flight; symbolic-BDD recognizer trust core, enumeration wall broken); tip 75ff066
…gy-test OOM The energy tests (crates/theseus-tisc/tests/energy.rs) elaborate CPU-step netlists (~GB) into OnceLock statics while building large balance() transients. libtest runs tests within a binary at --test-threads=ncpu, and glibc's default per-thread arenas keep each thread's freed pages unshared — fragmenting peak RSS to ~86 GB and SIGKILL-ing the maestro gate for theseus tasks under memory pressure (the concrete failure that sent BVEQ slice-3b to a spurious 'failed'). One arena lets the threads share freed memory: peak drops to ~48 GB (measured, 50777088 KB) with no wall-clock regression (4:08). Home is flake.nix targetToolsEnv — the ADR-0019 env seam the maestro daemon, its workers, the gate's cargo test, and dev shells all inherit; confirmed $MALLOC_ARENA_MAX=1 in the devshell and 48 GB end-to-end via nix develop with no explicit env. Rejected alternatives (measured): serializing the test bodies with a mutex (fragmentation is per-arena not per-body — still 82 GB); .cargo/config.toml [env] (reaches build/rustc only, not the test runtime — 81 GB); a target 'runner' (cargo doesn't apply it to the host target without --target — 81 GB).
…im RECOGNITION (the Wall-2 payoff) — SELECTION-BY-EQUIV. For a symbolic-spec prim, iterate the finite arm library, symbolic_exec each candidate, equiv vs the spec RegTransfer, first pass wins (sound by construction). Recognizes a 3-op Flat(8) prim (masked-accum) with NO 16.7M table. Builds on slice-3a (merged). LIVE RECOGNIZER = highest bar; full adversarial impl-review + L19.
…-first doc
Fresh-context Fable adversarial impl-review verdict SHIP-WITH-FIXES:
- A-1 (MAJOR): the shipped selection suite only homed operands at the
identity mapping Reg(0,1,2), so it was blind to a bug in the spec->register
remap shim (disabling remap_expr_operands left the suite green). The shipped
code is correct; add selection_non_identity_register_mapping (scrambled homes
Reg(4,2,7) -> Ccnot{4,2,7}), teeth-proven: fails under remap-disable
(over-rejects Deferred) and under a neutered equiv gate (wrong body). L20.
- E-1 (MINOR): document selection_by_equiv's admit-first contract — a
recognized symbolic prim's table (if any) is always spec-consistent because
core::admit rejects SpecTableMismatch, so eval's table-wins-else-spec path
cannot diverge from the emitted body.
No recognizer logic change (test + doc only). symbolic_prim 24/24, clippy clean.
…(L21) Fresh-context Fable adversarial impl-review of selection-by-equiv symbolic-prim recognition. Verdict SHIP-WITH-FIXES: mechanism sound with proven teeth (5 tests flip under a neutered equiv gate), TCB untouched, I1 preserved, Flat(8)^3 payoff real at full width with no enumeration. A-1 (MAJOR, remap teeth) + E-1 (MINOR, admit-first doc) addressed in b805c74. Advisor disposition appended.
… + tiering-next status.md/roadmap.md: slice-3b symbolic-prim recognition via selection-by-equiv MERGED (Flat(8)^3 masked-accum -> [Ccnot], 2^24 table never built; Fable SHIP-WITH-FIXES, A-1/E-1 applied). BVEQ ladder (1/2b/2/3a/3b) complete. Energy OOM fixed via MALLOC_ARENA_MAX=1 (flake). Full tisc suite exceeds the 3000s gate window -> gate tiering is next, then TP-5 S-box (cashes in BVEQ; over widen-PC).
…S) + POC (L21) First nonlinear crypto layer target = Keccak-chi, bit-sliced over Flat(8) (one byte-parallel Ccnot per lane = the BVEQ-delivered masked-AND; 8x bit-slicing, 5.25e-9 J/row-chi). Fable design-review BUILT a working POC (7/7 green, exact 17-instr in-place schedule, whole-per-row + discriminating + Keccak golden + injectivity + energy) and caught a real design error: the forward-only chi is NOT garbage-free (24/32 dirty ancillas) -> ship Rev-A (garbage-free-under-adjoint) with the dirty-ancilla L20 regression assertion. NO recognizer/lower change (chi is Rust-composed, never lowers). POC scaffold docs/scratch/chi_poc.rs.ref.
…linear crypto layer, bit-sliced over Flat(8) — the first useful program on the BVEQ-delivered byte-parallel masked-AND (Ccnot). PRODUCTIONIZE the reviewed POC: promote to tests/chi.rs, ship Rev-A (garbage-free-UNDER-ADJOINT, honest), add a real system-ring authority tier, tier fast/heavy. TEST-ONLY (no src change — χ is Rust-composed, never lowers). L19 real-run authority.
…liced over Flat(8) — the first useful program on the BVEQ-delivered byte-parallel masked-AND (Ccnot). PRODUCTIONIZE the reviewed POC: promote to tests/chi.rs, ship Rev-A (garbage-free-UNDER-ADJOINT, honest), add a real system-ring authority tier, tier fast/heavy. TEST-ONLY (no src change — χ is Rust-composed, never lowers). L19 real-run authority.
…to layer chi bit-sliced over Flat(8): one byte-parallel Ccnot (BVEQ-delivered masked-AND) per lane = the chi gate for 8 Keccak rows at once. 8x bit-slicing (5.25e-9 J/row). Rev-A garbage-free-under-adjoint (honest; forward-only leaves ancillas dirty = L20 assertion). Rust-composed, never lowers (no recognizer/lower change). Fast tier + heavy system-ring L19 authority (advisor-run single-threaded, 3/3 green). Next: gate tiering; then AES S-box / Rev-B / Keccak-f follow-ups.
…tion gate is fast The full integration suite exceeds ~50 min (measured: compile 723s, bveq_recognize 460s, valwidth_add 301s, valwidth 296s, branching 274s, + energy/decoder/ring family/composite/mde_spill/whole-domain mem+iter). It cannot finish in a maestro delegation gate window and was the real cause of slow delegations (independent of the energy OOM). Gate 23 heavy integration-test binaries behind #![cfg(feature = "heavy-tests")] (off by default): a plain 'cargo test -p theseus-tisc' now compiles them empty and the fast tier runs in seconds. Advisor runs the heavy tier '--features heavy-tests -- --test-threads=1' pre-merge (single-threaded is mandatory: concurrent heavy tests stack GB-scale resident structures past RAM even with MALLOC_ARENA_MAX=1). Convention documented in CONTRIBUTING.md. Fast tier verified green; full tier compiles clean. Categorized by MEASURED per-binary runtime (markers were a poor proxy — they missed compile/bveq_recognize/valwidth/branching, all >4 min).
…e question for design-review Continues the crypto arc past Keccak-χ: a full byte-substitution S-box, same bit-sliced-over-Flat(8) / Rust-composed / run_on_cpu==eval pattern. The crux is register pressure — a bit-sliced AES S-box (Boyar-Peralta ~115 gates) has many live temps vs 8 regs + 8 scratch; a 4-bit PRESENT S-box is far smaller. Fable design-review-with-POC will do the live-range analysis, pick the target, and POC it.
AES-8 infeasible on the current machine: reviewer reconstructed the 115-gate Boyar-Peralta circuit (validated vs independent GF-inversion table 256/256), peak-live 30 signals > 18 addressable slots (8 regs + 6 usable scratch + 4 mem). PRESENT-4 fits in 6 registers, zero paging, STANDALONE garbage-free (inputs preserved). POC 8/8 green: whole-domain==table, bijection, system-ring L19 authority, 8x bit-slicing 2.82e-7 J, 47 instrs. Zero src change. Slice-1 = PRESENT-4; AES-8 = follow-up needing a recomputation-bounded schedule / wider machine. POC scaffold docs/scratch/sbox_present_poc.rs.ref.
…t S-box, bit-sliced over Flat(8) — a full byte-substitution crypto S-box (the second nonlinear crypto program, after Keccak-χ). PRODUCTIONIZE the reviewed 8/8-green POC: promote to tests/sbox.rs, honest STANDALONE-garbage-free framing, tier fast/heavy. TEST-ONLY (no src change — Rust-composed, never lowers). L19 real-run authority.
…lat(8) — a full byte-substitution crypto S-box (the second nonlinear crypto program, after Keccak-χ). PRODUCTIONIZE the reviewed 8/8-green POC: promote to tests/sbox.rs, honest STANDALONE-garbage-free framing, tier fast/heavy. TEST-ONLY (no src change — Rust-composed, never lowers). L19 real-run authority.
…-substitution S-box Bit-sliced ANF of the PRESENT 4->4 S-box over Flat(8), 47-instr Rust-composed ROM (31 Ccnot). STANDALONE garbage-free (inputs preserved -> temps uncomputed; stronger than chi). 8x bit-slicing 3.52e-8 J/S-box. Verified vs published table + system-ring L19 authority (advisor single-threaded 3/3 green). AES-8 proven infeasible on the 18-slot machine (peak-live 30). Follow-ups: AES-8 recomputation-bounded schedule, factored PRESENT, Rev-B chi, Keccak-f.
…before widen-PC Grounding (Explore map): PC=u8 (256 cap, explicit reject at compile.rs:2688/3209), Trace k_max=|measure|+1, delta_u mod 256, MAX_LEAVES_LOOP=4. Reframing: the FIRST genuine variable-T loop may not need the expensive widen-PC (permanent decoder- netlist energy tax) — a small-domain subtractive GCD (4-bit: WCET~252<256) fits today, showing real variable T<B park tax with zero tax; widen-PC is the follow-on to scale to 8-bit. Fable design-review-with-POC will try to compile+run small GCD on real system_step and resolve the slicing.
…x + gcd2) + POC (L21) Design-review refuted the 'small GCD fits today' hypothesis with a 7/7 POC: four walls (no trace syntax; Bennett 2-to-1 body needs self-delimiting history; k_max=|u|+1 is carrier-cardinality not a measure = the binding wall; recognizer- only body). widen-PC is NOT the first wall (alone it just fits a 99.97%-park program). BUT the bijective GCD exists at eval level (admit Ok, eval==gcd over 64 pairs, T varies 0..7). REVISED slice-1 = exact-k_max in lower_trace (trajectory- derived WCET, |u|+1 fallback) + pinned gcd2 recognizer + 2-bit GCD demo = the first variable-T algorithm, zero energy tax. HIGHEST BAR (lower_trace). widen-PC = follow-on (w=4 needs it; ~+10-15% step_j/bit). POC docs/scratch/tloop_poc.rs.ref.
…ce the loose Trace WCET bound k_max=|u|+1 (full carrier cardinality) with a trajectory-derived exact bound (walk the lowered body from every real input, k_exact = max applications-to-exit + safety, FALLBACK to |u|+1). SOUNDNESS-CRITICAL control-flow/lowering change (a too-small k_exact = park-wrap = silent corruption) → HIGHEST BAR: full L15/L19/L20/L21, adversarial impl-review + behavioral round-trip.
…low-authority green (L21)
Comment-only. (A) The walk's marshal-layout == body-home-layout equality — the
entire reason the exec_instr walk simulates the same registers as the real CPU —
holds ONLY because the F-1 canonical-homes guard runs first; a future F-1
relaxation would silently make k_exact unsound. (C) The walk tests the whole tag
byte while hardware routes on bit 0; safe because lowered bodies keep the tag
canonical (∈{0,1}) at iteration boundaries.
…riable-T enabler Trace WCET now trajectory-derived (k_max=min(k_exact,|u|+1)) not |u|+1; large- carrier fast-exit Traces fit under the 8-bit PC, zero energy tax. Fable review SHIP + real-system_step H1 authority 2/2. Next: slice-1b gcd2 + 2-bit GCD.
compile.rs: introduce REG_PLUS_SCRATCH (14 = 8 regs + 6 usable scratch), SCRATCH_OFFSET (6), and SWAP_TEMP_REG (r0) so home_of's leaf routing, the resident head-leaf bound, MAX_LEAVES, and the swap_homes temp register are derived from named constants instead of bare 14 / leaf-6 / 0u8. types.rs: decode/decode_composite now read IR via IR_B0_FIELD and scratch via scratch_field(i) instead of baking 10*W and (14+i)*W, reusing the symbolic field accessors that sit next to BR_FIELD. Behavior identical.
Grep-confirmed zero callers across the workspace (only self-references in the definitions). pc_byte_field had no reduced-w_pc callers by design; IR_LO_FIELD/IR_HI_FIELD were legacy 16-bit-IR aliases superseded by IR_B0_FIELD/IR_B1_FIELD.
Add a 'measurement' cargo feature and gate the internal energy-regression measurement entry points behind it so they no longer ship on the default public API: - synth.rs: RELAXED_OPERAND_CAP + RelaxedOperandCap guard + transcribe_word_bennett_peak_measure (emits non-runnable programs). check_operand_legal now reads the cap via current_operand_cap(), which is the strict NUM_OPERAND_LOCS off the feature -- byte-identical production path. Named the bare 200 cap MEASURE_OPERAND_CAP. - decoder.rs: the six *_for_measurement hooks, plus their now-exclusively- measurement helpers reg_imm_shared / reg_imm_alu / group_a_alu_view. Stripped raw cell-count magic numbers (185864/75520/63770) from the shared_alu_block_for_measurement doc. - bveq.rs: expr_to_bdd_shifted (a copy of expr_to_bdd with one test caller). The corresponding tests are gated too: individual #[cfg(feature = "measurement")] on the poc_b1*_measure / b13_cswap_scratch_operand_equiv / bveq_major4_mismap_canary_has_teeth / gcd2_word_body_length_measurement functions (their files mix non-measurement tests, so per-test gating is correct rather than a file-level attr). Verified: default cargo test -p theseus-tisc green (measurement skipped); --features measurement compiles + green; --features heavy-tests,measurement runs and passes all six gated measurement tests.
- types.rs: CpuState field-count comments now say 23 (the actual num_cpu_fields() at the default layout) instead of 22/24, phrased off num_cpu_fields(); br_fields() doc corrected from ceil to floor (w_br is always a whole multiple of w_ctl); cpu_field_widths default corrected to [8; 23]; state_ty_with field-order header corrected to 23 fields. - bveq.rs: admit_symbolic doc no longer lists num_operands/width params the signature dropped -- both are read from spec.forward. - decoder.rs: group_a_alu_view doc now names shared_alu_block as the wired ALU path (was reg_imm_alu, which is measurement-only). - theseus-netlist balance.rs: is_tick_exact doc no longer promises an assert it never performs (the body just returns true by construction).
docs/paper/outline.md: thesis/contributions, draft abstract + conclusion, a section-by-section outline, and reviewer-defense notes. docs/paper/references.bib: ~35 recalled citations across thermodynamics, adiabatic circuits, reversible architectures/languages, reversible synthesis, verified compilation, and BDDs. Every citation marked VERIFY -- details recalled from memory, unchecked.
The differential oracle invented ancilla inits (i%2) instead of using the values the lowering allocated. R1's garbage-free construction (ADR-0040) only computes correctly when each ancilla starts at its allocated value, so the guessed pattern corrupted the reductions and produced a wrong output bit. Use lower_iso_with_ancillas' real values (as fib_reversible already does); oracle now passes 32/32. Also update the energy-breakdown assertion k3->r1 (the full adder now lowers conditional NOTs to R1, not a K3 swap).
Remove ~180 private review-workflow tag codes (MAJOR-<n>, BLOCKER-<n>, MINOR-<n>, A-5b, W_BR-a/b/c, review-round R<n>/N<n>, finding F<n>.<n>) from comments (and a few CompileError diagnostic strings) across compile.rs, synth.rs, decoder.rs, bveq.rs. Each edit keeps the WHY/invariant sentence and rephrases back-references (e.g. 'the MAJOR-1 analogue') into plain language. Architectural references are preserved: ADR-00xx, operating lessons L19-L21, milestone/phase names (M-D.x, B-2.x, B1.x, A-0/A-6.4/TP-x), register names, config-line/field identifiers, and code constants (W_BR16 etc.). Comment/diagnostic-text only; both default and --features measurement builds compile, and the default test suite stays green.
…hen reversibility algebra; fix mathlib drift
Lean meta-theory expansion. All lake-checked; axioms reduce to the Mathlib
base {propext, Classical.choice, Quot.sound} only (verified via #print axioms),
no sorry / admit / native_decide.
FiniteTrace (TH-1):
- mutual inverse / backward run: trace_mutual_inverse (fuel-free) + run_symm_entry
(fueled |u|+1), built on a fuel-free Steps relation inter-derivable with run
(run_some_of_steps / steps_of_run_some), steps_reaches, steps_output_unique.
The backward run is the forward run of the adjoint -- one reversed trajectory.
- class-wide exactness / trajectory disjointness (TH-1b): traj_cross_injective,
traj_disjoint, traj_card_bound (the Sigma_inputs (T_i - 1) <= |u| carrier bound).
Reversibility:
- extend the iso algebra to the full reversible-rig fragment (product/sum
associators, left unitor, product-over-sum distributor, NOT = SwapSum(1,1)),
each with bijectivity DERIVED in denote_bijective (raw-function denotation,
not baked into the type) plus rfl-level behavioral pins.
- new NL companion docs/src/theory/reversibility.md: a classical proof per
theorem, an honest modeling-scope section, and borrowed-vs-novel provenance.
- obligation-ledger rows TH-REV-1..5; TH-1 row updated to record the new
mechanized parts.
Also fixes pre-existing mathlib API drift in Reversibility.lean that the base
commit's stale-olean build had masked: the Inhabited-sum instance, the
symm_apply_apply / apply_symm_apply inverse lemmas, and seq_inv / inv_inv
via LeftInverse.eq_rightInverse.
…claims
The Fable adversarial review found the Lean sound (clean axiom base, no vacuous
theorems) but flagged two places where docs/ledger claimed more than the Lean
proved. Both are now mechanized, not merely re-scoped.
Blocking 1 -- genuine ADR-0037 accumulator fold (was: List.map, a degenerate
per-cell map that inverts in either order):
- foldAcc / unfoldAcc over List Bool: a reversible mapAccumL threading an
accumulator head-to-tail, adjoint runs f.symm tail-to-head (cells coupled).
- unfold_fold_acc, fold_unfold_acc (mutual inverse at every length),
foldAcc_bijective. foldBits kept, relabelled as the accumulator-free case.
Blocking 2 -- genuine per-input Sigma carrier bound (was: uniform |S|*fuel):
- traj_cross_injective generalized to per-input fuels (fx, fx').
- traj_card_bound now proves Sigma_{x in S} fuel x <= |U| over a dependent-sigma
index set -- the real Sigma_inputs (T_i - 1) <= |u| bound, not a uniform product.
Advisory/nit fixes (docs): honest fold Modeling-scope (per-cell claim was false);
SWAPBR in-flight-invariance caveat added (Lean comment + reversibility.md +
ledger); general-|u| tightness listed as text-only; TH-REV-2 marked
denotational; notI_involution given an NL section; iter data-carried (ADR-0036)
note. All lake-checked; #print axioms on all key theorems reduces to the Mathlib
base {propext, Classical.choice, Quot.sound}, no sorry / native_decide.
The stale-.olean episode showed that "lake build is green" did not imply "the
proofs are sound": `lake build` only WARNS on `sorry`, and `#print axioms` is a
manual command. Make the soundness invariant enforced by the build itself.
- TheseusProofs/AxiomGuard.lean: a metaprogram (`collectAxioms`) that fails
elaboration -- hence `lake build`, hence CI -- if any of the 32 key theorems
depends on an axiom outside {propext, Classical.choice, Quot.sound}. A `sorry`
(sorryAx) or `native_decide` (Lean.ofReduceBool) turns the build red. Verified
by a negative test (dropping Classical.choice from the whitelist fails the
build with a precise message). Imported by the TheseusProofs root so it runs on
every default build.
- Because the guard imports the proof modules, Lake re-elaborates it whenever a
proof changes -- it cannot go stale relative to the proofs.
- CI note: the proofs job builds from a fresh checkout (no cached project
.lake/build), so modules always recompile from source and the guard runs.
- obligation-ledger.md: record the remaining verification future-work
(model-to-Rust correspondence; generalize modeled fragments; independent
proof-specialist review) as deferred; the axiom check is now enforced.
- Machine-checked proofs subsection: separate lake build command, the no-sorry/no-native_decide policy enforced by AxiomGuard, and the Lean+NL-companion+obligation-ledger definition-of-done for a proof. - Reword the heavy-tests gate out of internal orchestration terms (per-attempt maestro gate / delegation spec / the chi task) into plain contributor language (while iterating / before merging); drop the stale ~50 min figure.
theseus-verify was scaffolded in the initial v2 commit as the intended home for SAT/CNF-based lowering verification (miter -> Tseitin -> CnfSolver, the `--verify-lowering` path, ADR-0012/0020). It was never implemented: one commit of history, four empty module stubs, nothing depends on it, and no `--verify-lowering` / CnfSolver / Tseitin is wired anywhere. The need it was meant to serve -- proving a lowered netlist equivalent to its spec -- is instead met by the BVEQ program (whole-domain symbolic BDD equivalence, `bveq_netlist::eval_bdd`) and the Lean meta-theory, so the SAT-miter approach was superseded before it was built. Remove the dead skeleton, drop it from the workspace members, and delete CONTRIBUTING's stale `--verify-lowering` nightly line. (ADR-0012/0020 remain cited elsewhere, so the citation lint is unaffected.)
`bveq_invariant_poc.rs` failed to compile under `--features heavy-tests` (E0027):
two `Instr::Swapbr { rd }` patterns predated the W_BR-b change that added the `rs`
(source register) field, so the binary never compiled after that change. Because
heavy tests are off by default, a plain `cargo test` never built it and the rot
sat unnoticed. Complete both patterns with `rs: _` (the tests only read `rd`).
The heavy suite now compiles all 41 binaries.
Publication-readiness review found docs describing features that don't exist. Corrected prose to match the code (status.md was already honest): - lowering lives in theseus-netlist, not the empty theseus-emit crate; Verilog emission marked future work (v0.2+) - removed deleted theseus-verify + empty theseus-emit from crate-map; BVEQ (theseus-tisc) is the actual verification path - --emit=energy / --verify-lowering / machine-checked invariant ledger marked planned (no such CLI flags/registry exist) - bijection-table 'flagship generator' marked planned; documented the real generators (exhaustive enumerator, oracle-chain differential) - obligation-ledger: TH-4a-label is proved (text), not Lean-mechanized; TH-1 label discharge reframed as Lean-TH-1 + text-TH-4a-label - documented the shipped 'theseus lower' verb; dropped stale 'no lower verb' gap; enumerated all 46 ADRs in the index - paper outline: 'variable-time loops' -> 'bounded/synthetic loops' (GCD does not lower today, per status.md) - fixed stale date, broken [[maestro-fast-tests-tenet]] links, and the Structurizr diagram (still listed the removed crates)
…seus-emit Review found production paths that crash on malformed input, plus empty scaffolding crates/modules: - value_to_leaf_bytes (theseus-core) and parse_surface_value (theseus-cli) now return Result; the CLI/REPL report a diagnostic instead of panicking - spice_value / parse_caps (theseus-spice) return Result and propagate - deleted the empty theseus-emit crate (nothing depended on it), mirroring the earlier theseus-verify removal; dropped from workspace members - removed empty pub-mod stubs: theseus-netlist sim_bits, theseus-spice deck cargo check --workspace --tests clean; fast tests on all changed crates pass (theseus-core/cli/spice/eval).
All 42 VERIFY-flagged entries checked against DOI/arXiv/DBLP/publisher sources. Substantive fixes: corrected author lists (axelsen2011arch, axelsen2011rfun, athas1994, benes2020aeon +Kadlecaj), replaced the 2LAL placeholder with the canonical ESA'04 paper, retyped frank2017spectrum and lutz1986janus, resolved venues/DOIs across the set. 4 fields left marked UNVERIFIED (pre-digital page ranges; ngspice version to be pinned by the author).
Replace the >4min concrete-eval brute-force branching test with a whole-domain symbolic BVEQ proof (branching_bveq.rs, ~37s), following the GO-rollout convention (symbolic primary + concrete reality-anchor + negative control): - SWAPBR branch step proven over the whole symbolic (regs,BR) domain at concrete PC: rd'=old BR, BR'=old rd, PC'=pc+sext(BR)+1, IR=0, scratch restored, untouched regs = identity; spec built from the ISA definition (independent of the walked netlist) since instr_semantics rejects SWAPBR - reality anchor: same step iso via concrete eval on branching's scenarios - negative controls: wrong specs (drop +1, wrong direction) must differ - reversibility (forward+adjoint = start) kept as a concrete check branching.rs becomes a retirement stub (0 compiled tests) documenting where each obligation moved.
Skeleton phase is over (zero todo!() macros remain in src); enforce it so no placeholder stub can ship.
cleanCargoSource stripped everything but Rust/Cargo files, so the sandboxed nix-flake-check build could not see assets pulled in at compile time via include_str! (theseus-check's stdlib/prelude.thse, theseus-spice's rung0-chardb.ron) or the conformance corpus the test binaries embed (*.thse/*.expect/*.diag). Widen the filter to keep those extensions. This is why CI's build/test/clippy checks failed where a local cargo build (seeing the whole tree) succeeded.
…s debt The repo was never cargo-fmt'd against the flake's rustfmt and carried a workspace clippy debt; CI's fmt check failed first and masked both, so the nix flake check had never actually passed. Run cargo fmt --all and clear every clippy lint under --all-targets --deny warnings: - fmt: ~110 files reformatted (no semantic change) - clippy: auto-fixed the mechanical lints (useless vec!, redundant pattern matching / closure, ref-deref, manual is_multiple_of, or-as-range); reflowed doc-comment lists (doc_lazy_continuation); rewrote trivially-safe needless_range_loop to iterators in tests; added targeted #[allow(needless_range_loop)] with justification in synth.rs/compile.rs where the index is load-bearing arithmetic; #[allow(too_many_arguments)] on test fixtures; removed a dead test helper; collapsed a match in theseus-check coverage.rs Verified: nix flake check green (fmt + clippy + nextest 935 passed / 37 skipped); branching_bveq heavy test 5/5.
…eVals/bveq helpers to lib DRY consolidation of the theseus-tisc test harness (behavior-preserving, ~1615 LOC of copy-paste removed from 42 files): - new crates/theseus-tisc/tests/common/ (mod.rs + bveq_support.rs + bdd_helpers.rs + prim_builders.rs, #![allow(dead_code)] per the tests/common idiom): ref_instr/ref_step ISA oracle, r_ins/i_ins encoders (unvalidated behavior kept), eval_state (fuel now a param), the BVEQ symbolic-state helpers (field_bit_var/n_vars/const_word8/symbolic_word8/ out_field_bits/sv_bdd_sizes/...), ripple adders, xor_prim builders - L1: StateVals::zero_state()/state_with_regs() promoted into src/types.rs (were 9/11 verbatim test copies) - L2: zero_out()/transfer_zero_out() promoted into src/bveq.rs (4 copies) Guardrails honored: build_state_fields shares only the type-walk skeleton (concretization strategies stay local); xor_prim excludes xor_reduce.rs / general_lowering.rs (different semantics). Verified: theseus-tisc 325 passed / 0 failed / 36 ignored; clippy --all-targets 0 warnings; fmt clean; heavy tier compiles.
DRY: the three Bennett transcribers + emit_weqzero/wlt shared copy-pasted validation/construction blocks. Extract private helpers (validate_bennett_operands, validate_bennett_carrier_reads, validate_bennett_identity_rows, build_bennett_operand_maps, emit_bennett_swaps, generic validate_operands_distinct with a per-site error-message closure). Behavior-preserving: identical emitted output and error detail strings. Guardrail: the BDD variant's temp+node-unified disjointness and the message-differing inline blocks were deliberately kept per-site to avoid reordering first-error semantics. Verified: theseus-tisc 325 passed / 0 failed; clippy 0; fmt clean.
…elpers DRY: load_source() (fs read + exit) and elaborate_or_exit() into theseus-cli (cmd_check kept separate); finalize_deck() (SPICE footer) and require_meas() into theseus-spice. Behavior-preserving (exact messages, exit codes, deck bytes). Verified: build clean, clippy 0, fmt clean, theseus-cli tests pass.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.