Skip to content

ci(hardening): curl|sh installers → download-then-run#37

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/dazzling-albattani-ubS9r
Jun 18, 2026
Merged

ci(hardening): curl|sh installers → download-then-run#37
hyperpolymath merged 1 commit into
mainfrom
claude/dazzling-albattani-ubS9r

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Part of the workflow-hardening pass. Removes the curl | sh pipe-to-shell pattern from the installer sites, clearing the Hypatia download_then_run / shell_download_then_run findings.

Done

  • proof-regression.yml — the elan (Lean toolchain) installer now downloads to a file, then executes, instead of curl … | sh.
  • setup.sh — the just installer (both sites) + the usage one-liner comment switched to download-then-run (download, inspect, then run — on-brand for a security language).
  • All explanatory comments reworded so they don't themselves contain the literal the scanner matches (the lesson from the rsr_check false-positive earlier in this branch's history).

Deferred — can't do safely from this session

Both need the hyperpolymath/standards reusable contract, which is out of this session's MCP scope (the repo is private — WebFetch 403 — and list_repos/add_repo aren't surfaced here). I only have a partial SHA (524523c) from STATE, and guessing the filename/full-SHA would break the workflow:

  • secret-scanner.yml (missing_workflow) — needs hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@<full-SHA>.
  • scorecard.yml job-permissions — needs the scorecard reusable's permission contract (too-narrow perms break supply-chain scanning).

To finish those I'd need the reusable refs, standards added to scope, or for you to apply them.

https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742


Generated by Claude Code

Clears the Hypatia download_then_run / shell_download_then_run findings by
removing the pipe-to-shell pattern: download the installer to a file first,
then execute it (so it can be inspected/checksummed before running).

- proof-regression.yml: elan installer (Lean toolchain) download-then-run.
- setup.sh: the `just` installer (2 sites) + the usage one-liner comment.

Deferred (cannot do from this session): secret-scanner.yml and scorecard.yml
job-permissions both require the hyperpolymath/standards reusable contract,
which is out of this session's MCP scope (private; WebFetch 403) with only a
partial SHA known -- guessing the ref would break the workflow.

https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742
@github-actions

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 51 issues detected

Severity Count
🔴 Critical 0
🟠 High 25
🟡 Medium 26
View findings
[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (10 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/interpreter_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (6 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/parser_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (3 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Js.Promise deprecated -- use Promise (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Belt.Array deprecated -- use Array (30 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Belt.Option deprecated -- use Option (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (7 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath
hyperpolymath marked this pull request as ready for review June 18, 2026 00:02
@hyperpolymath
hyperpolymath merged commit a4485e8 into main Jun 18, 2026
29 checks passed
@hyperpolymath
hyperpolymath deleted the claude/dazzling-albattani-ubS9r branch June 18, 2026 00:02
hyperpolymath pushed a commit that referenced this pull request Jun 18, 2026
Records the approved resolution of the ADR-0007 D2 open tension (the surviving
DataExpr.neg primitive):

- neg leaves the purist core; in purist-jtv `-` is a parse error and subtraction
  is reverse-only (effect-level), in every number system.
- neg/`-` is re-admitted only under an optional feature-gated `sugar` aspect
  (adulterated-jtv), with a discouragement lint -- works but nags.
- the compiler stamps every build with a purity certificate (purist vs
  adulterated), making the escape hatch visible and accountable, not silent.
- chosen architecture: feature-gated dialect (rung 1); sidecar desugarer and
  co-product grammar noted as future purity upgrades.

Key insight recorded: subtraction-as-reverse-addition is effect-level while neg
is expression-level -- that mismatch is why neg is the escape hatch. Decision
record only; feature-gating + lint + certificate are follow-on implementation.

STATE.a2ml: artefact location + session-history catch-up (license #36,
hardening #37, ADR-0008).

https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants