text:
\section{Introduction}

The mass of our own galaxy would seem to be one of a modest set of fundamental parameters that is both necessary for a complete understanding of our universe and relatively straightforward to measure. However, convergence on a precise final answer has proven difficult.
\cite{zar89} presented three mass estimates, two of which are based on a statistical treatment of satellite galaxy radial velocities and one of which is a lower limit based on the properties of a single, extreme satellite (Leo I):
($0.93^{+0.41}_{-0.12},1.25^{+0.84}_{-0.32},  1.3^{+0.33}_{-0.33})\times 10^{12} {\rm M}_\odot$.
Exemplar, state-of-the-art studies conclude that the Galaxy's mass is
 ($0.85^{+0.23}_{-0.26},
0.96^{+0.29}_{-0.28}, 1.29^{+0.37}_{-0.37})\times 10^{12} {\rm M}_\odot$ based on satellite dynamics and the stellar escape velocity \citep{patel18,grand2019} .
The casual observer may be somewhat underwhelmed by 30 years of ``progress''.

This cursory comparison is misleading.
Studies in the intervening years identified areas ripe for improvement in earlier analyses \citep[e.g.,][]{li, patel18}, utilized the ever-increasing amount of available data \citep[e.g.,][]{watkins}, most importantly by adding proper motions \citep[e.g.,][]{bk}, and developed the cosmological framework in which we construct our models \citep[e.g.,][]{barber,carlesi,patel17}. The surprise is that better data in combination with more sophisticated models did not manifestly result in evident quantitative improvements. Derived parameter uncertainties grew or remained at best constant even as the quantity and quality of the data improved because the increasingly sophisticated models contain more degrees of freedom. The apparent stagnation is therefore partly an illusion. Improvements over the years have implicitly tested for systematic biases in previous, oversimplified and underconstrained models. However, as happens sometimes, there were no such biases of a magnitude above and beyond the quoted precision of the earlier measurements.
 This result should be both disappointing and reassuring to  practitioners in the field.

How to proceed? There is a tension between using increasingly realistic models and the larger parameter space these models access. One way to mitigate this tension is to develop more constraining parameter priors. Lower mass limits, such as provided by an escape velocity measurement or the timing argument, could possibly help, but have historically been discounted when in conflict with other results \citep[e.g.,][]{xue, gibbons}. The rejection of this additional information was not unreasonable given that the largest (most constraining) lower mass limit came from the study of the single satellite galaxy Leo I \citep{zar89,li}, which might not be on a simple orbit \citep{sales,mateo}\footnote{An alternative lower limit that is also highly constraining comes from the Local Group timing argument, but that measures the sum of the Milky Way and M 31 masses. In this case uncertainty is introduced by the partitioning of the calculated mass.}. Subsequent work, including new proper motion measurements and a careful theoretical treatment, concluded that Leo I is indeed bound to the Galaxy and likely to be a strong constraint \citep{bk}. However, any mass limit from Leo I is still susceptible to the usual
concern of relying too heavily on the properties of a single object.

Our aim is to reinforce a meaningful lower mass limit.
In doing this we have
two key points of emphasis. First, we aim to use the most distant dynamical tracers available to measure the total Galactic mass without having to extrapolate too much in radius.
Meeting this goal can be challenging because tracer particles are generally available in quantity only to distances $<$ 50 kpc \citep[e.g.,][]{williams} and the Milky Way's virial radius, is likely to be 250 kpc or larger.
Second, we want to obtain a conservative, but stringent inference using a straightforward and simple analysis.

The two principal methods for determining a Galactic lower mass limit are based on the escape velocity and the timing argument\footnote{A non-dynamical lower limit can be formulated using the cosmological baryon fraction \citep{zar17}, but the uncertainties are large until the circumgalactic gas mass is measured more precisely.}. The escape velocity argument is highly intuitive: the Galaxy needs to have sufficient mass to retain the fastest moving stars that are still found  near the Galaxy. Several treatments of the escape velocity measurement have been published recently \citep{piffl,williams,deason,grand2019}. While limits can be obtained from the fastest moving stars in any sample, the most meaningful limits come from large samples of stars where the high velocity tail truly includes stars moving at nearly the escape velocity. Such studies are necessarily carried out with samples of stars at modest Galactic radii of, at best, a few tens of kpc.
Because of this limitation, evaluating the total Galactic mass requires a model of the Galactic potential and the phase space distribution of the stars. The uncertainties arising from the model choice can then be dominant (for example, see discussion by \cite{deason} comparing their inference to that of \cite{piffl}, which differ despite similar direct measurements.)

The second method that can provide a
lower mass limit is the timing argument \citep{kw,sandage}. The timing argument posits that all matter initially expands away from the future galaxy due to universal expansion and that the subsequent gravitational pull of the galaxy eventually recalls some of that matter. In the simplest version of this scenario, the tracer particles, galaxies or stars, follow a radial orbit around a point mass. In a slightly more complex version, orbit crossing leads to the behavior seen in secondary infall models without angular momentum \citep{fillmore,bertschinger} or with angular momentum \citep{white}.
More complete treatments are currently being investigated to define the splashback radius and study the growth of structure \cite[e.g.,][]{diemer}.

In the simplest version, the system mass can be solved for analytically if the current separation and relative velocity between the Galaxy and a tracer particle are known. One does not need to know the phase space distribution of the population of tracer particles.
The advantage provided by the timing argument comes from using one additional piece of information, namely the constrained orbital time (which is the age of the Universe). Because this analysis does not require us to assume either a velocity distribution function or radial tracer density profile, we do not need detailed knowledge of the accretion history of the tracer particles or the assumption of dynamical relaxation.

The timing argument is an exceedingly elegant and robust treatment, particularly given the now well-measured age of the universe. There are a few, limited caveats. First, the standard solution is for a radial orbit. If the tracer particle has non-zero tangential velocity then the actual mass can be significantly larger than that inferred \citep[see][for how the additional tangential velocity component of Leo I as measured with {\sl HST} affected the inferred Galactic mass]{bk}. Second, the Galaxy is modeled as a point mass. Neglecting both its extent and its growth over time result in the classical timing argument underestimating the current mass within the orbit of the tracer particle.
Finally, there is the possibility of an invalid result if the tracer particle has a large peculiar velocity resulting from interactions between the tracer particle and other mass concentrations. This, for example, was one of the principal concerns in the application of the timing argument to Leo I \citep{sales,mateo}. If Leo I has been flung toward the Milky Way due to an encounter with a third galaxy, then its current position and velocity do not reflect those of the assumed cosmologically-motivated, radial orbit about the Milky Way.
All of these concerns are addressed when using numerical simulations both to calibrate the estimator and to determine the likelihood of catastrophic failures. Catastrophic failures can be mitigated by repeating the analysis using multiple, independent tracer particles.

Numerical simulations confirm
that the simple timing argument systematically underestimates the system mass and that statistical corrections are necessary to accurately recover the true mass \citep{kroeker, li}.
For the Local Group timing argument, using the orbit of M 31 and the Milky Way, that statistical correction requires increasing the result obtained from the application of the simple timing argument by about a factor of 1.7. Those studies also confirm that the scatter between the estimated and true mass can be large when using only M 31 and the Galaxy or Leo I and the Galaxy.

We present the application of the timing argument to a sample of outer halo ($R > 60$ kpc) stars from the H3 Spectroscopic Survey \citep{conroy}.
We discuss the sample of stars in \S2, the application and results from the timing argument to both the models and data in \S3, discuss the results in \S4, including an illustration of how constraining a robust lower mass limit can be on previous results, and summarize our conclusions in \S5.

\section{The Sample}

H3 is a sparsely sampled survey of $\sim$ 15,000 square degrees of sky that will provide stellar
parameters and spectrophotometric distances for $\approx$ 200,000 stars to $r = 18$  \citep{conroy}.
The procedure used for the parameter determinations and distance estimation is developed and presented by \cite{Cargile2019}. From the currently available set of observed and analyzed stars, about 80,000, we select those with fitting flag set to 0 (denoting fitting was problem-free), spectral signal-to-noise ratio (SNR) per pixel $>$ 3, a stellar rotational velocity $<$ 5 km sec$^{-1}$, an effective temperature $<$ 7000 K, and a tangential velocity, ${\rm v}_{\rm T}$, that is $ < 1000$ km sec$^{-1}$. These criteria are all meant to remove stars with problematic and unphysical parameter determinations and were arrived at after a careful examination of numerous fits.
From that sample, we then select those stars with Galactocentric distance $>$ 60 kpc (Figure \ref{fig:data}) to focus on stars that are likely to have completed only a few Galactic orbits at most.

\begin{figure}[htbp]
\begin{center}
\includegraphics[width = 0.48 \textwidth]{figure1.eps}
\end{center}
\caption{The H3 sample and outer halo stars. From the full sample we select a sample of 32 outer halo stars ($R > 60$ kpc, $-400 \le {\rm v}_{\rm R}^{\rm GSR} \le 400$ km sec$^{-1}$) for the timing argument analysis, as shown highlighted within the dotted selection box. }
\label{fig:data}
\end{figure}

In Figure \ref{fig:data} we highlight the 32 outer halo stars within a selection box that adds the criteria that the radial velocity in the Galactic Standard of Rest, ${\rm v}_{\rm R}^{{\rm GSR}}$, satisfies $|{\rm v}_{\rm R}^{\rm GSR}| < 400$ km sec$^{-1}$.
This selection removes the one star at $R > 60$ kpc that clearly does not belong in our sample (with ${\rm v}_{\rm R}^{\rm GSR} < -500$ km sec$^{-1}$). Whether this star represents a particularly catastrophic parameter determination or a physically compelling outlier, is unknown and merits follow-up, but in neither case is this star suitable for our mass estimation. A preliminary investigation of the model fit for this one star suggests that this system has a large residual flux in the IR and is, therefore, perhaps an unresolved binary star for which the parameter estimation failed. The radial velocity errors in general are on the order of a few km sec$^{-1}$, so the distance errors dominate in our calculations and are plotted in the figure.
The distribution of stars follows the apparent caustics that can be visually defined at $R < 60$ kpc. Substructure is clearly evident at $R < 50$ kpc and illustrates the difficulty faced by any statistical analysis of the velocities where one needs to model the phase space distribution.

