Improve/agc arithmetic model#974
Open
alin9661 wants to merge 39 commits intochrislgarry:masterfrom
Open
Conversation
Comprehensive plan for building verification infrastructure across 4 phases: - Phase 1: yaYUL assembly CI pipeline with binary verification - Phase 2: Rust-based interpreter arithmetic test harness - Phase 3: Integration testing via yaAGC simulator - Phase 4: Restart/recovery fuzzing Covers exact AGC Hastings polynomial coefficients, 1's complement word model design, proptest property-based testing strategy, and dependency graph. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Build infrastructure for assembling AGC source and verifying binaries: - tools/build.sh: Assemble a program directory (Comanche055 or Luminary099) with yaYUL, producing .bin rope image and .lst listing - tools/verify-binary.sh: Compare assembled binary against known-good reference binsource via byte-for-byte comparison - tools/Dockerfile: Multi-stage Docker image with yaYUL, yaAGC, and Rust toolchain for reproducible builds Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Standalone Rust tool to convert Virtual AGC binsource files (octal text dumps of core rope memory) into raw binary for comparison against yaYUL output. Parses the binsource format: BANK= headers, 8 octal words per data line, comment lines (;), and outputs 36 banks × 1024 words as big-endian 16-bit. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Two parallel CI jobs on every push and pull request: 1. assemble: Build yaYUL from virtualagc source, assemble both Comanche055 and Luminary099 via matrix strategy, upload .bin and .lst as artifacts 2. test-arithmetic: Run the Rust agc-math test suite (58 tests covering 1's complement types, DP arithmetic, and trig functions) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Documents the source of known-good reference binaries from the Virtual AGC project, explains the binsource format (bank headers, octal words, bugger checksums), and describes the verification process. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Exclude Rust build artifacts from the new test workspace. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Set up Cargo workspace at tests/ with the agc-math crate. This workspace will host the interpreter arithmetic model, integration tests, and fuzzer as separate crates sharing common AGC types. Uses proptest for property-based testing of 1's complement arithmetic. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Core types modeling the AGC Block II's 15-bit 1's complement arithmetic: - AgcWord: 15-bit word with distinct +0/−0, CCS semantics, magnitude ops - DpWord: double-precision (28-bit) with sign-agreement invariant - TpWord: triple-precision as used by the MPAC accumulator - Accumulator: 16-bit register with overflow detection (bits 14-15 disagree) - DAS: double add to storage with end-around carry The AGC uses 1's complement (not 2's complement), meaning negation is bitwise NOT and zero has two representations. These newtypes enforce correct width and semantics at the Rust type level. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Transcribe exact constant values from Comanche055/FIXED_FIXED_CONSTANT_POOL.agc: BIT1-BIT14, POSMAX, NEGMAX, ZERO, ONE-SEVEN, QUARTER (pi/2 scaled), HALF (0.5), NEG_HALF (used by SINE routine), and LOW7 mask. All values match the octal literals in the original flight software. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Port the AGC interpreter's DP arithmetic operations from INTERPRETER.agc: - DAD (line 807): double-precision add via DAS - DSU (line 819): double-precision subtract via complement-and-add - BDSU (line 871): reverse subtract - DMP (line 904): double-precision multiply using DMPSUB algorithm - DMPR (line 1363): multiply with rounding - DSQ (line 2346): double-precision square (DMP with self) DMP uses 28-bit fixed-point multiplication with proper fractional scaling: both operands are scaled by 2^-14, so the product requires a 2^-28 shift to maintain the correct binary point position. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Horner's method polynomial evaluator mirroring the AGC's POLY instruction. Takes coefficients in [C0, C1, ..., CN] order and evaluates using AGC double-precision multiply and add operations. Used by the SINE, COSINE, and ARCCOS routines for their Hastings polynomial approximations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
SINE, COSINE, ARCSIN, and ARCCOS using the exact polynomial coefficients from Comanche055/INTERPRETER.agc: - Sine (lines 2682-2688): 4th-order Hastings polynomial Coefficients: +.3926990796, -.6459637111, +.318758717, -.074780249, +.009694988 Convention: SIN(x) returns (1/2)sin(2*pi*x), argument in revolutions - Cosine (line 2641): COS(x) = SIN(QUARTER - |x|) - Arccos (lines 2758-2767): 7th-order Hastings polynomial with sqrt(1-x) term Input is half-scaled: agc_arccos(x) computes arccos(2x)/(2*pi) This convention avoids overflow in the (-1,1) fractional range - Arcsin (line 2779): ARCSIN(x) = QUARTER - ARCCOS(x) Verified against IEEE f64 reference to <1e-4 accuracy across full domain. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Property-based tests using proptest for AgcWord and DAS: - Negation is involution: negate(negate(x)) = x - Negation flips sign bit for non-zero values - Magnitude preserved through negation - to_i16/from_i16 roundtrip - CCS branch index always 0-3, diminished absolute value non-negative - Absolute value is always positive - DAS additive identity: x + 0 = x - Explicit tests for +0 and -0 CCS branch behavior Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Property-based and known-value tests for DAD, DSU, DMP, DSQ: - DAD commutativity: a + b = b + a - DAD identity: a + 0 = a - DSU self-subtraction: a - a ≈ 0 - DMP commutativity: a * b ≈ b * a (within 1 LSB) - DMP by zero: a * 0 = 0 - DSQ equivalence: DSQ(a) = DMP(a, a) - DSQ non-negative: a^2 >= 0 - DAD/DSU roundtrip: (a + b) - b ≈ a - Known-value tests: 0.5*0.5=0.25, sign correctness Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Property-based tests verifying the Hastings polynomial implementations: - Pythagorean identity: sin²(x) + cos²(x) = 1 - Sine odd symmetry: sin(-x) = -sin(x) - Cosine even symmetry: cos(-x) = cos(x) - Arcsin/arccos complementary: arcsin(x) + arccos(x) = pi/2 - Sine/arcsin roundtrip: sin(arcsin(x)) ≈ x - Sine matches IEEE f64 reference within 1e-4 - Arccos matches IEEE f64 reference within 1e-3 All tests sweep continuous domains via proptest, not just fixed points. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Port of SQRTSUB from INTERPRETER.agc lines 2497-2629. Uses piecewise linear approximation (SLOPEHI/BIASHI for [0.25,0.5), SLOPELO/BIASLO for [0.125,0.25)) followed by two Newton-Raphson iterations for full 28-bit precision. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Port of DDV/BDDV from INTERPRETER.agc lines 1792-1987. Handles sign tracking (DVSIGN), divisor normalization, and overflow clamping to ±POSMAX. BDDV reverses operand order (computes b/a instead of a/b). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Full vector math suite built on the DP arithmetic primitives: - DOT (DOTSUB, line 967): dot product via three DMP+DAD pairs - VXV (line 1265): cross product, anti-commutative (a×b = -(b×a)) - VAD/VSU: component-wise vector add/subtract - VXSC: vector times scalar - ABVAL (line 2353): vector magnitude via sqrt(dot(v,v)) - UNIT (line 2203): unit vector, returns half-unit (v/(2|v|)) when |v| >= 0.25 to avoid fractional overflow at 1.0 - MXV/VXM: matrix-vector and vector-matrix multiply Includes AgcVector and AgcMatrix types for 3-component/3x3 operations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
SQRT properties: - sqrt(x^2) ≈ |x|, sqrt non-negative, matches f64 reference Vector operation properties: - DOT commutativity: a.b = b.a - VXV anti-commutativity: a×b = -(b×a) - VXV orthogonality: (a×b).a = 0 and (a×b).b = 0 - Self cross product is zero: a×a = 0 - VAD/VSU roundtrip: (a+b)-b ≈ a - ABVAL non-negative - Known-value tests: 3-4-5 triangle, basis vector cross products Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add yaYUL assembly CI pipeline and build tools
Add Rust model of AGC 15-bit 1's complement arithmetic
Relay word parser for channel 010 output: - parse_relay_word(): extract relay number, sign bit, left/right digit codes - relay_code_to_digit(): 5-bit AGC code → decimal digit (0o25=0, 0o03=1, etc.) - relay_code_to_segments(): 5-bit code → 7-segment activation bitmap (a-g) - DskyLights: channel 011/013 indicator light state (14 lights total) - DskyState: full display state (21 segment digits, 6 signs, all lights) The 5-bit relay codes are NOT sequential — they're segment bitmaps in AGC bit ordering, remapped to standard a(0)-g(6) for rendering. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Standalone Rust binary (dsky-bridge) that:
- Connects to yaAGC via TCP (4-byte channel protocol, default port 19697)
- Exposes WebSocket server (default port 8765) for browser clients
- Translates AGC channel packets to JSON: {"type":"channel","channel":N,"value":V}
- Translates browser key events to AGC keyboard input (channel 015)
- Handles key press/release timing (30ms debounce)
- Auto-recovers from disconnected browsers
- ~60fps polling loop for display updates
Usage: cargo run -- --agc-host localhost:19697 --ws-port 8765
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Single-file browser DSKY emulator (tools/dsky-web/public/index.html): Display: - SVG seven-segment digit rendering for all 21 display positions (PROG 2, VERB 2, NOUN 2, R1/R2/R3 5 each) - 14 indicator lights (COMP ACTY, UPLINK ACTY, PROG ALARM, GIMBAL LOCK, TRACKER, ALT, VEL, NO ATT, STBY, KEY REL, OPR ERR, RESTART, TEMP, PROG) - Sign indicators (+/-) for R1, R2, R3 Input: - Clickable DSKY keyboard (VERB, NOUN, 0-9, +, -, CLR, ENTR, RSET, KEY REL, PRO) - Keyboard shortcuts (v=VERB, n=NOUN, 0-9, Enter, Backspace=CLR, r=RSET) Connection: - WebSocket to dsky-bridge at ws://localhost:8765 - Auto-reconnect on disconnect - Processes channel 010 relay words, channel 011/013 discrete lights Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Documents the three-component architecture: Browser (SVG) ←WebSocket→ dsky-bridge (Rust) ←TCP→ yaAGC Includes quick start guide, keyboard shortcut table, display element inventory, and JSON protocol specification. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add DSKY web emulator with SVG seven-segment display
New agc-integration crate providing: - channel_protocol: yaAGC 4-byte packet encode/decode with byte-position markers for resynchronization (channels 010-032 octal) - dsky_client: high-level DSKY interface — press_key(), verb_noun(), wait_for_display() over TCP socket to yaAGC - agc_runner: yaAGC subprocess lifecycle management with auto-cleanup - dsky_display: display state tracker for relay words and alarm lights Integration test scenarios (all #[ignore], require yaAGC + .bin): - fresh_start: verify both Comanche055 and Luminary099 boot to P00 - verb_noun_basic: V35E lamp test, V05N09E alarm display, V99E OPR ERR Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Model of the AGC's 2048-word erasable memory: - Unswitched: 256 registers at 0000-0377 (always accessible) - Switched: 8 banks × 256 registers (selected by EBANK) - Named address constants from ERASABLE_ASSIGNMENTS.agc: MPAC (0100), PRIORITY (0113), FAILREG (0317), PHASE1-6 (0340-0352), PHSPRDT1-6 (0363-0375), REDOCTR (0376), LST1/LST2 (EBANK 3) - Correct address decoding (unswitched vs switched) - Snapshot support for state comparison Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
New agc-fuzzer crate with named AGC erasable addresses for fuzzing: - PHASE_ADDRS, NEG_PHASE_ADDRS, PHSPRDT_ADDRS arrays for iteration - core_set_priority_addr() for executive core set addressing - EXECUTIVE_START/END range, FAILREG_SIZE, LST1/LST2 sizes - All constants reference ERASABLE_ASSIGNMENTS.agc source Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Targeted corruption generators for each AGC subsystem: - CorruptionTarget enum: PhaseTable, PhasePriority, FailReg, Executive, Waitlist, RandomUnswitched - CorruptionSet::phase_table() — 12 phase registers with random values - CorruptionSet::executive() — PRIORITY registers for 7 core sets - CorruptionSet::waitlist_timing() — LST1 delta-T corruption - CorruptionSet::random_single() — arbitrary unswitched address - All values masked to 15 bits (AGC word width) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
RestartExpectation for each corruption target based on FRESH_START_AND_RESTART.agc logic: - Phase table → alarm 1107, DOFSTART reinitializes - FAILREG → overwritten with restart alarm code - Executive → core sets reinitialized via STARTSUB - Waitlist → LST1/LST2 reset to ENDTASK/NEG1/2 - Random → AGC must not hang, REDOCTR must increment - Clean restart baseline for infrastructure validation Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Orchestrates the full fuzz cycle: start yaAGC → boot → corrupt → GOJAM → validate. - FuzzConfig: yaAGC path, .bin path, port, timeouts - FuzzResult: Recovered (with timing), Timeout, or Error - run_fuzz_scenario(): drives the corruption/restart/validation loop - validate_result(): checks result against oracle expectations Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Integration fuzz tests (all #[ignore], require yaAGC + assembled .bin): - restart_basic: clean GOJAM baseline (no corruption) - phase_table_fuzz: corrupt PHASE1-6 with zeros, POSMAX, random patterns - general_erasable: corrupt MPAC, NEWJOB, STATE flagwords Each test uses the fuzz scenario runner with the restart oracle to validate recovery. Workspace updated to include agc-fuzzer crate. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Critical fixes from code review: 1. ErasableMemory EBANK 0 aliasing: unswitched erasable (0000-0377) and EBANK 0 are the same physical memory. Removed separate `unswitched` array — all reads/writes now go through `banks[0]`. 2. Phase table addresses swapped: in the AGC, -PHASEn is allocated at the even (lower) address, PHASEn at the odd (higher) address. Verified against Comanche055/ERASABLE_ASSIGNMENTS.agc lines 1759-1770. 3. Fixed NUM_CORE_SETS comment (7 for both modules, not "Comanche=6"). 4. Fixed EXECUTIVE_END comment (0o237, not 0o245). 5. Added tests: EBANK 0 aliasing, boundary addresses (0o377/0o400), #[should_panic] for out-of-range addr/ebank, snapshot_bank overflow. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Replace unwrap_or(false) with match blocks that propagate real I/O errors (connection reset, broken pipe) into FuzzResult::Error - Log runner.stop() failures with eprintln instead of silently discarding - Reject unexpected PROG ALARM in validate_result when no alarm expected Previously, a yaAGC crash would be misreported as "timeout" because the connection reset error was swallowed by unwrap_or(false). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…_noun agc_runner.rs: - Pipe stderr to Stdio::piped() instead of null (crash diagnostics preserved) - Detect immediate exit via try_wait() after 50ms (bad args, port conflict) - Add captured_stderr() method for failure diagnostics dsky_client.rs: - Change poll_display break to continue on WouldBlock/TimedOut — poll for the full requested duration instead of exiting on first 100ms gap - Validate verb/noun 0-99 range — reject >99 with InvalidInput error instead of silently dropping digit keypresses - Log packet decode failures with eprintln for sync error diagnosis lib.rs: - Fix channel descriptions: 010=relay output, 011=DSALMOUT, add 015=keyboard Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
channel_protocol.rs: - Per-byte marker failure tests (bytes 0-3 individually) - Golden-vector test: hand-computed bytes for channel 0o15/value 0o12345, verified both encode→bytes and bytes→decode directions dsky_display.rs: - decode_digit: blank (0), all valid codes 1-10, invalid codes 11-31, 5-bit masking behavior - update_channel_11: prog_alarm bit position (bit 1 = 0x02), adjacent bit rejection (0x01 should not trigger), all-bits-set, lights storage - relay word storage verification Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Improve/testing ci infrastructure
…sking) Remaining low-priority items from code review: - ChannelPacket::new: mask inputs to valid widths (9-bit channel, 15-bit value) instead of panicking — safer for fuzzer-generated values - DskyClient::connect: use connect_timeout(5s) instead of OS default (~75s); add write_timeout(5s) to prevent blocking on full send buffer - AgcRunner::stop: tolerate already-exited processes instead of returning a confusing "failed to kill" error - find_yaagc: check exit status and log when yaAGC is found but broken (missing shared library, corrupt binary) instead of silently treating all errors as "not found" Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
9e9e089 to
8b6da36
Compare
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
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.