LinxCoreModel

LinxCoreModel is the Rust modeling workspace for LinxCore.

Project policy and verification entrypoints:

• contributor guidance: CONTRIBUTING.md
• security process: SECURITY.md
• workspace layout: docs/project/layout.md
• crosscheck gates: docs/verification/crosscheck-gates.md
• latest gate report: docs/bringup/gates/latest.json

Current workspace contents:

• isa: shared architectural types and trace contracts
• elf: static ELF loading for LinxISA user-mode programs
• runtime: guest runtime state and syscall shim scaffolding
• funcmodel: first functional engine path
• camodel: first stage-structured cycle engine path
• trace: commit JSONL and linxtrace.v1 emission
• cosim: M1 JSONL lockstep protocol helpers
• dse: sweep and report generation
• lx-tools: lx-run, lx-cosim, lx-trace, lx-sweep

Current crate layout:

• camodel: core/, frontend/, issue/, backend/, control/, decode/, trace/
• funcmodel: core/, exec/, memory/, syscalls/, trace/
• trace: linxtrace/, commit/, schema/
• cosim: protocol/, compare/, qemu/
• lx-tools: shared helpers in cli/, thin binaries in bin/

The current implementation lands the full workspace shape, executable lx-* surface, static ELF loading, runtime bootstrap, syscall allowlist scaffolding, commit/pipeview emission, lockstep compare helpers, and a full table-driven LinxISA v0.4 decoder sourced from a vendored copy of the canonical ISA JSON.

Current functional-engine status:

• decodes the full canonical v0.4 instruction corpus, including 16/32/48/64-bit forms
• bootstraps a Linux-style user stack and places the initial stack pointer in sp
• executes a substantial user-mode scalar subset in Rust: ALU/immediate ops, W variants, compares, shifts, loads/stores, SETC, SETRET, J/JR, SSRGET/SSRSET, compressed scalar forms, and basic block/macro control flow
• forwards the current user-mode syscall subset through a host shim: read, write, eventfd2, epoll_create1, epoll_ctl, epoll_pwait, openat, close, lseek, fstat, futex, getcwd, dup3, fcntl, ioctl, pipe2, pselect6, ppoll, newfstatat, readlinkat, getrandom, prctl, madvise, membarrier, rseq, sigaltstack, set_tid_address, set_robust_list, setuid, setgid, setresuid, getresuid, setresgid, getresgid, uname, getppid, wait4, sysinfo, prlimit64, brk, mmap, munmap, mprotect, rt_sigaction, rt_sigprocmask, clock_gettime, getpid, getuid, geteuid, getgid, getegid, gettid, exit, exit_group
• enforces guest page permissions for architectural loads/stores and syscall copy-in/copy-out, including mprotect-driven access changes
• normalizes host errno values to Linux guest errno numbers before returning through the Linx Linux-user syscall ABI
• emits commit JSONL and linxtrace.v1 traces from the executing functional path

Still incomplete in this phase:

• many ISA classes remain unsupported in the functional executor, especially FP, atomics, wide HL forms, and full privileged behavior
• syscall ABI coverage is pragmatic bring-up coverage, not a complete Linux user ABI
• futex currently implements the single-process WAIT/WAKE subset only; there is no real waiter queue or multi-thread scheduler yet
• sysinfo and prlimit64 currently expose deterministic single-process model values suitable for libc bring-up, not host-kernel passthrough
• setxid coverage is currently single-process identity-state emulation for libc startup and credential probes, not full Linux credential or threading semantics
• getrandom currently returns deterministic model-generated bytes so user-mode bring-up and regression traces stay reproducible across hosts
• prctl, madvise, and membarrier currently implement the small single-process subset needed for libc/thread-runtime bring-up, not the full Linux kernel surface
• rseq currently supports deterministic single-thread register/unregister bring-up semantics and initializes the guest ABI fields the runtime is expected to read
• ioctl currently implements deterministic tty-style TIOCGWINSZ, TIOCGPGRP, and TIOCSPGRP behavior for guest stdio fds only
• ppoll currently marshals guest pollfd arrays onto host poll(2) and ignores signal-mask effects beyond guest-memory validation
• pselect6 currently marshals guest fd_set bitmaps onto host poll(2) and validates, but does not apply, guest signal masks
• eventfd2 and epoll_* currently run through a deterministic user-mode shim: eventfd readiness is backed by internal counter state plus a pollable host pipe, and epoll wait reuses host poll(2) across registered guest fds
• wait4 currently reports deterministic single-process -ECHILD semantics after validating guest status/rusage pointers; there is not yet a modeled child-task table
• sigaltstack currently tracks deterministic single-thread alternate-stack state for libc/runtime queries; it does not imply modeled signal delivery yet
• bootstrap auxv now includes deterministic AT_MINSIGSTKSZ, AT_PLATFORM, AT_HWCAP*, AT_CLKTCK, and AT_SYSINFO_EHDR entries for libc startup paths
• cycle-accurate execution and QEMU lockstep remain separate follow-on work

Verification

Minimum structural check:

bash tools/ci/check_repo_layout.sh

Full repo-local gate pack:

bash tools/regression/run_crosschecks.sh

To require the local CLI smoke on a previously built bring-up ELF:

bash tools/regression/run_crosschecks.sh --require-smoke