\section{The Timing Argument}

The basic timing argument is simple in its application. Using the equations provided by \cite{sandage}, we find the smallest orbital phase, $\theta$, that solves the equations relating distance, velocity, and orbital time for a selected star. The orbital time is taken to be the age of the universe, 13.75 Gyr \citep{wmap}. Once we solve for the orbital phase, we calculate the mass.

\subsection{Calibration Using Simulations}

We construct H3 mock catalogs from the Auriga suite of simulations \citep{grand2017}.  Specifically, we have catalogs that mock the H3 selection, including a 10\% distance uncertainty, for their model numbers 6,16,21,23,24, and 27. We construct the plots corresponding to our Figure \ref{fig:data}, applying all of the same selection criteria except those aimed at removing stars with poor spectral fits. We find that models 16 and 21 have dominant substructures visible at large radii ($R > 60$ kpc) that are qualitatively different from what we find in H3 (but perhaps similar to what is seen in H3 at smaller radii, between 25 and 40 kpc). The remainder of this discussion uses only the four models that do not show such structure (see Figure \ref{fig:sims}) and are, at least visually, plausible matches to the data.

\begin{deluxetable}{rrr}
\label{tab:auriga}
\tablewidth{0pt}
\caption{Auriga Model Parameters}
\tablehead{
\colhead{Auriga Run}  &
\colhead{$M_{200}$}& \colhead{$R_{200}$}\\
&\colhead {[$10^{12} {\rm M}_\odot$]} & \colhead {[kpc]}}
        \startdata
         6&1.04 &214 \\
         23&1.58&245 \\
         24&1.49 &241\\
         27&1.75&254 \\
         \enddata
\end{deluxetable}

\begin{figure}[htbp]
\includegraphics[width = 0.48 \textwidth]{figure2.pdf}
\caption{Mock H3 catalogs created from Auriga models (6, 23, 24, and 27) from \cite{grand2017}. The outer halo star selection box from Figure \ref{fig:data} is also shown. The model number is given in the upper right of each panel. Each model contains roughly twice as many stars in the selection box than H3 because we apply the additional data quality and model fitting criteria to the actual data.}
\label{fig:sims}
\end{figure}

We are interested in using timing argument calculations for stars at 60 kpc $< R < 120$ kpc to recover M$_{200}$, where M$_{200}$
is the mass contained inside a radius within which the mean density equals 200 times the critical density. When we apply the timing argument calculation to all of the star particles in each of these four models and then scale the recovered timing mass and the calculated apocenter\footnote{We utilize the calculated apocenter distances using the timing argument equations rather than the apocenter distances presented in the H3 catalog, which are calculated in a completely independent manner. We do this to avoid introducing different model assumptions into our current analysis and discussion.} of each star particle by  the corresponding M$_{200}$ and R$_{200}$ of each model, we find the relation between derived mass and apocenter shown in the upper panel of Figure \ref{fig:apocenters}.

As expected, the timing mass significantly underestimates M$_{200}$ in all cases. The closest any estimate gets to the true value in any of the four models is less than half of the true value. The models show very little scatter in the estimates along the sequence, demonstrating that strong orbital perturbations are not significantly affecting the estimates. Because the four models together have roughly eight times as many stars as we have in the H3 sample (257 vs. 32), the likelihood of a star in H3 resulting in an estimate closer to M$_{200}$ than what we find in the models is small ($\sim 12$\%). Therefore,
the results from analyzing the models suggest that one can take the star with the largest timing mass estimate in H3, multiply that result by 2.3 (1/0.43) to estimate M$_{200}$, and still have a conservative estimate of M$_{200}$.

\subsection{Application to the H3 Outer Halo Sample}

Among the H3 sample, the largest resulting timing mass comes from H3 star 117408280 ($\alpha = 355.479908, \delta = 15.82972)$ and is $0.49 \times 10^{12}$ M$_\odot$. Using the calibration factor of 2.3, yields a timing mass estimate for M$_{200}$ of $1.1 \times 10^{12}$ M$_\odot$. Simulating the effect of the distance uncertainty by drawing 1000 realizations of the distance and re-evaluating the resulting mass estimate, we find that with 90\% confidence M$_{200} > 0.97 \times 10^{12}$ M$_\odot$.
This star has a negative radial velocity, eliminating any concern that this star happens to be an unbound, hypervelocity star \citep{brown}.

The weakness of this argument is that it relies on identifying the largest, most constraining timing mass estimate. Again, as with Leo I, we are at the mercy of a single object. Therefore, we now approach the problem in a complementary manner by looking at the distribution of timing mass estimates. We
compare the distribution of M$_{Timing}/$M$_{200}$ for the H3 data to that drawn from the four simulations.  Of course, we do not yet know M$_{200}$ for the Galaxy. However, if we choose an acceptable value of M$_{200}$ then the resulting H3 distribution should be statistically consistent with those produced from the mock catalogs. We visualize this approach in the bottom panels of Figure \ref{fig:apocenters}, where we have rescaled the H3 results using three hypothetical values of M$_{200}$ for the Milky Way ($10^{12}, 1.2\times 10^{12},$ and $1.5\times 10^{12}$ M$_\odot$).
To calculate the radial rescaling, we use the relationship between M$_{200}$ and R$_{200}$ given by the Auriga simulations (Appendix A). The differences are most evident at the largest values of M$_{Timing}/$M$_{200}$, but the entire distribution of points slides along the locus and this behavior is what we use to obtain our mass estimate.

We apply the Kolmogorov-Smirnov (KS) test to assess which rescaled H3 M$_{\rm Timing}/$M$_{200}$ distributions can be discriminated from that of the mock catalogs. If we can reject with $>$ 90\% confidence the hypothesis that the resulting M$_{\rm Timing}/$M$_{200}$ distribution is drawn from the same parent sample as the distribution obtained from the mock catalogs, then we reject the adopted M$_{200}$ as valid for the Milky Way. In this way, we conclude that M$_{200} > 0.91 \times 10^{12}$ M$_{\odot}$ (and that M$_{200} < 2.13 \times 10^{12}$ M$_\odot$). The KS test, by construction, tends to focus on deviations in the middle of the distribution rather than at the extremes, making this a valued complement to our prior estimate that used only the most extreme star. Indeed, this general behavior is also the case here, where the maximum deviation in the cumulative distributions between data and mocks for our lower limit of M$_{200} = 0.91 \times 10^{12}$  M$_{\odot}$ occurs halfway through the ranked values of M$_{\rm Timing}/$M$_{200}$ for the H3 stars.

The weakness of this argument is that because we are relying on the distribution of a sample of tracers, such as is done in the escape velocity estimation, we are assuming that the model is a fair representation of both the tracer distribution in phase space and the underlying potential. We have already seen that substructure can vary  significantly from model to model. We mitigate this concern by combining four different models, hoping to average over any undetected substructure at $R > 60$ kpc, but even so, an underlying systematic difference in the modeling can skew the result.

It is highly reassuring that both approaches, one based on the most extreme outer halo star in the sample and the other based on something closer to the typical outer halo star, produce nearly identical limits. We adopt the smaller of the two limits as the limit that we quote (M$_{200} > 0.91 \times 10^{12}$ M$_\odot$) but note that the preferred values ($1.1 \times 10^{12}$ M$_\odot$ from the single, extreme star and $1.38 \times 10^{12}$ M$_\odot$ from the most likely scaling value) provide further guidance on what the Milky Way mass might actually be.

\begin{figure}[t]
\includegraphics[width = 0.48 \textwidth]{figure3.pdf}
\caption{Distribution of scaled timing argument results. We scale the derived mass by M$_{200}$ for each of the outer halo star particles in each of the four simulations and the calculated apocenter distances by R$_{200}$ in the upper panel. The different models are represented by different colors and inbound and outbound stars by closed and open symbols, respectively. All estimates are less than half of the true value regardless of the model and whether the inward or outward moving stars are used. The dotted horizontal line represents M$_{\rm Timing}$/M$_{200} = 0.43$ and lies above all estimates.
In the lower panels, we reprise the simulation results in all panels and present the scaled values for the H3 outer halo stars, large open squares, for three different adopted values of M$_{200}$ ($10^{12}$, $1.2\times 10^{12}$ and $1.5\times 10^{12}$ M$_\odot$) in each of the three panels, as labeled. There are roughly a factor of eight more tracer particles in the combined simulations, so we do not expect the H3 sample to sample the extreme upper end of the distribution better than the simulations. This consideration and visual examination of the Figure suggest that M$_{200}$ for the Milky Way is $> 10^{12}$ M$_\odot$.}
\label{fig:apocenters}
\end{figure}

\section{Discussion}

These results will strengthen as the number of independent probes increases.
Our mass limit is consistent with that drawn previously from Leo I \citep{zar89,bk}, lending further credence to both our current limit and that from Leo I, and more data are imminent. First, H3 itself when complete will be three times the size of the current sample. Second, other large halo star surveys are  ongoing or about to start \citep{majewski,martell,deng,dalton,guiglion} from which we expect to gain more examples of such stars.  It will be increasingly more difficult to dismiss a lower mass limit of $\sim 10^{12}$ M$_\odot$.

\begin{figure}[t!]
\begin{center}
\includegraphics[width = 0.48 \textwidth]{figure4.pdf}
\end{center}
\caption{A sample of literature measurement of the Milky Way mass. The shaded region illustrates the region excluded by our 90\% confidence lower limit. Only two previous measurements are strongly argued against, but for most of the measurement our lower limit reduces the allowed range of values and so provides a useful prior. The data shown represent results (from oldest to most recent): \cite{li,xue,watkins,barber,gibbons,cautun,kafle,piffl,dierickx,patel17,fragione,carlesi,patel18,deason,watkins} (\cite{patel18} is represented twice, as the fourth and second to last).  The dashed vertical line represents our preferred value derived from the comparison of actual vs. model timing mass estimates.}
\label{fig:lit}
\end{figure}

\begin{figure}[t!]
\begin{center}
\includegraphics[width = 0.48 \textwidth]{figure5.pdf}
\end{center}
\caption{The timing argument and M$_{200} = 1.1\times 10^{12}$ M$_\odot$. We compare the distribution of stars in this phase space, reproducing Figure \ref{fig:data} to the region that produces timing mass estimates equal to or smaller than that produced by our most constraining H3 star at $R > 60$ kpc (shaded region). The shaded region traces faithfully the distribution of stars at $R < 60$ kpc and leaves little doubt that the few stars outside the shaded region are some type of interloper rather than indicative of a much larger Milky Way mass. }
\label{fig:timing_orbits}
\end{figure}

\subsection{How Constraining Is Our Lower Mass Limit?}

In Figure \ref{fig:lit}, we compare a selection of recent measurements (publication since 2008) of the Milky Way mass to our 90\% confidence lower mass limit of $0.91\times10^{12}$ M$_\odot$.
Most of the published masses refer to either M$_{200}$ or the virial mass. Only in one of these cases is the mass quoted within a fixed physical radius of 300 kpc. All of these are thought to be roughly interchangeable given the other outstanding uncertainties.

Each of the published analyses, even if they incorporate data from previous work, is independent. We argue that once provided with a robust, non-trivial lower limit each study could significantly benefit by limiting the mass range over which they consider models. In many cases in the figure, about half of the internally allowed Milky Way mass range is inconsistent with the lower limit we provide.

Two results whose uncertainty ranges lie entirely or nearly entirely within our excluded zone in Figure \ref{fig:lit}
are those of \cite{gibbons} and \cite{dierickx}. Both of these are based on an analysis of the Sagittarius dwarf, suggesting that perhaps there is something that is not well understood about this system. A third recent analysis of this system concludes that the enclosed mass within 100 kpc is $\sim$ $7 \times 10^{11}$ M$_\odot$ \citep{fardal}, which is in tension with the previous estimates and more in line with our estimates.

\subsection{Could Our Limit be a Significant Underestimate?}

We associated the star with the largest timing mass estimate with the upper end of the modeled timing mass estimates to derive a mass limit. It is possible that this star does not represent the upper end of the distribution of Milky Way stars and results in a significant underestimate of the total mass. The complementary limit obtained by using the full distribution of timing mass estimates argues against such a premise, but we noted that this analysis has its own potential problems, namely its dependence on models that might not be producing an accurate match to the phase-space distribution of the dynamical tracers even if they are accurately representing the gravitational potential.

We previously rejected one star at very large negative velocities from the sample and we have not yet considered stars with $R< 60$ kpc. Are there similar stars at $R< 60$ kpc that support an argument for a significantly larger mass estimate?
In Figure \ref{fig:timing_orbits} we reprise our presentation of the distribution of H3 stars and highlight, in the shaded region, where stars need to be to result in timing mass estimates that are less than or equal to that of our most constraining star at $R > 60$ kpc. We find only three stars in the Figure that are outside the shaded region (there are a few more beyond the boundaries of the plot but those are very likely to be spurious). We conclude that there is no indication, even when considering stars at $R<60$ kpc, of a convincing population of stars that would support a mass that is  significantly larger than that resulting from the most extreme star in our sample at $R>60$. Instead, we find a number of stars near the boundary of the shaded region at both positive and negative ${\rm v}_{\rm R}^{\rm GSR}$, providing support for the value of the timing mass estimate derived previously using the one star.

This figure raises the question of whether we should be fitting to data at all radii, rather than just to outer halo stars. There are, however, a few complications in working with stars at smaller radii. First, the steepness of the caustic curve at small radius means that the mass estimation is much more sensitive to distance errors than it is at the larger distances we have worked at. Additionally, the radial velocities are also more dependent on the proper motion measurements than for stars at large distance, where the line-of-sight velocity and the radial velocity in the Galactic frame are closer to being parallel. Lastly, working at small radii there are greater concerns regarding the impact of perturbations. All of this does not lead us to conclude that these data are not useful, but rather that they require a more complete treatment, including perhaps a closer examination of numerical simulations of halo stars, that is beyond the current study.

\section{Summary}

We propose that investigators exploring increasingly more complex and sophisticated mass modeling of the Galaxy, utilize simple and robust mass estimates to constrain the range of mass priors that they explore. In this particular study, we use the timing argument and the H3 spectroscopic catalog to present such a limit. We use mock catalogs constructed from published, independent simulations to test our methodology and validate our conclusions. Our derived, conservative, 90\% confidence lower limit on the mass of the Milky Way, $0.91\times10^{12}$ M$_\odot$, already helps eliminate much of the mass range that previous models were unable to exclude.
Our analysis suggests a Milky Way mass of $\approx 1.4 \times 10^{12}$ M$_\odot$. The properties of stars at $R<60$ kpc qualitatively support these result, but those stars become increasingly more difficult to analyze as $R$ becomes smaller. Instead, we advocate for larger samples that may identify more stars at large $R$.
Outer halo surveys are growing prodigiously. We expect a lower mass limit, such as that produced here, to continue to gain in confidence and be used generally to refine complex dynamical modeling.

\acknowledgements{We thank the Hectochelle operators Chun Ly, ShiAnne
Kattner, Perry Berlind, and Mike Calkins, and the CfA
and U. Arizona TACs for their continued support of this
long-term program. This research was supported in part
by the National Science Foundation under Grant No.
NSF PHY-1748958 and AST-1812461. DZ acknowledges the hospitality of
DARK, University of Copenhagen where the majority of this paper was written.
}

\facilities{MMT (Hectochelle)}

\begin{appendix}
\renewcommand\thefigure{\thesection.\arabic{figure}}
\setcounter{figure}{0}
\section{R$_{200}$ vs. M$_{200}$}

When we rescale the calculated apocenter distances for the H3 stars, we require a calibration of M$_{200}$ vs R$_{200}$. In order to compare most directly to the Auriga simulations, we use the quoted values for all of the \cite{grand2017} models to derive an empirical relation. In Figure \ref{fig:scaling} we show both the data as presented by \cite{grand2017} and our low order fit to the relation given by
$${\rm R}_{200} = 128.968 + 95.7676 {\rm M}_{200} - 13.8829 {\rm M}_{200}^2,$$
where M$_{200}$ is in units of $10^{12}$ M$_\odot$ and R$_{200}$ in kpc.

\begin{figure}[t!]
\begin{center}
\includegraphics[width = 0.48 \textwidth]{figure6.pdf}
\end{center}
\caption{R$_{200}$ vs. M$_{200}$ for simulated halos from the Auriga suite \citep{grand2019}. The curve is our low order fit to the relation that we use in estimating R$_{200}$ given M$_{200}$. The exact functional form is given in the text.}
\label{fig:scaling}
\end{figure}

\end{appendix}

\input{main.bbl}

\end{document}


$1200 plus $15 shipping in U.S.
I've been doing a lot of California dreaming lately. We're flying to San Diego in a couple of weeks to attend our granddaughter Ashley's high school graduation in Murrieta, where we used to live. We'll stay in a condo near Del Mar beach--always one of our favorite haunts. It will be fun to walk those serene and sunny shores again.
This painting was done in October of 2007, just before we moved back to Oregon.
You can't beat a sparkly ocean ! Beautiful painting!
Love the serene and calm mood!
Lovely sense of light, and you captured the sparkle!
Thanks, Steve! I enjoy your sunny beach plein air paintings--looks like SoCal!
Thanks, Oli and welcome to my blog. You do beautiful pastels.
Hi Shirley--thanks! Enjoyed seeing your new paintings.


text:
Q: Signed PDF content digest calculated during verification is different from decrypted digest from signature I am using properly signed PDF and standard libraries to check message digest.
signerInformation.getContentDigest() return digest value different from decripted digestInfo.getDigest() value. In addition, signature verification fails on properly signed PDF file.
Went through all possible questions about digital signature.
import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.security.PublicKey;
import java.security.Security;
import java.security.Signature;
import java.security.cert.X509Certificate;
import java.util.ArrayList;
import java.util.Base64;
import java.util.Collection;
import java.util.List;
import javax.crypto.Cipher;
import javax.xml.bind.DatatypeConverter;

import org.apache.pdfbox.pdmodel.PDDocument;
import org.apache.pdfbox.pdmodel.interactive.digitalsignature.PDSignature;
import org.bouncycastle.asn1.ASN1InputStream;
import org.bouncycastle.asn1.ASN1Primitive;
import org.bouncycastle.asn1.ASN1Sequence;
import org.bouncycastle.asn1.x509.DigestInfo;
import org.bouncycastle.cert.X509CertificateHolder;
import org.bouncycastle.cert.jcajce.JcaX509CertificateConverter;
import org.bouncycastle.cms.CMSProcessable;
import org.bouncycastle.cms.CMSProcessableByteArray;
import org.bouncycastle.cms.CMSSignedData;
import org.bouncycastle.cms.SignerInformation;
import org.bouncycastle.cms.SignerInformationVerifier;
import org.bouncycastle.cms.jcajce.JcaSimpleSignerInfoVerifierBuilder;
import org.bouncycastle.jce.provider.BouncyCastleProvider;
import org.bouncycastle.util.Store;

