Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 79
    • Issues 79
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !286

Fix potential stack overflow related to `Pretty N`.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/pretty_N_go_stackoverflow into master Jun 24, 2021
  • Overview 8
  • Commits 3
  • Pipelines 3
  • Changes 2

As reported by @simongregersen at https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E, lemmas involving Pretty N could lead to stack overflow. I minimized his problem as follows:

Lemma test_no_stack_overflow p n :
  get n (pretty (N.pos p)) ≠ Some "_"%char →
  get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
Proof. intros Hlem. apply Hlem. (* stack overflow *) Qed.

The problem is that Coq's conversion unfolds too much, and triggers the wf_guard 32 in:

Definition pretty_N_go (x : N) : string → string :=
  pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).

The wf_guard is needed to make sure that computation of pretty n for concrete numbers n works (see tests in tests/pretty.v). However, due to concrete number 32, which adds 2 ^ n Acc_intro constructors to the opaque accessibility proof N.lt_wf_0 for the well-founded recursion, Coq's conversion might unfold wf_guard 32 too eagerly.

I hence changed the 32 into S (N.size_nat x), which causes the tests in tests/pretty.v to still work, and the stack overflow to disappear. The key idea is that S (N.size_nat x) is not a concrete number if x is an open term, thus preventing wf_guard from unfolding.

Edited Jun 24, 2021 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/pretty_N_go_stackoverflow