-
-
Notifications
You must be signed in to change notification settings - Fork 0
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Replace the Idris2 ABI module-wide partiality waiver
feeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#380 In hyperpolymath/ephapax;Add hard-gated Creusot verification for proof-critical Rust kernels
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#378 In hyperpolymath/ephapax;clippy: box the
Value::Closurepayload (large_enum_variant, currently allowed)priority:p2Normal - queue itNormal - queue itrefactorRestructuring that preserves observable behaviourRestructuring that preserves observable behaviourscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#360 In hyperpolymath/ephapax;codegen: structural miscompile — region + let-bound String.new/String.len emits invalid wasm (type mismatch, empty stack)
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#348 In hyperpolymath/ephapax;Estate continuation (post-branding): wiki + business case; gated CLADE/ANCHOR reconciliation
documentationDocs, prose, diagrams, READMEs, ADRsDocs, prose, diagrams, READMEs, ADRspriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:needs-rulingAwaiting an owner decisionAwaiting an owner decisionStatus: Open.#327 In hyperpolymath/ephapax;Machine-readable currency: deferred follow-ups (post-checkpoint #288)
priority:p2Normal - queue itNormal - queue itscope:estateAffects many or all repos across the estateAffects many or all repos across the estatetech-debtKnown shortcut, drift, or hygiene owed - includes cleanupKnown shortcut, drift, or hygiene owed - includes cleanupStatus: Open.#289 In hyperpolymath/ephapax;deps: classify #139 fxhash CVE as dev-dep-only + recommended fix
wasmtime = { default-features = false }priority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorysecuritySecurity-related issue or vulnerabilitySecurity-related issue or vulnerabilitystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#269 In hyperpolymath/ephapax;ci:
mirror.yml— mirror-radicle job fails (needs upstream investigation at hyperpolymath/standards)bugSomething is broken or behaves incorrectlySomething is broken or behaves incorrectlycicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesCI/CD: workflows, actions, lockfiles, pins, runners, release gatespriority:p2Normal - queue itNormal - queue itscope:estateAffects many or all repos across the estateAffects many or all repos across the estatestatus:blockedCannot proceed until a dependency clearsCannot proceed until a dependency clearsStatus: Open.#268 In hyperpolymath/ephapax;Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#242 In hyperpolymath/ephapax;Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:blockedCannot proceed until a dependency clearsCannot proceed until a dependency clearsStatus: Open.#241 In hyperpolymath/ephapax;Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments
enhancementNew capability or improvement to existing behaviourNew capability or improvement to existing behaviourfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked upStatus: Open.#240 In hyperpolymath/ephapax;