public class PDFSignatureValidatorSample {

    public static void verifyPDF(byte[] doc) throws Exception {
        PDDocument document = PDDocument.load(doc);
        List<PDSignature> signatures = document.getSignatureDictionaries();
        PDSignature sig = signatures.get(0);
        if (sig != null) {
            String subFilter = sig.getSubFilter();
            if (subFilter != null) {
                Collection<X509Certificate> certs = new ArrayList<X509Certificate>();
                switch (subFilter) {
                case "ETSI.CAdES.detached":
                case "adbe.pkcs7.detached":
                    byte[] signatureContent = sig.getContents(doc);
                    System.out.println("---------signatureContent length------------");
                    System.out.println(signatureContent.length);
                    String signatureContentB64 = Base64.getEncoder().encodeToString(signatureContent);
                    // System.out.println("---------signatureContent b64------------");
                    // System.out.println("signatureContentB64);
                    byte[] signedContent = sig.getSignedContent(doc);
                    String signedContentB64 = Base64.getEncoder().encodeToString(signedContent);
                    System.out.println("---------signedContent length------------");
                    System.out.println(signedContent.length);
                    // System.out.println("---------signedContent b64------------");
                    // System.out.println(signedContentB64);

                    // Now we construct a PKCS #7 or CMS.
                    CMSProcessable cmsProcessableInputStream = new CMSProcessableByteArray(signedContent);
                    CMSSignedData cmsSignedData = new CMSSignedData(cmsProcessableInputStream, signatureContent);
                    Store certificatesStore = cmsSignedData.getCertificates();
                    Collection<SignerInformation> signers = cmsSignedData.getSignerInfos().getSigners();
                    SignerInformation signerInformation = signers.iterator().next();
                    Collection matches = certificatesStore.getMatches(signerInformation.getSID());
                    X509CertificateHolder certificateHolder = (X509CertificateHolder) matches.iterator().next();
                    certificateHolder.getSerialNumber();
                    X509Certificate certFromSignedData = new JcaX509CertificateConverter()
                            .getCertificate(certificateHolder);
                    certs.add(certFromSignedData);

                    SignerInformationVerifier signerInformationVerifier = new JcaSimpleSignerInfoVerifierBuilder()
                            .build(certificateHolder);
                    boolean isValid = signerInformation.verify(signerInformationVerifier);

                    System.out.println("---------isValid - checked by signerInformation ------------");
                    System.out.println(isValid);
                    System.out.println("---------certSerialNumber dec------------");
                    System.out.println(certificateHolder.getSerialNumber());
                    System.out.println("---------certSerialNumber hex------------");
                    System.out.println(String.format("0x%08X", certificateHolder.getSerialNumber()));
                    System.out.println("---------getContentType------------");
                    System.out.println(signerInformation.getContentType().toString());
                    System.out.println("---------contentDigest base64------------");
                    byte[] contentDigest = signerInformation.getContentDigest();
                    String contentDigestB64 = Base64.getEncoder().encodeToString(contentDigest);
                    System.out.println(contentDigestB64);
                    System.out.println("---------contentDigest hex------------");
                    String contentDigestHex = DatatypeConverter.printHexBinary(contentDigest);
                    System.out.println(contentDigestHex);
                    System.out.println("---------digestAlgOID------------");
                    System.out.println(signerInformation.getDigestAlgOID());
                    System.out.println(signerInformation.getDigestAlgorithmID());
                    System.out.println("---------encryptionAlgOID------------");
                    System.out.println(signerInformation.getEncryptionAlgOID());

                    byte[] signatureBytes = signerInformation.getSignature();
                    String signatureBytesB64 = Base64.getEncoder().encodeToString(signatureBytes);
                    System.out.println("---------getSignature (encrypted) base64------------");
                    System.out.println(signatureBytesB64);
                    System.out.println("---------getSignature (encrypted) hex------------");
                    String signatureBytesHex = DatatypeConverter.printHexBinary(signatureBytes);
                    System.out.println(signatureBytesHex);

                    Cipher encryptCipher = Cipher.getInstance("RSA");
                    PublicKey publicKey = certFromSignedData.getPublicKey();
                    byte[] publicKeyBytes = publicKey.getEncoded();
                    String publicKeyBytesB64 = Base64.getEncoder().encodeToString(publicKeyBytes);
                    String publicKeyHex = DatatypeConverter.printHexBinary(publicKeyBytes);
                    System.out.println("---------publicKey base64------------");
                    System.out.println(publicKeyBytesB64);
                    System.out.println("---------publicKey hex------------");
                    System.out.println(publicKeyHex);
                    encryptCipher.init(Cipher.DECRYPT_MODE, publicKey);
                    byte[] cipherText = encryptCipher.doFinal(signatureBytes);
                    String cipherTextB64 = Base64.getEncoder().encodeToString(cipherText);
                    System.out.println("---------getSignature (decrypted) base64------------");
                    System.out.println(cipherTextB64);
                    System.out.println("---------getSignature (decrypted) hex------------");
                    String cipherTextHex = DatatypeConverter.printHexBinary(cipherText);
                    System.out.println(cipherTextHex);

                    byte[] digest = null;

                    ASN1InputStream ais = new ASN1InputStream(cipherText);
                    ASN1Primitive obj = ais.readObject();
                    DigestInfo digestInfo = new DigestInfo((ASN1Sequence) obj);
                    System.out.println("---------getAlgorithmId------------");
                    System.out.println(digestInfo.getAlgorithmId().getAlgorithm().getId());
                    System.out.println("---------getDigest hex------------");
                    digest = digestInfo.getDigest();
                    String digestHex = DatatypeConverter.printHexBinary(digest);
                    System.out.println(digestHex);
                    ais.close();

                    final Signature signature = Signature.getInstance("SHA256withRSA");
                    signature.initVerify(publicKey);
                    signature.update(digest);
                    boolean signatureVerified = signature.verify(signatureBytes);
                    System.out.println("---------signature.verify------------");
                    System.out.println(signatureVerified);

                    Security.addProvider(new BouncyCastleProvider());
                    Signature bcSignature = Signature.getInstance("RSA", "BC");
                    bcSignature.initVerify(publicKey);
                    bcSignature.update(digest);
                    boolean signatureVerifiedBC = bcSignature.verify(signatureBytes);
                    System.out.println("---------signature bc.verify------------");
                    System.out.println(signatureVerifiedBC);

                    if (digestHex != contentDigestHex) {
                        System.out.println("--------------------------------------");
                        System.out.println("---------VERIFICATION FAILED---------");
                        System.out.println("---------calculated digest------------");
                        System.out.println(contentDigestHex);
                        System.out.println("---------decrypted digest ------------");
                        System.out.println(digestHex);
                        System.out.println("--------------------------------------");
                    }
                    else
                        System.out.println("VERIFICATION PASSED");
                    break;

                default:
                    throw new IOException("Unknown certificate type " + subFilter);

                };
            };
        };
    };

    public static void main(String[] args) throws Exception {
        String fileName = "c:/test.pdf";
        byte[] doc = Files.readAllBytes(Paths.get(fileName));
        verifyPDF(doc);
    }

}

Console output:
---------signatureContent length------------
18944
---------signedContent length------------
91250
---------isValid - checked by signerInformation ------------
true
---------certSerialNumber dec------------
8811972559309533840
---------certSerialNumber hex------------
0x7A4A6A5AD8227290
---------getContentType------------
1.2.840.113549.1.7.1
---------contentDigest base64------------
hcDVAjmJolBuurj1d2/2vWgO1bajqj1M8gGsQTGa/7w=
---------contentDigest hex------------
85C0D5023989A2506EBAB8F5776FF6BD680ED5B6A3AA3D4CF201AC41319AFFBC
---------digestAlgOID------------
2.16.840.1.101.3.4.2.1
org.bouncycastle.asn1.x509.AlgorithmIdentifier@da3a9fbd
---------encryptionAlgOID------------
1.2.840.113549.1.1.11
---------getSignature (encrypted) base64------------
uV9h778EUQ0wl7O9vNd5bvuzaq/XEx0zHeSnGKWAQQGqPe1YkKByZ1Pexo4ZZ6MqrKx7Ofpvje2gMhls6SAqqs4U2bMdrrM7a3udLDWLjjCHNy90zne2KUz/737gpIbiV4kzWbxlh44oWYgwM1Zc73hwWfh+I7G/fw0H//U4fgjnxbkXIEYU/zBOqQX4xlsWSAvAs1LB1N2+ySCGU9XvT5Btj9/F+e6hH8yMoyOFB1GrChdyasToUNq+5yAQa28nIxCcURvPo20mDtACgccLCVX+joMlFT21SI7mXIiFsIdBzGMqenyi7atJV53Gtvmp+tIpxowsvWTbCEMofsYVHw==
---------getSignature (encrypted) hex------------
B95F61EFBF04510D3097B3BDBCD7796EFBB36AAFD7131D331DE4A718A5804101AA3DED5890A0726753DEC68E1967A32AACAC7B39FA6F8DEDA032196CE9202AAACE14D9B31DAEB33B6B7B9D2C358B8E3087372F74CE77B6294CFFEF7EE0A486E257893359BC65878E2859883033565CEF787059F87E23B1BF7F0D07FFF5387E08E7C5B917204614FF304EA905F8C65B16480BC0B352C1D4DDBEC9208653D5EF4F906D8FDFC5F9EEA11FCC8CA323850751AB0A17726AC4E850DABEE720106B6F2723109C511BCFA36D260ED00281C70B0955FE8E8325153DB5488EE65C8885B08741CC632A7A7CA2EDAB49579DC6B6F9A9FAD229C68C2CBD64DB0843287EC6151F
---------publicKey base64------------
MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAxR7C91bL7cfR6NFMUvDCTtg4Fp91AH89efm7+1u2NO/nJNAtKvlhItNz4GDv28Ffp5WvKRZlHe5ORbnFvbHOaAAFG43k/tIx23ePa63TdYo8LY5M1/Auw2qDt7UZPZ4vbyABF7wtuNySrYOEcK5pdyAcXjECYHfEQSAH7DItOxMtU9I+Scl7oVo5rFHWEWWxBj3sIW5hxTUAVI9kZufi53XO5jEsHwh+5olR0tsJvrEeUPFHanPiBLi3Y+rrRMimPEeqfHV8jY+rZouovWEoivxNyLb3aooihAS5x4tC1A9p92TeQHBu3RZNfoC9KBB5F0iyb/CAFw9k5Aype8vgDQIDAQAB
---------publicKey hex------------
30820122300D06092A864886F70D01010105000382010F003082010A0282010100C51EC2F756CBEDC7D1E8D14C52F0C24ED838169F75007F3D79F9BBFB5BB634EFE724D02D2AF96122D373E060EFDBC15FA795AF2916651DEE4E45B9C5BDB1CE6800051B8DE4FED231DB778F6BADD3758A3C2D8E4CD7F02EC36A83B7B5193D9E2F6F200117BC2DB8DC92AD838470AE6977201C5E31026077C4412007EC322D3B132D53D23E49C97BA15A39AC51D61165B1063DEC216E61C53500548F6466E7E2E775CEE6312C1F087EE68951D2DB09BEB11E50F1476A73E204B8B763EAEB44C8A63C47AA7C757C8D8FAB668BA8BD61288AFC4DC8B6F76A8A228404B9C78B42D40F69F764DE40706EDD164D7E80BD2810791748B26FF080170F64E40CA97BCBE00D0203010001
---------getSignature (decrypted) base64------------
MDEwDQYJYIZIAWUDBAIBBQAEIOFF1ONvV7F2h9Cq5WOGXtM0CvzuwMyL2zahkGwcjebN
---------getSignature (decrypted) hex------------
3031300D060960864801650304020105000420E145D4E36F57B17687D0AAE563865ED3340AFCEEC0CC8BDB36A1906C1C8DE6CD
---------getAlgorithmId------------
2.16.840.1.101.3.4.2.1
---------getDigest hex------------
E145D4E36F57B17687D0AAE563865ED3340AFCEEC0CC8BDB36A1906C1C8DE6CD
---------signature.verify------------
false
---------signature bc.verify------------
false
--------------------------------------
---------VERIFICATION FAILED---------
---------calculated digest------------
85C0D5023989A2506EBAB8F5776FF6BD680ED5B6A3AA3D4CF201AC41319AFFBC
---------decrypted digest ------------
E145D4E36F57B17687D0AAE563865ED3340AFCEEC0CC8BDB36A1906C1C8DE6CD
--------------------------------------

File was signed using DSS Demonstration WebApp
https://ec.europa.eu/cefdigital/DSS/webapp-demo/sign-a-document
File can be validated DSS Demonstration WebApp
https://ec.europa.eu/cefdigital/DSS/webapp-demo/validation
        <DigestMatcher type="MESSAGE_DIGEST">
            <DigestMethod>SHA256</DigestMethod>
            <DigestValue>hcDVAjmJolBuurj1d2/2vWgO1bajqj1M8gGsQTGa/7w=</DigestValue>
            <DataFound>true</DataFound>
            <DataIntact>true</DataIntact>
        </DigestMatcher>

DSS Demonstration WebApp calculates the same digest as presented code.
Digest from signature can be decrypted using openssl:
signature=uV9h778EUQ0wl7O9vNd5bvuzaq/XEx0zHeSnGKWAQQGqPe1YkKByZ1Pexo4ZZ6MqrKx7Ofpvje2gMhls6SAqqs4U2bMdrrM7a3udLDWLjjCHNy90zne2KUz/737gpIbiV4kzWbxlh44oWYgwM1Zc73hwWfh+I7G/fw0H//U4fgjnxbkXIEYU/zBOqQX4xlsWSAvAs1LB1N2+ySCGU9XvT5Btj9/F+e6hH8yMoyOFB1GrChdyasToUNq+5yAQa28nIxCcURvPo20mDtACgccLCVX+joMlFT21SI7mXIiFsIdBzGMqenyi7atJV53Gtvmp+tIpxowsvWTbCEMofsYVHw==
publicKey=MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAxR7C91bL7cfR6NFMUvDCTtg4Fp91AH89efm7+1u2NO/nJNAtKvlhItNz4GDv28Ffp5WvKRZlHe5ORbnFvbHOaAAFG43k/tIx23ePa63TdYo8LY5M1/Auw2qDt7UZPZ4vbyABF7wtuNySrYOEcK5pdyAcXjECYHfEQSAH7DItOxMtU9I+Scl7oVo5rFHWEWWxBj3sIW5hxTUAVI9kZufi53XO5jEsHwh+5olR0tsJvrEeUPFHanPiBLi3Y+rrRMimPEeqfHV8jY+rZouovWEoivxNyLb3aooihAS5x4tC1A9p92TeQHBu3RZNfoC9KBB5F0iyb/CAFw9k5Aype8vgDQIDAQAB

echo $signature | base64 --decode > signature.bin
echo -----BEGIN PUBLIC KEY----- > publicKey.pem
echo $publicKey  >> publicKey.pem
echo -----END PUBLIC KEY----- >> publicKey.pem
openssl rsautl -verify -inkey publicKey.pem  -pubin -in signature.bin |

openssl asn1parse -inform DER
    0:d=0  hl=2 l=  49 cons: SEQUENCE
    2:d=1  hl=2 l=  13 cons: SEQUENCE
    4:d=2  hl=2 l=   9 prim: OBJECT            :sha256
   15:d=2  hl=2 l=   0 prim: NULL
   17:d=1  hl=2 l=  32 prim: OCTET STRING      [HEX DUMP]:E145D4E36F57B17687D0AAE563865ED3340AFCEEC0CC8BDB36A1906C1C8DE6CD

openssl also returns the same decrypted digest as presented code.
Test file is available here:
https://drive.google.com/open?id=1UlOZOp-UYllK7Ra35dggccoWdhcb_Ntp
Message digest decrypted from signature ("real digest") is definitely digest that must be used for comparison with calculated message digest. This value is in file; more precisely, encrypted in signature field and has to be decrypted with public key (extracted from certificate). This is a fact.
According to the SignerInformation documentation getContentDigest() - return the content digest that was calculated during verification. Verification was successful, as signerInformation verify returned true. As stated, this value is calculated, not read from file (or some field in file), and indeed it has to be calculated. These two values should match.
Those facts lead to the conclusion that both values are most likely equal but given hex or b64 representation differ. The question is how original binary of values is encoded and how are they decoded from binary to their representation or better the question is how to get "real digest" from pdf file using standard java libraries.

A: ###The backgrounds
The signed byte ranges of a PDF are signed using a CMS signature container (in case of the Subfilter values adbe.pkcs7.detached and ETSI.CAdES.detached).
The first step in the construction of a CMS signature container is

For each signer, a message digest, or hash value, is computed on
the content with a signer-specific message-digest algorithm.  If
the signer is signing any information other than the content, the
message digest of the content and the other information are
digested with the signer's message digest algorithm (see Section
5.4), and the result becomes the "message digest."

(RFC 5652 section 5 Signed-data Content Type)
and later

The result of the message digest calculation process depends on
whether the signedAttrs field is present.  When the field is absent,
the result is just the message digest of the content as described
above.  When the field is present, however, the result is the message
digest of the complete DER encoding of the SignedAttrs value
contained in the signedAttrs field.  Since the SignedAttrs value,
when present, must contain the content-type and the message-digest
attributes, those values are indirectly included in the result.

(RFC 5652 section 5.4. Message Digest Calculation Process)
You apparently believe to be in the case that only the content is signed, i.e. that the signedAttrs field is absent.
This believe is wrong, every CMS signature profile (as in CAdES/PAdES) to be taken seriously requires certain additional information to be signed.
Thus, the hash value you extract from the encrypted signature value is not the hash of the signed PDF byte ranges but of the signed attributes and the hash of the signed PDF byte ranges merely is the value of one of those attributes, the message-digest attribute
If you inspect an ASN.1 dump of that signature container (openssl also allows you to create an ASN.1 dump, try it!), you'll find the (implicitly 0-tagged) signed attributes starting at offset 1828:
1828  234: . . . . . [0] {
1831   24: . . . . . . SEQUENCE {
1833    9: . . . . . . . OBJECT IDENTIFIER contentType (1 2 840 113549 1 9 3)
         : . . . . . . . . (PKCS #9)
1844   11: . . . . . . . SET {
1846    9: . . . . . . . . OBJECT IDENTIFIER data (1 2 840 113549 1 7 1)
         : . . . . . . . . . (PKCS #7)
         : . . . . . . . . }
         : . . . . . . . }
1857   47: . . . . . . SEQUENCE {
1859    9: . . . . . . . OBJECT IDENTIFIER messageDigest (1 2 840 113549 1 9 4)
         : . . . . . . . . (PKCS #9)
1870   34: . . . . . . . SET {
1872   32: . . . . . . . . OCTET STRING
         : . . . . . . . . . 85 C0 D5 02 39 89 A2 50    ....9..P
         : . . . . . . . . . 6E BA B8 F5 77 6F F6 BD    n...wo..
         : . . . . . . . . . 68 0E D5 B6 A3 AA 3D 4C    h.....=L
         : . . . . . . . . . F2 01 AC 41 31 9A FF BC
         : . . . . . . . . }
         : . . . . . . . }
1906  156: . . . . . . SEQUENCE {
1909   11: . . . . . . . OBJECT IDENTIFIER
         : . . . . . . . . signingCertificateV2 (1 2 840 113549 1 9 16 2 47)
         : . . . . . . . . (S/MIME Authenticated Attributes)
1922  140: . . . . . . . SET {
1925  137: . . . . . . . . SEQUENCE {
1928  134: . . . . . . . . . SEQUENCE {
1931  131: . . . . . . . . . . SEQUENCE {
1934   32: . . . . . . . . . . . OCTET STRING
         : . . . . . . . . . . . . 7E 0A 99 20 3C E5 79 10    ~.. <.y.
         : . . . . . . . . . . . . B7 22 59 58 A1 7F A3 3B    ."YX...;
         : . . . . . . . . . . . . C4 BC 78 14 BC C1 B6 A1    ..x.....
         : . . . . . . . . . . . . FF A6 AE 9E 0A FD 8D A6
1968   95: . . . . . . . . . . . SEQUENCE {
1970   83: . . . . . . . . . . . . SEQUENCE {
1972   81: . . . . . . . . . . . . . [4] {
1974   79: . . . . . . . . . . . . . . SEQUENCE {
1976   11: . . . . . . . . . . . . . . . SET {
1978    9: . . . . . . . . . . . . . . . . SEQUENCE {
1980    3: . . . . . . . . . . . . . . . . . OBJECT IDENTIFIER
         : . . . . . . . . . . . . . . . . . . countryName (2 5 4 6)
         : . . . . . . . . . . . . . . . . . . (X.520 DN component)
1985    2: . . . . . . . . . . . . . . . . . PrintableString 'HR'
         : . . . . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . . . . }
1989   19: . . . . . . . . . . . . . . . SET {
1991   17: . . . . . . . . . . . . . . . . SEQUENCE {
1993    3: . . . . . . . . . . . . . . . . . OBJECT IDENTIFIER
         : . . . . . . . . . . . . . . . . . . organizationName (2 5 4 10)
         : . . . . . . . . . . . . . . . . . . (X.520 DN component)
1998   10: . . . . . . . . . . . . . . . . . UTF8String 'AKD d.o.o.'
         : . . . . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . . . . }
2010   26: . . . . . . . . . . . . . . . SET {
2012   24: . . . . . . . . . . . . . . . . SEQUENCE {
2014    3: . . . . . . . . . . . . . . . . . OBJECT IDENTIFIER '2 5 4 97'
2019   17: . . . . . . . . . . . . . . . . . UTF8String 'VATHR-58843087891'
         : . . . . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . . . . }
2038   15: . . . . . . . . . . . . . . . SET {
2040   13: . . . . . . . . . . . . . . . . SEQUENCE {
2042    3: . . . . . . . . . . . . . . . . . OBJECT IDENTIFIER
         : . . . . . . . . . . . . . . . . . . commonName (2 5 4 3)
         : . . . . . . . . . . . . . . . . . . (X.520 DN component)
2047    6: . . . . . . . . . . . . . . . . . UTF8String 'HRIDCA'
         : . . . . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . . }
         : . . . . . . . . . . . . . }
2055    8: . . . . . . . . . . . . INTEGER 7A 4A 6A 5A D8 22 72 90
         : . . . . . . . . . . . . }
         : . . . . . . . . . . . }
         : . . . . . . . . . . }
         : . . . . . . . . . }
         : . . . . . . . . }
         : . . . . . . . }
         : . . . . . . }

and the second entry therein is the hash value you were looking for:
1857   47: . . . . . . SEQUENCE {
1859    9: . . . . . . . OBJECT IDENTIFIER messageDigest (1 2 840 113549 1 9 4)
         : . . . . . . . . (PKCS #9)
1870   34: . . . . . . . SET {
1872   32: . . . . . . . . OCTET STRING
         : . . . . . . . . . 85 C0 D5 02 39 89 A2 50    ....9..P
         : . . . . . . . . . 6E BA B8 F5 77 6F F6 BD    n...wo..
         : . . . . . . . . . 68 0E D5 B6 A3 AA 3D 4C    h.....=L
         : . . . . . . . . . F2 01 AC 41 31 9A FF BC
         : . . . . . . . . }
         : . . . . . . . }

which is identical to the value you calculated
---------contentDigest base64------------
hcDVAjmJolBuurj1d2/2vWgO1bajqj1M8gGsQTGa/7w=
---------contentDigest hex------------
85C0D5023989A2506EBAB8F5776FF6BD680ED5B6A3AA3D4CF201AC41319AFFBC

###Extracting the messageDigest value with PDFBox and BouncyCastle
To extract the messageDigest value you can proceed as follows:
PDDocument document = PDDocument.load(THE_PDF);
List<PDSignature> signatures = document.getSignatureDictionaries();
PDSignature sig = signatures.get(0);
byte[] cmsBytes = sig.getContents(bytes);
CMSSignedData cms = new CMSSignedData(cmsBytes);
SignerInformation signerInformation = cms.getSignerInfos().iterator().next();
Attribute attribute = signerInformation.getSignedAttributes().get(PKCSObjectIdentifiers.pkcs_9_at_messageDigest);
ASN1Encodable value = attribute.getAttributeValues()[0];
System.out.printf("MessageDigest attribute value: %s\n", value);

(CalculateDigest test testExtractMessageDigestAttributeForUser2893427)
The output:
MessageDigest attribute value: #85c0d5023989a2506ebab8f5776ff6bd680ed5b6a3aa3d4cf201ac41319affbc

###An aside
You referred to a Wiki diagram showing how a digital signature is applied and then verified. It can only be used to get the general idea, not to understand all details of specific signature profiles like CAdES/PAdES signature containers.
Furthermore, it isn't representative for all signing algorithms either. only for some, like RSA signing, you can actually extract the hash from the signature bytes value after decrypting; for others, like DSA and ECDSA, you can only check a given hash value against the signature bytes.

A: package hr.ccr.validator;

import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.security.MessageDigest;
import java.security.PublicKey;
import java.security.Security;
import java.security.Signature;
import java.security.cert.X509Certificate;
import java.util.ArrayList;
import java.util.Base64;
import java.util.Collection;
import java.util.List;
import javax.crypto.Cipher;
import javax.xml.bind.DatatypeConverter;

import org.apache.pdfbox.pdmodel.PDDocument;
import org.apache.pdfbox.pdmodel.interactive.digitalsignature.PDSignature;
import org.bouncycastle.asn1.ASN1InputStream;
import org.bouncycastle.asn1.ASN1Primitive;
import org.bouncycastle.asn1.ASN1Sequence;
import org.bouncycastle.asn1.x509.DigestInfo;
import org.bouncycastle.cert.X509CertificateHolder;
import org.bouncycastle.cert.jcajce.JcaX509CertificateConverter;
import org.bouncycastle.cms.CMSProcessable;
import org.bouncycastle.cms.CMSProcessableByteArray;
import org.bouncycastle.cms.CMSSignedData;
import org.bouncycastle.cms.SignerInformation;
import org.bouncycastle.cms.SignerInformationVerifier;
import org.bouncycastle.cms.jcajce.JcaSimpleSignerInfoVerifierBuilder;
import org.bouncycastle.jce.provider.BouncyCastleProvider;
import org.bouncycastle.util.Store;

public class PDFSignatureValidatorSample {

    public static void verifyPDF(byte[] doc) throws Exception {
        PDDocument document = PDDocument.load(doc);
        List<PDSignature> signatures = document.getSignatureDictionaries();
        PDSignature sig = signatures.get(0);
        if (sig != null) {
            String subFilter = sig.getSubFilter();
            if (subFilter != null) {
                Collection<X509Certificate> certs = new ArrayList<X509Certificate>();
                switch (subFilter) {
                case "ETSI.CAdES.detached":
                case "adbe.pkcs7.detached":
                    byte[] signatureContent = sig.getContents(doc);
                    System.out.println("---------signatureContent length------------");
                    System.out.println(signatureContent.length);
                    String signatureContentB64 = Base64.getEncoder().encodeToString(signatureContent);
                    // System.out.println("---------signatureContent b64------------");
                    // System.out.println("signatureContentB64);
                    byte[] signedContent = sig.getSignedContent(doc);
                    String signedContentB64 = Base64.getEncoder().encodeToString(signedContent);
                    System.out.println("---------signedContent length------------");
                    System.out.println(signedContent.length);
                    // System.out.println("---------signedContent b64------------");
                    // System.out.println(signedContentB64);

                    // Now we construct a PKCS #7 or CMS.
                    CMSProcessable cmsProcessableInputStream = new CMSProcessableByteArray(signedContent);
                    CMSSignedData cmsSignedData = new CMSSignedData(cmsProcessableInputStream, signatureContent);
                    Store certificatesStore = cmsSignedData.getCertificates();

                    Collection<SignerInformation> signers = cmsSignedData.getSignerInfos().getSigners();
                    SignerInformation signerInformation = signers.iterator().next();
                    Collection matches = certificatesStore.getMatches(signerInformation.getSID());
                    X509CertificateHolder certificateHolder = (X509CertificateHolder) matches.iterator().next();
                    certificateHolder.getSerialNumber();
                    X509Certificate certFromSignedData = new JcaX509CertificateConverter()
                            .getCertificate(certificateHolder);
                    certs.add(certFromSignedData);

                    SignerInformationVerifier signerInformationVerifier = new JcaSimpleSignerInfoVerifierBuilder()
                            .build(certificateHolder);
                    boolean isValid = signerInformation.verify(signerInformationVerifier);

                    byte[] encodedSignedAttributes = signerInformation.getEncodedSignedAttributes();
                    String encodedSignedAttributesB64 = Base64.getEncoder().encodeToString(encodedSignedAttributes);
                    System.out.println("---------encodedSignedAttributesB64------------");
                    System.out.println(encodedSignedAttributesB64);
                    MessageDigest sha256 = MessageDigest.getInstance("SHA-256");
                    byte[] derSignedAttributesHash = sha256.digest(encodedSignedAttributes);
                    String derSignedAttributesHashB64 = Base64.getEncoder().encodeToString(derSignedAttributesHash);
                    String derSignedAttributesHashHex = DatatypeConverter.printHexBinary(derSignedAttributesHash);
                    System.out.println("---------derSignedAttributesHashB64------------");
                    System.out.println(derSignedAttributesHashB64);
                    System.out.println("---------derSignedAttributesHashHex------------");
                    System.out.println(derSignedAttributesHashHex);

                    System.out.println("---------isValid - checked by signerInformation ------------");
                    System.out.println(isValid);
                    System.out.println("---------certSerialNumber dec------------");
                    System.out.println(certificateHolder.getSerialNumber());
                    System.out.println("---------certSerialNumber hex------------");
                    System.out.println(String.format("0x%08X", certificateHolder.getSerialNumber()));
                    System.out.println("---------getContentType------------");
                    System.out.println(signerInformation.getContentType().toString());
                    System.out.println("---------contentDigest base64------------");
                    byte[] contentDigest = signerInformation.getContentDigest();
                    String contentDigestB64 = Base64.getEncoder().encodeToString(contentDigest);
                    System.out.println(contentDigestB64);
                    System.out.println("---------contentDigest hex------------");
                    String contentDigestHex = DatatypeConverter.printHexBinary(contentDigest);
                    System.out.println(contentDigestHex);
                    System.out.println("---------digestAlgOID------------");
                    System.out.println(signerInformation.getDigestAlgOID());
                    System.out.println(signerInformation.getDigestAlgorithmID());
                    System.out.println("---------encryptionAlgOID------------");
                    System.out.println(signerInformation.getEncryptionAlgOID());

                    byte[] signatureBytes = signerInformation.getSignature();
                    String signatureBytesB64 = Base64.getEncoder().encodeToString(signatureBytes);
                    System.out.println("---------getSignature (encrypted) base64------------");
                    System.out.println(signatureBytesB64);
                    System.out.println("---------getSignature (encrypted) hex------------");
                    String signatureBytesHex = DatatypeConverter.printHexBinary(signatureBytes);
                    System.out.println(signatureBytesHex);

                    Cipher encryptCipher = Cipher.getInstance("RSA");
                    PublicKey publicKey = certFromSignedData.getPublicKey();
                    byte[] publicKeyBytes = publicKey.getEncoded();
                    String publicKeyBytesB64 = Base64.getEncoder().encodeToString(publicKeyBytes);
                    String publicKeyHex = DatatypeConverter.printHexBinary(publicKeyBytes);
                    System.out.println("---------publicKey base64------------");
                    System.out.println(publicKeyBytesB64);
                    System.out.println("---------publicKey hex------------");
                    System.out.println(publicKeyHex);
                    encryptCipher.init(Cipher.DECRYPT_MODE, publicKey);
                    byte[] cipherText = encryptCipher.doFinal(signatureBytes);
                    String cipherTextB64 = Base64.getEncoder().encodeToString(cipherText);
                    System.out.println("---------getSignature (decrypted) base64------------");
                    System.out.println(cipherTextB64);
                    System.out.println("---------getSignature (decrypted) hex------------");
                    String cipherTextHex = DatatypeConverter.printHexBinary(cipherText);
                    System.out.println(cipherTextHex);

                    byte[] digest = null;

                    ASN1InputStream ais = new ASN1InputStream(cipherText);
                    ASN1Primitive obj = ais.readObject();
                    DigestInfo digestInfo = new DigestInfo((ASN1Sequence) obj);
                    System.out.println("---------getAlgorithmId------------");
                    System.out.println(digestInfo.getAlgorithmId().getAlgorithm().getId());
                    System.out.println("---------getDigest hex------------");
                    digest = digestInfo.getDigest();
                    String digestHex = DatatypeConverter.printHexBinary(digest);
                    System.out.println(digestHex);
                    ais.close();

                    final Signature signature = Signature.getInstance("SHA256withRSA");
                    signature.initVerify(publicKey);
                    signature.update(encodedSignedAttributes);
                    boolean signatureVerified = signature.verify(signatureBytes);
                    System.out.println("---------signature.verify------------");
                    System.out.println(signatureVerified);

                    if (!digestHex.equalsIgnoreCase(derSignedAttributesHashHex)) {
                        System.out.println("--------------------------------------");
                        System.out.println("---------VERIFICATION FAILED---------");
                        System.out.println("---------calculated digest------------");
                        System.out.println(derSignedAttributesHashHex);
                        System.out.println("---------decrypted digest ------------");
                        System.out.println(digestHex);
                        System.out.println("--------------------------------------");
                    }
                    else System.out.println("VERIFICATION PASSED");
                    break;
                default:
                    throw new IOException("Unknown certificate type " + subFilter);

                };
            };
        };

    };

    public static void main(String[] args) throws Exception {
        String fileName = "c:/test.pdf";
        byte[] doc = Files.readAllBytes(Paths.get(fileName));
        verifyPDF(doc);
    }

}

redpajama_set_name: RedPajamaStackExchange


Despite years of government support of electric vehicles, not much ground has been gained.
Simply put, EV technology is not good enough yet: The best developed electric cars have a range of about 100 miles and take several hours to recharge, making them fit only for city driving.
According to a new report from the Information Technology & Innovation Foundation, that is because governments around the world are taking the wrong approach.
In "Shifting Gears: Transcending Conventional Economic Doctrines to Develop Better Electric Vehicle Batteries," Clifton Yin and Matthew Stepp break down the standard methods for encouraging the adoption of electric vehicles into two economic approaches.
The neo-Keynesian program is to subsidize EV purchases and impose gas mileage standards, in the belief that this will spur demand for more efficient cars, which drives economic growth and, in turn, innovation.
The Neoclassical approach attacks from the other end, imposing a carbon tax to make sure that drivers who choose conventional cars pay for the damage their vehicles do to the environment.
In the paper, Yin and Stepp lay out a variety of cases in which all these tactics have been tried. It is clear these approaches do not work, because so little progress has been made.
To promote the EV industry, the authors suggest "innovation economics," a third way that "recognizes knowledge, technology, entrepreneurship, and innovation as primary factors for economic growth." It boils down to the idea of supporting research and development, to overcome the most fundamental problem facing EVs: short battery life.
The pursuit of next-generation clean energy innovation — as in the case of electric vehicle batteries —will require radical or breakthrough technologies, often coined "pipeline innovation," which is long term in nature and less price sensitive at the R&D stages.
To spur that innovation, Yin and Stepp suggest funding research with money that would be used to provide EV subsidies and tax credits. They also suggest improving and legislating the relationship between the Departments of Energy and Defense, both of which sponsor research in the field, especially with respect to lithium ion batteries.
These policies would likely draw the ire of fiscal conservatives and free market proponents. But for those who want the government to help electric vehicles take off, and are frustrated by the lack of progress to date, they may be just the thing.


text:
Leadership and Board Members
Franson Fellowship
Donor Account Access
Talk to a Missions Coach
TEAM in the News
Support a Kingdom Worker (US)
Support a Kingdom Worker (CA)
Support a Project (US)
Support a Project (CA)
TEAM.org uses cookies to improve your online experience. By continuing to the site, you accept cookies from TEAM.org. View our updated Privacy and Usage Policy to learn more. To clear cookies from TEAM.org, click here.
10 Opportunities
The great Saharan desert forms a natural barrier, both culturally and ecologically, between North Africa and Sub-Saharan Africa. Islam is the predominant religion in North Africa, and the region is home to a wide variety of people groups with rich cultural histories. In recent years, political shifts in the region have opened up some of these countries like never before.
Spiritual Need in North Africa
North Africa is a region of rich cultural heritage and diverse people groups. In recent years, political shifts in many of the countries in this region have opened up opportunities for education like never before. Many parents believe that the best opportunity for their children is an education in English. Many Muslim parents also desire their children to attend schools that promote values such as respect for others and responsible living.
New schools and other educational opportunities are being developed in the region. Positions will be filled with educators who will be trained in cultural and linguistic skills overseas. The educational professionals working in these schools will have the opportunity to powerfully impact students, parents, and society through high quality educational services. We are looking for dedicated college graduates of any major who are excited about pursuing transformational education in North Africa. Join us for a two-week cultural immersion trip to check things out and then consider a two-year initial commitment.
Many immigrants from North Africa have also moved to Europe in search of employment. Here, in countries where there is religious freedom, you can also work with the European Diaspora population in a variety of educational settings. Engage with North Africans, both young and old, as they learn English, computer skills, and spend time at community centers. To find out more about TEAM's work among North Africans in Europe, click here.
Slightly more than 20% of North Africans are 20 years old or younger.
Families view education as the key to the future for their children
Countries are struggling to determine whether governments should be more Islamic or secular.
The Arab Spring is bringing unprecedented changes to this region.
Opportunites to Serve in North Africa
Opportunity Name
Long-term - Mid-term
Teaching and Education, Muslims
School Principal for International School
Mid-term
Entrepreneurial and Business, Teaching and Education, Muslims, Unreached People Groups, Youth and Children
English Teaching Tutors
Teaching and Education, Muslims, Professionals, Unreached People Groups, Youth and Children
Teaching and Education, Muslims, Unreached People Groups, Youth and Children
English TOEFL Instructor
Training Leaders and National Workers, Teaching and Education, Muslims, Youth and Children, Unreached People Groups
First Grade Teachers
North Africa Initiatives
Meet TEAM North Africa
We want to hear from you! Fill out this contact form, and we will get back to you soon. Thanks for your interest in TEAM.
TEAM Annual Report
TEAM's mission is to partner with the global Church in sending disciples who make disciples and establish missional churches to the glory of God.
© TEAM 2022 | All Rights Reserved
Talk with a Missions Coach:

redpajama_set_name: RedPajamaCommonCrawl


Have you ever taken a road trip somewhere, and after you are finish visiting your final destination you realize that it is time to take the long drive back home? If so, you are not alone because many of us have found ourselves in the same situation with traveling. Wouldn't it be nice if wherever it was that we were visiting had accommodations for their visitors and guest to stay the night or week if they wanted? Well if you visit lighthouses in some of the most far out and remote places, you will be happy to know that many of the provide exactly this type of lodging for those who are interested. They are most commonly know now a days as a lighthouse lodge.
Can you see yourself saying at your favorite lighthouse suite for the weekend in a room that is equipped with a king size bed, TV, fireplace, hot tub, free wireless internet, a dock for boating or fishing, etc? If you answer to that question is yes, you will be happy to know that there are tons of lighthouses that offer these amenities to all of their guests. Below we will be listing and reviewing lighthouses that offer exactly those types of things to their visitors, so stay tuned.


With Rosie, we started by laying out a game plan for her business rather than just discussing her site and design. We helped her develop a business plan around her desire to expand her reach using the internet so that she could turn her local success into a nationwide phenomenon.
Rosie is herself a content machine. This was both great for us and tough for her. She had so much great content that it was hard to figure out what should come first. In the end, we went back to basics: what do you want visitors to your site to do if they do nothing else. That led to the creation of a home page design that got people to start with her free program. The reason was to show how big change happens by simply taking that first step. We created a 21 day free program of her best advice and encouragement to show people how little things can add up to something really big.


1040 Park Avenue Apt.6D - Stephen P. Wald Real Estate Associates Inc.
Estate Condition – Bring Your designer! By Appointment Only.
Two photos are virtually staged.
Beautiful corner unit, huge LR with 4 oversized windows facing Park Avenue & 86 Street – southeast Park Avenue and city views. Bright sunlight throughout the apartment. Two large bedrooms + two full baths. High ceilings, oversized windows, prewar detail. This is a grand Park Avenue apartment – two units share the landing, close to Central Park and the Lex line. Full service building – doorman, lobby concierge and ive-In resident manager. There is a fitness room on the lobby level, storage bins and bike storage for rent. Washer/Dryer Allowed. Pet Friendly.


Doing good things for animals - Mogo Zoo caters for endangered animals and participates in animal breeding programs.
Care for the Wild International is an animal welfare and conservation charity who protect wildlife from exploitation and cruelty and fund projectsfor injured and sick animals , plus forthose who cannot return to the wild.
News story on extreme cruelty and trapping of Snow Leopards and trading in body parts.
Place where you can offer badly needed and urgent help with Snow Leopard anti poaching.
conservation of these these species in the wild.
For over 600 images of snow leopards.
Live from the snow leopard exhibit at the Bronx zoo.


We are a 501(c)3 non-profit organization made of our school's families, teachers, administrators, and community leaders. The PTA raises funds that support the educational success of our children and promotes parent involvement in our school through volunteer programs with a focus on filling in gaps where they may be needed. We seek to support our students and teachers alike, wherever it may be required.


text:
Michael Jackson to have Detroit street named after him, two-hour ABC special coming May 24
May 18th, 2018 by KRNB
Believe it or not, next year marks the 10th anniversary of Michael Jackson's death, and the tragic event is being examined in a two-hour ABC special airing Thursday, May 24.
The Last Days of Michael Jackson explores the late King of Pop's life and legacy, via interviews with those who knew him, and never-before-seen footage of interviews MJ did with Barbara Walters and Diane Sawyer.
The show also will feature new interviews with Derek "Cooley" Jaxson, who taught Michael how to moonwalk; the MJ impersonator Navi, who served as the star's decoy at public appearances; and Lisa Staub, a tour operator who was in front of MJ's house the day he died.
The Last Days of Michael Jackson airs May 24 at 8 p.m. ET.
Meanwhile, MJ is getting his own street in the Motor City. According to the Detroit Free Press, the city will rename a stretch of Randolph Street in the theater district "Michael Jackson Avenue." A ceremony will be held June 15, as part of the Detroit Music Weekend festival. The surviving members of The Jackson 5 will also receive a key to the city by Mayor Mike Duggan, and will play a headlining concert during the festival.
The honor comes nearly 50 years after The Jackson 5's July 23, 1968, audition for Motown Records. They were initially turned down by label head Berry Gordy, but he reconsidered and signed them in early 1969. The group remained on the label through 1975, scoring hits like "I Want You Back," "ABC" and "I'll Be There."
after coming detroit jackson michael named special street two-hour
The Weeknd makes Billboard history after 'Dawn FM' becomes top-selling album in the world Read More
Cardi B testifies she felt extremely suicidal after YouTuber Tasha K alleged she had an STI Read More
Kanye West named as suspect in criminal battery investigation Read More
Jason Momoa and Lisa Bonet to divorce after 16 years together Read More


What Spinal Problems can Occur in Childhood Cancer Survivors?
Treatment for childhood cancer can sometimes result in abnormal curvatures of the spine.
The spine is the group of bones held together with muscles and ligaments that are stacked in a straight line down the middle of the back.
Two distinct spine conditions that can result from childhood cancer treatment are called scoliosis and kyphosis.
Scoliosis can occur in many young people, especially teenagers. Most often the cause is unknown. But certain cancer treatments can increase the risk of developing the condition.
Radiation may also cause the spinal ligaments to stretch, increasing the natural curve of the spine. Radiation can also cause back muscles and ligaments to develop unevenly. Both problems can result in kyphosis.
Having a tumor in or near the spine can also cause spinal problems.
Scoliosis and kyphosis can be detected with physical examination.
Doctors may order X-rays of the spine. Scoliosis is diagnosed when there is at least a 10-degree lateral (side-to-side) curve on the X-ray. Kyphosis is confirmed when there is a 50-degree or higher curve on the X-ray.
Observation. The curve should be closely monitored, particularly during puberty and other periods of rapid growth.
Brace. If the curve progresses, a plastic body brace should be worn underneath clothing to halt progression and attempt to correct abnormal curvature.
Surgery. In cases when realignment does not work, a physician may recommend surgery to fuse or stabilize spine bones.


What filters do we have in place when we are reading our Bible? What filters do we have in place when we pray? What filters do we have in place when we ask God for a fresh word?
The problem is, we want a fresh word, a new revelation but we haven't been obedient to the last revelation. We want God to something big in us, but we haven't been faithful w/ the small things.
We have filtered things too much & therefore become disobedient to the Word of God. He gave you a fresh word asking you to step out, in faith, yet you stayed where you were. He asked you to give sacrificially & even put a specific amount in your head yet you gave what you were comfortable with. He asked you to serve in a certain position, but you come up w/ an excuse.
Why should God give us a fresh word when we haven't been obedient w/ the last one?
What filters do you need to remove: pride, comfort, financial, apathy, or …?


text:
Q: Z3 variable name causing "unknown" satisfiability Using Z3 to check the satisfiability of
(declare-fun length ((Array Int Int)) Int)

(declare-const lindx2 (Array Int Int))
(declare-const findx1 (Array Int Int))
(declare-const orig_findx1 (Array Int Int))

(assert (and
  (forall ((i Int) (j Int))
    (let ((a!1 (and (<= 0 i)
                    (<= i (- (length findx1) 1))
                    (<= 0 j)
                    (<= j (- (length orig_findx1) 1))
                    (= i j))))
      (=> a!1 (= (select findx1 i) (select orig_findx1 j)))))
  (= (length lindx2) 11)
  (forall ((i Int)) (=> (and (<= 3 i) (<= i 25)) (= (select findx1 i) (- 1))))))
(check-sat)

returns unknown. This essentially tries to assert that all elements in findx1 and orig_findx1 are equal, that length(lindx2)=11, and that findx1[i]=-1 for i=[3,25]. However, changing "findx1" to "indx1" allows Z3 to return satisfiable. Does anyone know what might be causing the unknown satisfiability? I am using Z3 version 4.8.8 on Ubuntu 18.04

A: I can replicate this, and it is really bizarre!
I'm not surprised this benchmark is unknown since it's full of quantifiers and it'd be hard to solve for z3. But changing findx1 to indx1 should have no impact on this; i.e., it should remain unknown.
I've reported this at https://github.com/Z3Prover/z3/issues/4600. The response is: It is MBQI that ends up failing to determine satisfiability. It is tied to array models. MBQI is more stable when you replace arrays by uninterpreted functions. That is, these sorts of discrepancies are unfortunately par for the course. Too bad!

A: This is unfortunately (albeit for technical reasons) not surprising: it has been observed many times before that syntactic changes (renaming symbols, reordering SMT commands) cause performance and unknown/sat fluctuations, see e.g. https://github.com/Z3Prover/z3/issues/909/. It seems that Z3's heuristics are affected by the program structure, even when explicitly setting random seeds.